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. Because the set of valid first-order formulas is recursively enumerable but not recursive, no general algorithm can settle validity for every formula, so the procedure terminates only on valid formulas. It rests on Herbrand's theorem, which implies that an unsatisfiable formula has an unsatisfiable ground instance, and on the fact that a formula is valid exactly when its negation is unsatisfiable. The procedure puts the negation of the formula in prenex form and eliminates quantifiers, generates propositional ground instances one at a time, and checks whether each is satisfiable, returning valid as soon as one is not. That last part is a resolution based satisfiability solver using unit propagation and pure literal elimination, and its resolution step can cause a worst case exponential blow up in formula size. Today the name is often used for that propositional resolution procedure alone. The Davis-Putnam-Logemann-Loveland algorithm of 1962 refined the satisfiability step to need only linear memory in the worst case, by replacing resolution with a backtracking splitting rule, and it remains the basis of the most efficient complete satisfiability solvers.