Backtracking with unit propagation, Schöning’s random walk, and PPSZ — every trick lowers the base of the exponential, none removes it
Brute force tries all 2ⁿ assignments. Cleverer algorithms still take exponential time on 3-SAT — as far as anyone knows, they must — but they shrink the base: 2ⁿ, then 1.334ⁿ, then 1.307ⁿ. At n = 100 that is the difference between about 10³⁰ steps and under a trillion.
Step or play the search and watch dead ends get cut off early. Then switch unit propagation off and run the same formula again: the tree balloons.
A small satisfiable formula: watch one wrong turn get repaired. Each step adds one node: a decision on the lowest-numbered free variable, True first. Green edges set a variable True, red edges False; amber chips (or ticks, when the tree is crowded) are literals forced by unit propagation. ✗ marks a conflict, ✓ a solution. Under the tree, every clause is coloured for the highlighted node: green satisfied, red falsified, dashed amber a unit clause that is about to force a value, fuchsia the clauses that just did. Hover or tap a node to inspect it.
Backtracking sets one variable at a time and retreats as soon as some clause has every literal false. The idea that makes it work is unit propagation: once every literal of a clause but one is false, the last one is forced, so set it at once instead of guessing. One decision often triggers a cascade of forced values, and a contradiction surfaces many levels earlier than plain backtracking would find it.
Martin Davis and Hilary Putnam proposed a procedure for satisfiability in 1960; in 1962 Davis, George Logemann and Donald Loveland replaced its memory-hungry resolution step with backtracking search. The result, with unit propagation, is called DPLL after all four. This demo uses the plainest branching rule (lowest-numbered free variable, True first) so that unit propagation is the only thing that changes.
Modern solvers add conflict-driven clause learning: when a branch fails, they work out which decisions were to blame, record that as a new clause, and jump back past irrelevant decisions instead of retreating one level at a time. The ideas appeared in GRASP (Marques-Silva and Sakallah, 1996) and were made fast by Chaff (2001). That is why SAT solvers often settle industrial formulas with millions of variables.
None of this changes the worst case. Armin Haken proved in 1985 that the pigeonhole formulas — n + 1 pigeons, n holes, every pigeon in a hole, no two sharing — need resolution proofs of exponential size. DPLL and clause-learning solvers are, in effect, searching for resolution proofs, so on these formulas they need exponential time. The three-pigeon preset above is the smallest member of that family.
Run the walk and watch the marker drift on the distance line: each flip of a variable from a broken clause moves it one step. Then run 100 trials and compare the tries they needed with (4/3)ⁿ.
Top: the current assignment (green 1, red 0); the three variables of the clause being repaired are outlined and the flipped one glows fuchsia; an amber dot marks each bit that differs from the planted solution. Middle: the fuchsia marker is the walk’s distance to the planted solution, with its recent history trailing below. Bottom: tries needed by 100 independent runs on this formula (each from its own random seed), with the worst-case (4/3)ⁿ marked. Formulas have 4.2·n random clauses chosen to agree with a hidden assignment, so a solution always exists.
Uwe Schöning’s algorithm (1999) is almost embarrassingly simple: start from a random assignment; up to 3n times, pick an unsatisfied clause and flip one of its variables at random; if nothing has worked, start again. He proved that for k-SAT it finds a solution, if there is one, in expected time (2(k−1)/k)ⁿ times a polynomial in n — that is (4/3)ⁿ·poly(n) for 3-SAT, often quoted as 1.334ⁿ.
Fix any solution and watch the Hamming distance to it. An unsatisfied clause is false, but the solution satisfies it, so at least one of its three variables disagrees with the solution. Flipping one of the three at random lowers the distance with probability at least 1/3. A walk that steps down with probability 1/3 and up with probability 2/3 drifts away from zero, but it still reaches zero from distance j within 3n steps with probability about (1/2)j, up to polynomial factors. A random start is at distance j with probability C(n, j)/2ⁿ, and averaging (1/2)j over that gives (3/4)ⁿ. So one try succeeds with probability about (3/4)ⁿ, and about (4/3)ⁿ tries are enough.
The argument fixes one solution only for the analysis. The walk itself never sees it, and may well finish at a different solution — the demo shows when that happens.
The same walk, without restarts, was Christos Papadimitriou’s 1991 algorithm for 2-SAT. With two literals per clause the step towards a solution has probability at least 1/2, so the walk is unbiased or better, and it reaches a solution after O(n²) expected flips: polynomial time.
Start the race: three algorithms solve the same random formulas at growing n, and each straight line’s slope is its exponential base. Click a record in the table to compare with the worst-case guarantees.
| Year | Worst-case 3-SAT record | Time | Kind |
|---|---|---|---|
| — | Brute force | 2ⁿ | deterministic |
| 1985 | Monien & Speckenmeyer | 1.618ⁿ | deterministic |
| 1999 | Schöning | 1.334ⁿ | randomized |
| 1998 / 2005 | Paturi, Pudlák, Saks & Zane | 1.36406ⁿ | randomized |
| 2011 | Hertli | 1.30704ⁿ | randomized |
| 2019 | Hansen, Kaplan, Zamir & Zwick | ≈ 1.307ⁿ | randomized |
Each size uses 6 random formulas with 4.26·n clauses, keeping only satisfiable ones (checked by DPLL) so all three algorithms solve the same instances. Small dots are single formulas, big dots medians, solid lines least-squares fits for n ≥ 14. Brute-force work is the exact number of assignments counting order tries before the first solution — computed by a search, not by trying them all. An algorithm drops out when one size takes it more than 1.5 s. The vertical axis is log₂, so cⁿ is a straight line of slope log₂ c.
PPSZ, after Ramamohan Paturi, Pavel Pudlák, Michael Saks and Francis Zane, goes through the variables in a random order. For each one it asks whether a small group of clauses, together with the values already chosen, forces its value; if so it takes the forced value, and otherwise it guesses at random. With luck the forcing does most of the work and only a fraction of the variables need guessing. For 3-SAT formulas with a unique solution this gives 1.30704ⁿ; Timon Hertli showed in 2011 that the same bound holds for all 3-SAT formulas. In 2019 Thomas Dueholm Hansen, Haim Kaplan, Or Zamir and Uri Zwick nudged both bounds lower by biasing the random choices, and later refinements have shaved off further decimals. The record today is still about 1.307ⁿ.
The measurements and the records answer different questions. The records are guarantees for every formula, including ones built to be nasty; the race measures typical random formulas, which good algorithms find much easier. Even so, every record is of the form cⁿ with c > 1: the improvements shrink c without ever reaching 1.
Is that unavoidable? The Exponential Time Hypothesis, a later lesson in this module, conjectures that it is: that some c > 1 is needed for 3-SAT, however clever the algorithm. It is a hypothesis, not a theorem.
Spot a mistake or have an idea?