Davis–Putnam algorithm

The procedure for checking validity of a formula φ roughly consists of these three parts: 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 that occur only positively or only negatively in the formula).

The resolution step leads to a worst-case exponential blow-up in the size of the formula.

The Davis–Putnam–Logemann–Loveland algorithm is a 1962 refinement of the propositional satisfiability step of the Davis–Putnam procedure which requires only a linear amount of memory in the worst case.

It eschews the resolution for the splitting rule: a backtracking algorithm that chooses a literal l, and then recursively checks if a simplified formula with l assigned a true value is satisfiable or if a simplified formula with l assigned false is.

It still forms the basis for today's (as of 2015) most efficient complete SAT solvers.

Two runs of the Davis-Putnam procedure on example propositional ground instances. Top to bottom, Left: Starting from the formula , the algorithm resolves on , and then on . 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 , then on , then on yields the empty clause; hence the algorithm returns " unsatisfiable ".