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 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 (Davis–Putnam procedure) that is actually only one of the steps of the original algorithm.

Overview Two runs of the Davis-Putnam procedure on example propositional ground instances. Top to bottom, Left: Starting from the formula $(a\lor b\lor c)\land (b\lor \lnot c\lor \lnot f)\land (\lnot b\lor e)$ , the algorithm resolves on $b$ , and then on $c$ . Since no further resolution is possible, the algorithm stops; since the empty clause couldn't be derived, the result is "satisfiable". Right: Resolving the given formula on $b$ , then on $a$ , then on $c$ yields the empty clause; hence the algorithm returns "unsatisfiable".

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 for checking validity of a formula φ roughly consists of these three parts:

• put the formula ¬φ in prenex form and eliminate quantifiers
• generate all propositional ground instances, one by one
• check if each instance is satisfiable.
• If some instance is unsatisfiable, then return that φ is valid. Else continue checking.

The last part is a SAT solver based on resolution (as seen on the illustration), with an eager use of unit propagation and pure literal elimination (elimination of clauses with variables of only one polarity in the formula).[clarification needed]

Algorithm DP SAT solver
Input: A set of clauses Φ.
Output: A Truth Value: true if Φ can be satisfied, false otherwise.
function DP-SAT(Φ)
if Φ is a consistent set of literals then
return true;
if Φ contains an empty clause then
return false;
for every unit clause {l} in Φ do
Φ ← unit-propagate(l, Φ);
for every literal l that occurs pure in Φ do
Φ ← pure-literal-assign(l, Φ);
// Davis-Putnam procedure:
for every literal l that occurs in both polarities in Φ do
for every clause c containing l and every clause n containing the negation of l in Φ do
rresolve(c, n);