DPLL algorithm

The DPLL algorithm, named for Martin Davis, George Logemann and Donald Loveland (with Hilary Putnam credited for the procedure it refines), is a complete, backtracking-based search algorithm for deciding whether a propositional logic formula in conjunctive normal form can be satisfied. This is the CNF-SAT problem, a central task in logic and computer science. The method was introduced in 1961 as a refinement of the earlier Davis-Putnam algorithm, a resolution-based procedure developed by Davis and Putnam in 1960. Older publications often call the Davis-Logemann-Loveland procedure the Davis-Putnam method or the DP algorithm, while the names DLL and DPLL are used by authors who keep the two procedures apart. Because it is complete, a run on any formula ends with a definite answer that the formula is satisfiable or that it is not. It remains the basis from which many later satisfiability solvers were developed.