Davis–Putnam algorithm: Difference between revisions

Revision as of 21:52, 22 September 2005

Revision as of 22:25, 22 September 2005

Line 1:

The '''[[Martin Davis|Davis]]-[[Hilary Putnam|Putnam]] algorithm''' is an algorithm for checking the [[Boolean satisfiability problem|satisfiability]] of formulae in [[conjunctive normal form]], i.e., setsets of [[clause]]s. It is a form of [[resolution_resolution (logic)|resolution]] in which variables are iteratively chosen and removed by resolving every clause in which the variable is contained positively with aany variableclause in which the variable is negated.

The algorithm works as follows:

* for every variable in the formula

** for every clause <math>c</math> containing the variable and every clause <math>n</math> containigcontaining the negation of the variable

*** resolve <math>c</math> and <math>n</math> and add the resolvant to the formula

** remove all original clauses containing the variable or its negation