◄ WORLD V · SONNY 5DART 106 · a helldive at the net

DPLL the backtracking search under every SAT solver

Is a boolean formula satisfiable? DPLL decides it by backtracking search with two accelerators: unit propagation (a one-literal clause forces its variable) and pure-literal elimination. It is the ancestor of every modern SAT and SMT solver — the engines behind verification, planning, and much of automated reasoning. And “DPLL” is really two papers, two years apart.

THE TECHNIQUE propagate what is forced, then guess

Repeatedly: if a clause has a single unassigned literal (a unit), that literal must be true — propagate it; if a variable appears only positively or only negatively (pure), fix it. When nothing is forced, pick a variable and split, recursing on both values with backtracking. Empty clause ⇒ conflict; all clauses satisfied ⇒ SAT. Edit the formula. live demo

HISTORY & CREDIT two algorithms wearing one acronym

“DPLL is the 1962 paper’s idea, including unit propagation” — unit propagation is in the 1962 1960 paper; 1962’s new idea is the split. cited

1960 · Davis & Putnam — a resolution / variable-elimination method, and already the one-literal rule (unit propagation) and affirmative-negative rule (pure literal).
1962 · Davis, Logemann & Loveland — replace resolution’s memory blow-up with backtracking case-analysis (the splitting rule). This is the “DPLL” everyone runs; the extra LL marks the different algorithm.
the boundary · SAT is the first NP-complete problem (Cook 1971) — yet DPLL with modern learning solves industrial instances with millions of variables.
the descendants · CDCL (clause learning, 1996+) turned DPLL into the SAT/SMT solvers behind chip verification and program analysis.

Two Davis papers, two methods; the resolution one (DP) and the search one (DPLL) are genuinely different. DP 1960 / DPLL 1962

RECOMMEND FOR I-13 clauses and an assignment, on arrays

Literals are signed integers, clauses and the assignment are bounded arrays — and the tiny formula decides on the compiler:

$ i13 run dpll.i13 # (-1)(1 2)(-2 3) SAT x=(false,true,true) add (-3): UNSAT (conflict at level 0)
Recommend: nothing new — a literal is a signed integer (+k = xᵤ, −k = ¬xᵤ), a clause a bounded int array, the formula an array of clauses, the partial assignment an int array; unit propagation, pure-literal, and the recursive split are array scans + integer comparisons + the recursion stack (verified SAT (F,T,T), and UNSAT when (¬x₃) is added). No new value kind.
Note: the whole solve above was forced — every assignment a unit propagation, no split needed — which is exactly why unit propagation is the workhorse of real solvers.