DPLL Algorithm

The DPLL algorithm (named for Davis, Putnam, Logemann, and Loveland) is the foundational systematic search procedure for the Boolean satisfiability problem. It operates by recursively assigning truth values to variables and simplifying the formula through unit propagation, backtracking when a contradiction is reached. DPLL is complete — it will always find a satisfying assignment if one exists, or prove unsatisfiability if none does — but its chronological backtracking strategy makes it exponentially slower than modern alternatives on most problem classes.

DPLL was the dominant SAT-solving paradigm from the 1960s through the early 2000s. Its simplicity is deceptive: the algorithm is conceptually straightforward, yet analyzing its average-case behavior led to major advances in probabilistic combinatorics and the study of computational phase transitions. The key limitation is that DPLL forgets its failures. When a contradiction is discovered, the solver retreats to the most recent decision and tries the opposite assignment, but it learns nothing about why the contradiction occurred. This amnesia is fatal: without the clause-learning mechanism of CDCL, DPLL cannot recognize that entire subtrees of the search space share a common impossibility.

The transition from DPLL to CDCL was not merely an algorithmic improvement. It was a conceptual revolution. DPLL searches; CDCL learns. The former explores a landscape; the latter constructs a theory of why the landscape has the shape it does. Every modern SAT solver retains DPLL's core propagation mechanism, but the architectural shift from chronological to non-chronological backtracking, and from amnesia to memory, changed the character of automated reasoning entirely.