The Cook–Levin Theorem

Some theorems answer a question. The Cook–Levin theorem did something rarer: it revealed that thousands of unrelated-looking hard problems are secretly the same problem in disguise.

In 1971, Stephen Cook — and independently, in the Soviet Union, Leonid Levin — proved that one specific problem, SAT (is there a way to set true/false values that makes a boolean formula true?), is NP-complete. That word means SAT is at least as hard as every problem whose answers can be checked quickly. If you could solve SAT fast, you could solve all of them fast.

How do you prove a single puzzle is as hard as a whole universe of puzzles you've never seen? The trick is breathtaking: you show that any computation that checks an answer can be rewritten, mechanically, as one giant boolean formula. Run the computer, and the formula is satisfiable. That is the idea we'll watch in action.

The core of Cook's proof is a tableau: a grid where each row is the machine's full state at one tick of time, and each column is a cell of its tape. The whole computation becomes a picture you can read top to bottom.

Below, a tiny machine flips bits on a 3-cell tape. Press Step to advance time one row at a time, and watch the grid fill in. Cook's insight was that legal grids — ones where every row follows from the one above by the machine's rules — are exactly the ones a boolean formula can pin down.

<p class="hint">{{hint}}</p>
<div id="tableau" class="tableau"></div>
<div class="legend">
  <span class="chip head">{{legend_head}}</span>
  <span class="chip state" id="stateChip">{{state_prefix}} q0</span>
</div>
<div class="status" id="status">{{status_initial}}</div>
<div class="btns">
  <button id="step" type="button">{{btn_step}}</button>
  <button id="run" type="button">{{btn_run}}</button>
  <button id="reset" type="button" class="ghost">{{btn_reset}}</button>
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .7rem; line-height: 1.45; }
.tableau { display: inline-block; border: 1px solid #cdd9e3; border-radius: 8px; overflow: hidden; }
.trow { display: flex; }
.trow.future { opacity: .28; }
.tlabel { width: 70px; height: 40px; display: flex; align-items: center; justify-content: center;
          font: 600 12px ui-monospace, monospace; background: #f1f5f9; color: #475569;
          border-right: 1px solid #cdd9e3; border-bottom: 1px solid #e2e8f0; }
.tcell { position: relative; width: 44px; height: 40px; display: flex; align-items: center; justify-content: center;
         font: 700 16px ui-monospace, monospace; color: #1d3557; border-right: 1px solid #e2e8f0;
         border-bottom: 1px solid #e2e8f0; background: #fff; }
.tcell.head { background: #dbeafe; box-shadow: inset 0 0 0 2px #2563eb; }
.tcell .caret { position: absolute; top: -1px; font-size: 10px; color: #2563eb; }
.accept .tlabel { background: #dcfce7; color: #166534; }
.legend { margin: .6rem 0 .2rem; display: flex; gap: .6rem; align-items: center; }
.chip { font: 600 12px system-ui; padding: .25rem .55rem; border-radius: 6px; }
.chip.head { background: #dbeafe; color: #1e40af; }
.chip.state { background: #e8eef3; color: #1d3557; }
.status { font-size: 1rem; font-weight: 600; margin: .5rem 0; min-height: 1.4em; }
.status.ok { color: #0a7d33; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .9rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
button:disabled { opacity: .45; cursor: not-allowed; }

// Code not found

Each filled cell is really a true/false variable in a formula. Constraints say "the start row is correct," "each step obeys the rules," and "an accepting row appears." A satisfying assignment of all those variables is a valid run of the machine — that's why solving SAT solves everything in NP.

What exactly did the theorem establish? Two halves that together make SAT NP-complete.

• SAT is in NP. Given a proposed true/false assignment, you can check whether it satisfies the formula in linear time — quick verification, the defining feature of NP.
• SAT is NP-hard. This is the deep half. Take any problem in NP. By definition it has a verifier — a polynomial-time machine that checks candidate solutions. Cook and Levin showed how to compile that machine's entire computation into a single boolean formula (the tableau) that is satisfiable exactly when a valid solution exists. The translation itself runs in polynomial time.
• So SAT is the first NP-complete problem. Every NP problem reduces to it. Solve SAT efficiently and you'd collapse P vs NP — the central open question, still unresolved and worth a Millennium Prize.
• It opened the floodgates. A year later Richard Karp reduced SAT to 21 famous problems, and today thousands are known NP-complete. Every one of those proofs traces back to this theorem.

The status is settled and proven: Cook (1971) and Levin (1973, published independently). What remains open is the prize question — whether NP-complete problems like SAT have any fast algorithm at all.

Cook–Levin is abstract, but its consequences run through everyday computing:

• Proving hardness. To show a new problem is intractable, you reduce a known NP-complete problem to it. That whole technique exists because Cook–Levin gave us the first anchor to reduce from.
• SAT solvers. Because so many problems reduce to SAT, engineers built industrial SAT solvers; today they verify chips, schedule fleets and find software bugs by encoding the task as one big formula.
• Formal verification. Checking that hardware or software can never reach a bad state is often compiled straight to SAT — the tableau idea, industrialized.
• Cryptography and security. Much of modern crypto rests on the belief that certain NP problems have no shortcut — the very belief Cook–Levin framed.

Understand this theorem and you understand the machinery behind SAT, P vs NP and nearly every "this problem is hard" claim in computer science.

The Cook–Levin theorem is the hinge the entire theory of NP-completeness turns on. By compiling any verifier's computation into a single boolean formula, it proved that SAT is as hard as everything in NP — the first member of a family that now numbers in the thousands.

Its deepest legacy is the question it sharpened rather than closed. We know all these problems stand or fall together; we still don't know whether they're truly hard. So the next time you hear that a problem is "NP-complete," remember the tableau: a grid of true/false cells, quietly tying that problem to P vs NP and to every hard problem we know.