Davis–Putnam algorithm
From Wikipedia, the free encyclopedia
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 so, strictly speaking, it is not an algorithm.
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 φ it is enough to prove that a ground instance of 
is unsatisfiable. If φ 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 c containing the variable and every clause 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
- for every clause c containing the variable and every clause n containing the negation of the variable
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.
[edit] See also
[edit] References
- Davis, Martin; Putnam, Hillary (1960). "A Computing Procedure for Quantification Theory". Journal of the ACM 7 (3): 201–215.
- Davis, Martin; Logemann, George, and Loveland, Donald (1962). "A Machine Program for Theorem Proving". Communications of the ACM 5 (7): 394–397.
- R. Dechter; I. Rish. "Directional Resolution: The Davis–Putnam Procedure, Revisited". J. Doyle and E. Sandewall and P. Torasso Principles of Knowledge Representation and Reasoning: Proc. of the Fourth International Conference (KR'94): 134-145, Kaufmann.
