Introduction

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.

Build the Tableau

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">A tiny machine reads a 3-cell tape, flips each bit it sees, then
    halts in an <b>accept</b> state. The Cook–Levin <b>tableau</b> records its whole
    run: one <b>row per time step</b>, one <b>column per tape cell</b>, plus the head
    position and current state. Press <b>Step</b> to advance time and fill the grid —
    every cell is really a true/false variable in one big boolean formula.</p>
<div id="tableau" class="tableau"></div>
<div class="legend">
  <span class="chip head">▾ head</span>
  <span class="chip state" id="stateChip">state: q0</span>
</div>
<div class="status" id="status">Step 0 of the computation. Press Step.</div>
<div class="btns">
  <button id="step" type="button">Step ▸</button>
  <button id="run" type="button">Run to accept</button>
  <button id="reset" type="button" class="ghost">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; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Cook–Levin tableau, made concrete. A deterministic machine on a 3-cell tape:
//   state q0: scan right, flipping each 0/1 it reads, move head right.
//   when the head reaches a blank '_', switch to the accepting state qA and halt.
// The tableau is the full sequence of configurations (rows). Each row records the
// tape, the head column and the state — exactly the true/false variables that the
    // Cook–Levin reduction constrains so the formula is satisfiable iff the machine accepts.
const TAPE0 = ['1','0','1','_']; // 3 data cells + a blank sentinel
const N = TAPE0.length;

// One configuration = { tape[], head, state }. step() applies the transition rule.
function step(cfg){
  if (cfg.state === 'qA') return cfg;           // halted
  const tape = cfg.tape.slice();
  const sym = tape[cfg.head];
  if (sym === '_') return { tape, head: cfg.head, state: 'qA' }; // accept
  tape[cfg.head] = (sym === '0') ? '1' : '0';   // flip the bit
  return { tape, head: cfg.head + 1, state: 'q0' };
}

// Build the whole tableau up front (finite, deterministic).
function buildTableau(){
  const rows = [{ tape: TAPE0.slice(), head: 0, state: 'q0' }];
  while (rows[rows.length-1].state !== 'qA' && rows.length < 12){
    rows.push(step(rows[rows.length-1]));
  }
  return rows;
}
const ROWS = buildTableau();
let shown = 1; // how many rows are revealed

function render(){
  const t = document.getElementById('tableau'); t.innerHTML = '';
  ROWS.forEach((cfg, r) => {
    const row = document.createElement('div');
    const accept = cfg.state === 'qA';
    row.className = 'trow' + (r >= shown ? ' future' : '') + (accept ? ' accept' : '');
    const lab = document.createElement('div');
    lab.className = 'tlabel'; lab.textContent = 't=' + r + (accept ? ' ✓' : '');
    row.appendChild(lab);
    cfg.tape.forEach((sym, c) => {
      const cell = document.createElement('div');
      cell.className = 'tcell' + (c === cfg.head ? ' head' : '');
      cell.textContent = sym;
      if (c === cfg.head){ const car = document.createElement('span'); car.className='caret'; car.textContent='▾'; cell.appendChild(car); }
      row.appendChild(cell);
    });
    t.appendChild(row);
  });
  const cur = ROWS[shown-1];
  document.getElementById('stateChip').textContent = fmt('state: %state%', { state: cur.state });
  const done = cur.state === 'qA';
  document.getElementById('step').disabled = done;
  document.getElementById('run').disabled = done;
  const s = document.getElementById('status');
  if (done){ s.textContent = 'Accepting row reached — the formula is satisfiable. ✓'; s.className = 'status ok'; }
  else { s.textContent = fmt('Row %v% filled. Each step must obey the rules; press Step.', { v: shown-1 }); s.className = 'status'; }
}
function doStep(){ if (shown < ROWS.length) shown++; render(); }
function doRun(){ shown = ROWS.length; render(); }
function doReset(){ shown = 1; render(); }
document.getElementById('step').addEventListener('click', doStep);
document.getElementById('run').addEventListener('click', doRun);
document.getElementById('reset').addEventListener('click', doReset);
render();
Result
Console

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.

The Real Complexity

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.

Where It Matters

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.

Conclusion

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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/cook-levin/Content licensed under CC BY-NC 4.0.