The idea: guess, but let the clauses force what they can
The Boolean satisfiability problem (SAT) asks: can the variables of a formula get values true (1) or false (0) so that the whole formula is true? Solvers take the formula in conjunctive normal form (CNF): an AND of clauses, where each clause is an OR of literals, and a literal is a variable a or its negation ¬a. A clause is true when at least one of its literals is true, so a single clause with every literal false makes the whole formula false.
A truth table would try all 2n assignments (see Truth Tables and Sets). The DPLL algorithm (Davis, Putnam, Logemann and Loveland, 1962) searches instead: it guesses one variable at a time, and after each guess it lets the clauses force every value they can. On the canvas the left panels are the clauses and the trail (the stack of assignments, newest at the bottom); the right panel is the search tree, one box per guess.
Unit propagation
A clause whose literals are all false except one is a unit clause. It can only become true one way, so its last literal is forced. Setting it can make other clauses unit in turn, and the chain goes on until no clause is unit. This is unit propagation, the rule that does most of the work in every SAT solver. A forced value is not a guess: it is never flipped, only undone when a guess above it is undone.
The Unit chain formula starts with the one-literal clause (a). Five propagations later every clause is true and the tree is just the start box (Demo 1: unit propagation alone solves it). Plain backtracking, which only checks for conflicts, needs 6 guesses and hits a conflict on the same formula.
Pure literals
A literal is pure if it appears in the clauses that are still open while its negation does not. Making it true satisfies every clause that holds it and takes nothing away from any other clause, so DPLL may set it without a guess. In the Pure literals formula, d appears only positively, and after the guess a = 1 the only open clause is (¬a ∨ ¬b ∨ ¬c), where ¬b is pure. One guess solves it; with unit propagation alone it takes two (Demo 3: pure literal rule). Modern solvers drop this rule because checking it is costly on large formulas.
Guess, conflict, backtrack
When no rule applies, DPLL makes a decision: here the first free variable, value 1 first. Each decision starts a new decision level on the trail. If some clause ends up with every literal false, that is a conflict: the trail is popped back to the newest decision, and that variable gets its other value. The flipped value is no longer a choice, so if it fails as well the search backs up one more level. When no decision is left to flip, the formula is unsatisfiable.
DPLL(formula):
loop:
if some clause has every literal false: (conflict)
pop the trail to the newest decision x = v not yet flipped
if there is none: return UNSAT
set x = not v (flipped, not a decision)
else if every clause has a true literal: return SAT
else if some clause is unit: set its last literal true
else if some literal is pure: set it true
else: decide: pick a free variable x, set x = 1
In One wrong guess, the guess a = 1 forces c, then d, then ¬b, and the clause (¬d ∨ ¬a ∨ b) has no true literal left. The solver pops the trail, flips to a = 0, and propagation finishes the job: b, ¬d, ¬c (Demo 2: wrong guess, conflict, flip).
The search tree
Each box in the tree is a guess; the line under it, after ⇒, lists the literals that propagation forced there. A red tag names the clause of a conflict, a green one marks the satisfying leaf. The two trees below are for the same formula: Knuth's 8-clause formula R, where each clause has 3 literals and every variable appears with both signs.
With DPLL, two guesses (a and b) are always enough: the other two variables are forced and the forced values clash. All four leaves fail, so R is unsatisfiable (Demo 5: Knuth's R, unsatisfiable). Plain backtracking reaches the same answer only after it has guessed down to the last variable in almost every branch (Demo 6: R with plain backtracking). Drop the last clause and the formula R′ is satisfiable: DPLL fails under a = 1, then finds a = 0, b = 1 with c free (Demo 4: Knuth's R′, satisfiable).
Counting the work
The table on the canvas runs the same formula under each set of rules. Guesses count every box below the start box (decisions plus flips); propagated counts unit and pure assignments.
| formula | DPLL guesses / conflicts | unit only | plain backtracking | result |
|---|---|---|---|---|
| Unit chain | 0 / 0 | 0 / 0 | 6 / 1 | SAT |
| One wrong guess | 2 / 1 | 2 / 1 | 19 / 9 | SAT |
| Pure literals | 1 / 0 | 2 / 0 | 5 / 1 | SAT |
| Knuth's R′ | 5 / 2 | 6 / 2 | 17 / 7 | SAT |
| Knuth's R | 6 / 4 | 6 / 4 | 26 / 14 | UNSAT |
Why it matters
SAT was the first problem shown to be NP-complete (Cook, 1971): every problem whose answers can be checked quickly reduces to it (see P vs NP). No known algorithm is fast on every formula, yet solvers built on DPLL handle industrial formulas with millions of clauses, for hardware and software verification, scheduling and planning. The search is the same depth-first pattern as CSP backtracking and N-Queens, with unit propagation playing the part of forward checking.
What the page leaves out
Modern solvers are CDCL (conflict-driven clause learning): at a conflict they analyse the implication graph, learn a new clause that blocks the cause, and jump back several levels at once (non-chronological backjumping). They find unit clauses fast with two watched literals per clause, pick variables with activity heuristics such as VSIDS, keep the last value of each variable (phase saving), restart often, and simplify the formula before the search. The page uses a fixed variable order a..e, value 1 first, scans every clause on every step, and has no learning or restarts. Turning any formula into CNF (the Tseitin transformation) is also left out.