DPLL

DPLL, named after Davis, Putnam, Logemann, and Loveland, is a complete backtracking algorithm for determining the satisfiability of propositional logic formulas in conjunctive normal form (CNF). It was developed as an improvement of the earlier Davis–Putnam procedure and remains a foundational method in the study of SAT.

The algorithm operates on a CNF formula by performing a depth-first search over truth assignments. Its two main mechanisms are unit propagation and recursive branching. Unit propagation repeatedly assigns truth values to literals that are the sole remaining way to satisfy a clause (unit clauses), simplifying the formula as it goes. If a conflict arises, meaning a clause fails to be satisfied (an empty clause), the algorithm backtracks to the most recent decision point and tries the opposite truth value for that variable. If all clauses become satisfied, a satisfying assignment has been found.

DPLL typically uses a decision rule to choose an unassigned variable and to try a truth value, coupled with ongoing simplification by unit propagation. Pure literal elimination (assigning a value that satisfies all occurrences of a variable) can also be employed, though it is not essential to the core algorithm.

DPLL is a complete procedure: it will determine satisfiability for any CNF formula, though its worst-case running time is exponential in the number of variables. In practice, performance depends on variable selection heuristics and the order of decisions. The algorithm forms the basis of many SAT solvers, with modern variants often extended by techniques such as conflict-driven clause learning and non-chronological backtracking to improve efficiency.