Davis–Putnam algorithm: Difference between revisions

Revision as of 15:20, 13 August 2010

Revision as of 15:22, 13 August 2010

Line 2:

{{Confusing|article|date=February 2009}}

The '''Davis-PutnamDavis–Putnam algorithm''' was developed by [[Martin Davis]] and [[Hilary Putnam]] for checking the validity of a [[first-order logic]] formula using a [[Resolution (logic)|resolution]]-based decision procedure for [[propositional logic]]. Since the set of valid first-order formulas is [[recursively enumerable]] but not [[recursive]], there exists no general algorithm to solve this problem. Therefore, the Davis-Putnam algorithm only terminates on valid formulas. Today, the term "Davis-Putnam algorithm" is often used synonymously with the resolution-based propositional decision procedure that is actually only one of the steps of the original algorithm.

The procedure is based on [[Herbrand's theorem]], which implies that an [[satisfiable|unsatisfiable]] formula has an unsatisfiable [[ground instance]], and on the fact that a formula is [[valid]] if and only if its negation is unsatisfiable. Taken together, these facts imply that to prove the validity of ''φ'' it is enough to prove that a ground instance of ''¬φ'' is unsatisfiable. If ''φ'' is not valid, then the search for an unsatisfiable ground instance will not terminate.

Line 19:

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

At each step, the intermediate formula generated is [[equisatisfiable]] to the original formula, but it does not retain [[Logical equivalence|equivalence]]. The resolution step leads to a worst-case exponential blow-up in the size of the formula. The [[DPLL algorithm]] is a refinement of the propositional satisfiability step of the Davis-PutnamDavis–Putnam procedure, that requires only a linear amount of memory in the worst case.

==See also==