Proof — Davis–Putnam algorithm

Statement

The Davis–Putnam algorithm is a resolution-based procedure for deciding the satisfiability of propositional formulas. It uses unit propagation and pure literal elimination. Published in JACM 1960; the backbone of modern SAT solvers and the precursor to DPLL.

Formula

SAT decision procedure

Equation

Unit propagation + pure literal elimination

Proof sketch

Davis and Putnam gave the first practical algorithm for propositional satisfiability in "A Computing Procedure for Quantification Theory" (JACM 1960). The procedure was later refined by Logemann and Loveland into DPLL (1962). Cook (1971) proved SAT is NP-complete, establishing the theoretical importance of the problem Davis–Putnam addresses.