Davis–Putnam algorithm: Difference between revisions

Revision as of 14:13, 9 November 2009

Revision as of 17:21, 17 December 2009

Line 1:

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

The '''Davis–Putnam algorithm''' was developed by [[Martin Davis]] and [[Hilary Putnam]] for checking the validity of a [[first-order logic]] formula using a [[resolution]]-based decision procedure for [[propositional logic]]. ItSince isthe knownset thatof therevalid existfirst-order noformulas is [[decisionrecursively procedureenumerable]] forbut not [[recursive]], there exists no general algorithm to solve this taskproblem. Therefore, the Davis–PutnamDavis-Putnam ''procedure''algorithm doesonly not terminateterminates on somevalid inputsformulas.{{Fact|date=May 2009}}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 <math>\phi</math> it is enough to prove that a ground instance of <math>\lnot\phi</math> is unsatisfiable. If <math>\phi</math> isn'tis not valid, then the search for an unsatisfiable ground instance will not terminate.

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 <math>\phi</math> it is enough to prove that a ground instance of <math>\lnot\phi</math> is unsatisfiable. If <math>\phi</math> isn't valid, then the search for an unsatisfiable ground instance will not terminate.

The procedure roughly consists of these three parts:

* put the formula in [[prenex]] form and eliminate quantifiers

* generate one by one all propositional ground instances

* ...and check for each if it is satisfiable

The last part is probably the most innovative one, and works as follows:

Line 17 ⟶ 18:

** 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–Putnam procedure, that requires only a linear amount of memory in the worst case.

The step done for each variable preserve satisfiability, while not preserving the models; in other words, the generated formula is [[equisatisfiable]] but not [[Logical equivalence|equivalent]] with the original one.

The [[DPLL algorithm]] is a refinement of the Davis–Putnam procedure that stemmed from its first implementation.

==See also==