Davis–Putnam algorithm
Encyclopedia
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. 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 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.
The procedure roughly consists of these three parts:
The last part is probably the most innovative one, and works as follows:
At each step, the intermediate formula generated is equisatisfiable to the original formula, but it does not retain 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.
Martin Davis
Martin David Davis, is an American mathematician, known for his work on Hilbert's tenth problem . He received his Ph.D. from Princeton University in 1950, where his adviser was Alonzo Church . He is Professor Emeritus at New York University. He is the co-inventor of the Davis-Putnam and the DPLL...
and Hilary Putnam
Hilary Putnam
Hilary Whitehall Putnam is an American philosopher, mathematician and computer scientist, who has been a central figure in analytic philosophy since the 1960s, especially in philosophy of mind, philosophy of language, philosophy of mathematics, and philosophy of science...
for checking the validity of a first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
formula using a resolution
Resolution (logic)
In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem-proving technique for sentences in propositional logic and first-order logic...
-based decision procedure for propositional logic. Since the set of valid first-order formulas is recursively enumerable but not recursive
Recursion
Recursion is the process of repeating items in a self-similar way. For instance, when the surfaces of two mirrors are exactly parallel with each other the nested images that occur are a form of infinite recursion. The term has a variety of meanings specific to a variety of disciplines ranging from...
, 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 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.
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:
- for every variable in the formula
- for every clause
containing the variable and every clause 
containing the negation of the variable
- resolveResolution (logic)In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem-proving technique for sentences in propositional logic and first-order logic...
c and n and add the resolvent to the formula
- resolve
- remove all original clauses containing the variable or its negation
- for every clause
At each step, the intermediate formula generated is equisatisfiable to the original formula, but it does not retain equivalence
Logical equivalence
In logic, statements p and q are logically equivalent if they have the same logical content.Syntactically, p and q are equivalent if each can be proved from the other...
. The resolution step leads to a worst-case exponential blow-up in the size of the formula. The DPLL algorithm
DPLL algorithm
The Davis–Putnam–Logemann–Loveland algorithm is a complete, backtracking-based algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem....
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.