Davis–Putnam algorithm

The Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first-order logic formula. It is known that there exist no decision procedure for this task. Therefore the Davis–Putnam procedure does not terminate on some inputs.^{[citation needed]}

The procedure is based on Herbrand's theorem, which implies that an unsatisfiable formula has is 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 ${\displaystyle \phi }$ it is enough to prove that a ground instance of ${\displaystyle \lnot \phi }$ is unsatisfiable. If ${\displaystyle \phi }$ 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 ground instances
• ...and check for each if it is satisfiable

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

• for every variable in the formula
  • for every clause ${\displaystyle c}$ containing the variable and every clause ${\displaystyle n}$ containing the negation of the variable
    • resolve c and n and add the resolvent to the formula
  • remove all original clauses containing the variable or its negation

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

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

See also

• Herbrandization

References

• Davis, Martin (1960). "A Computing Procedure for Quantification Theory". Journal of the ACM. 7 (3): 201–215. doi:10.1145/321033.321034. {{cite journal}}: Unknown parameter |coauthors= ignored (|author= suggested) (help)

• Davis, Martin (1962). "A Machine Program for Theorem Proving". Communications of the ACM. 5 (7): 394–397. doi:10.1145/368273.368557. {{cite journal}}: Unknown parameter |coauthors= ignored (|author= suggested) (help)

• R. Dechter. "Directional Resolution: The Davis–Putnam Procedure, Revisited". In J. Doyle and E. Sandewall and P. Torasso (ed.). Principles of Knowledge Representation and Reasoning: Proc. of the Fourth International Conference (KR'94). Kaufmann. pp. 134–145. {{cite conference}}: Cite has empty unknown parameter: |conferenceurl= (help); Unknown parameter |booktitle= ignored (|book-title= suggested) (help); Unknown parameter |coauthors= ignored (|author= suggested) (help)