Davis–Putnam algorithm: Difference between revisions

Revision as of 00:43, 7 September 2006

Revision as of 02:12, 7 September 2006

Line 1:

The '''Davis–Putnam algorithm''' is an algorithmwas developed by [[Martin Davis]] and [[Hilary Putnam]] for checking the [[Boolean satisfiability problem|satisfiability]] of [[propositional logic]] formulae in [[conjunctive normal form]], ''i.e.'', sets of [[Clause (logic)|clauses]]. It is a form of [[resolution (logic)|resolution]] in which variables are iteratively chosen and removed by resolving every clause in which the variable is contained positively with any clause in which the variable is negated.

The algorithm works as follows: