Flip switches until every clause is happy. Why 2ⁿ assignments is a wall, and the sharp cliff where random formulas go from easy to impossible
A formula is a list of clauses, and each clause wants at least one of its three literals to be true. Your job is to set the switches so that every clause is pleased at once. It sounds like a puzzle — and nobody knows a fast way to solve it in general.
Flip the seven switches until every clause turns green. Only two of the 128 settings work; the map below keeps track of where you have been.
(¬x₁ ∨ ¬x₂ ∨ ¬x₃) ∧ (x₁ ∨ x₂ ∨ ¬x₄) ∧ (¬x₁ ∨ ¬x₃ ∨ ¬x₆) ∧ (¬x₂ ∨ x₅ ∨ ¬x₆) ∧ (x₂ ∨ ¬x₅ ∨ ¬x₇) ∧ (x₃ ∨ ¬x₅ ∨ ¬x₇) ∧ (¬x₁ ∨ x₄ ∨ ¬x₇) ∧ (x₂ ∨ x₄ ∨ x₆) ∧ (¬x₂ ∨ ¬x₅ ∨ x₆) ∧ (¬x₃ ∨ ¬x₆ ∨ x₇) ∧ (x₁ ∨ ¬x₆ ∨ x₇) ∧ (¬x₂ ∨ x₅ ∨ x₆) ∧ (x₁ ∨ ¬x₆ ∨ ¬x₇) ∧ (x₄ ∨ ¬x₅ ∨ x₇) ∧ (¬x₁ ∨ ¬x₄ ∨ x₇) ∧ (x₂ ∨ x₅ ∨ ¬x₆)
Click a switch or any literal to flip that variable. A literal lights green when it is true; a clause (an OR of three literals) is green when at least one of its literals is. In the map, each square is one setting: grey is unvisited, red is visited (darker means more clauses violated), green is a solution, and the fuchsia outline is where you are. Neighbouring squares differ in exactly one switch.
A literal is a variable or its negation, such as x₃ or ¬x₃. A clause is an OR of literals, and a formula in conjunctive normal form (CNF) is an AND of clauses. The satisfiability problem, SAT, asks whether some true/false assignment makes the whole formula true. In k-SAT every clause has exactly k literals. Any Boolean constraint whatsoever can be written in CNF, so SAT is a universal language for yes-or-no puzzles: schedules, circuits, Sudoku, hardware bugs.
SAT was the first problem shown to be NP-complete — Stephen Cook proved it in 1971, and Leonid Levin independently in work published in 1973. A year after Cook, Richard Karp’s 1972 list of 21 NP-complete problems included 3-SAT, reached through Cook’s reduction. NP-complete means that a fast algorithm for SAT would give a fast algorithm for every problem whose solutions can be checked quickly.
The width of the clauses matters enormously. 2-SAT, where every clause has two literals, can be solved in linear time (Aspvall, Plass and Tarjan, 1979). With three literals per clause, the problem is already NP-complete.
Hardness is a statement about the worst case. Industrial SAT solvers routinely handle formulas with millions of clauses from hardware and software verification. What nobody has is an algorithm guaranteed to be fast on every formula.
Press Run and watch the odometer check every setting, then drag n upwards. Each extra switch doubles the work, and the projected time climbs past the age of the universe.
Each square is a switch (green = true). The odometer counts in binary, checking every setting against a random 3-CNF with 120 clauses — 6n random clauses, which for n ≳ 10 is almost always unsatisfiable. The rate is measured live (a short calibration on load, then the real run). Up to n = 26 the count really runs to the end; above that it samples and extrapolates. Tap the chart to choose n.
With n variables there are 2ⁿ assignments. Checking one against m clauses takes time proportional to the size of the formula, so trying them all costs 2ⁿ times a polynomial — the trivial upper bound that every SAT algorithm is measured against. Compare the formula size, which grows only linearly in n.
At a billion checks per second, n = 60 takes about 2⁶⁰ / 10⁹ ≈ 1.2 × 10⁹ seconds, roughly 36 years. n = 100 takes about 1.3 × 10²¹ seconds, or 4 × 10¹³ years — some three thousand times the age of the universe.
Exponential time turns hardware improvements into small additive gains. A computer a thousand times faster lets brute force handle only about ten more variables in the same time, because 2¹⁰ ≈ 1000. Cleverer algorithms shrink the base of the exponential below 2, but none known removes the exponential — see also Searching Smarter.
Random formulas with αn clauses: watch the share that can be satisfied fall off a cliff near 4.27 clauses per variable. Switch between sizes to see the cliff sharpen, and hover to read the numbers.
Each point is 50 random 3-CNFs with m = round(αn) clauses (three distinct variables per clause, random signs), solved by the module’s DPLL solver with unit propagation. “Nodes” counts branching decisions. The selected size is drawn solid; other sizes you have run stay faint for comparison. Sampling runs in 10 ms slices so the page stays responsive; n = 80 takes a few seconds.
In 1991 Peter Cheeseman, Bob Kanefsky and William Taylor published “Where the really hard problems are”, observing that hard instances of NP-complete problems cluster at a critical value of some parameter. In 1992 David Mitchell, Bart Selman and Hector Levesque found the hardness peak for random 3-SAT near 4.3 clauses per variable. Below the threshold almost all random formulas are satisfiable and easy; far above it almost all are unsatisfiable and refutations are found quickly; near it, solvers struggle most. That is an empirical observation about typical instances, not a theorem about the worst case.
Ehud Friedgut proved in 1999 that the transition is sharp: for each n there is a threshold where the probability of satisfiability drops from near 1 to near 0 in a window that shrinks as n grows — though his theorem allows that threshold to depend on n.
The value ≈ 4.267 comes from the cavity method of statistical physics (Marc Mézard, Giorgio Parisi and Riccardo Zecchina, 2002). For 3-SAT it is not proved: the rigorous bounds are roughly 3.52 < α₃ < 4.49. In 2015 Jian Ding, Allan Sly and Nike Sun proved that the physicists’ threshold formula is correct for k-SAT for every sufficiently large k.
At the small sizes a browser can sample, the half-satisfiable point and the hardness peak sit a little to the right of 4.27 — a finite-size effect that shrinks as n grows — while the effort at the peak climbs steeply with n.
Spot a mistake or have an idea?