Davis–Putnam algorithm

The Davis-Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the satisfiability of propositional logic formulae in conjunctive normal form, i.e., sets of clauses. It is a form of 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:

• 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 ${\displaystyle c}$ and ${\displaystyle 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 name Davis–Putnam algorithm or DP algorithm is sometimes incorrectly used to refer to the related but distinct DPLL algorithm.

See also

• DPLL algorithm

References

• Davis, Martin (1960). "A Computing Procedure for Quantification Theory". Journal of the ACM. 7 (3): 201–215. {{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. {{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)