The Cook-Levin Theorem

The Cook-Levin Theorem states that SAT is NP-complete. This has two halves, both essential to the definition of NP-completeness. First, SAT is in NP: given a satisfying assignment as a certificate, a verifier can check it in polynomial time by simply plugging in the values and evaluating the formula. Second — and this is the hard direction — SAT is NP-hard: every language $L \in \mathrm{NP}$ reduces to SAT via a polynomial-time (Karp) reduction. The key technical tool is a nondeterministic Turing machine (NTM), the standard model underlying the definition of NP: a language $L$ is in NP exactly when some NTM $N$ decides $L$ and, on every input of length $n$, every branch of $N$'s computation halts within $p(n)$ steps for some polynomial $p$. The proof of NP-hardness takes an arbitrary such $N$ and an arbitrary input $w$, and mechanically produces a Boolean formula $\phi_{N,w}$ with the property

Crucially, this construction must work for every NTM $N$ deciding every language in NP — it cannot be tailored to any particular problem. That is what makes SAT a universal target: it can simulate the internal machinery of any polynomial-time nondeterministic computation whatsoever. The construction represents a computation as a tableau: a two-dimensional grid where row $i$ records the machine's full configuration (tape contents, head position, state) at time step $i$. Since the machine runs in time $p(n)$, it uses at most $p(n)$ tape cells, so the tableau is a $p(n) \times p(n)$ grid — polynomial in size. The Boolean formula introduces one variable for "cell $(i,j)$ of the tableau holds symbol $s$" for every cell, every step, and every possible symbol/state marker, then writes clauses forcing the grid to be a legal, accepting computation history of $N$ on $w$. Satisfying the formula is equivalent to the existence of such a history, which is equivalent to $N$ accepting $w$.

Setting up the tableau

Fix a nondeterministic Turing machine $N = (Q, \Sigma, \Gamma, \delta, q_0, q_{accept}, q_{reject})$ deciding a language $L$, running in time at most $p(n)$ on inputs of length $n$ (a polynomial bound guaranteed by $L \in \mathrm{NP}$). Fix input $w$ with $|w| = n$. We build a table with $p(n)$ rows (steps $0$ through $p(n)-1$) and $p(n)$ columns (tape cells $0$ through $p(n)-1$ — the machine cannot reach farther in $p(n)$ steps). Each cell of the tableau holds one symbol from the alphabet

where a plain symbol means "just tape content here," and a pair $(q, a)$ means "the head is here, machine is in state $q$, and the tape cell holds $a$." Row $0$ is fixed to encode the start configuration: $w$ written out, blank symbols filling the rest, and the head/state marker at the left end in state $q_0$. For each cell $(i,j)$ and each symbol $s \in C$, introduce a Boolean variable

There are $p(n)^2 \cdot |C|$ such variables — polynomial in $n$, since both $p(n)$ and $|C|$ are fixed/polynomial quantities independent of the input's specific content.

The four clause groups

The formula is a conjunction $\phi_{N,w} = \phi_{cell} \wedge \phi_{start} \wedge \phi_{move} \wedge \phi_{accept}$.

1. Cell clauses ($\phi_{cell}$). Every tableau cell holds exactly one symbol:

The first part forces at least one symbol per cell; the second forces at most one. Together, exactly one.

2. Start clauses ($\phi_{start}$). Row 0 must literally spell out the start configuration — one clause per column simply asserting $x_{0,j,s}$ for the correct symbol $s$ dictated by $w$ and the initial head/state marker. There is no choice here; these are unit clauses.

3. Accept clause ($\phi_{accept}$). Somewhere in the tableau, a cell must contain the accept state marker:

We do not need to know when acceptance occurs — only that it occurs somewhere in the grid, so a disjunction over all cells suffices. (If $N$ halts and accepts before step $p(n)-1$, we assume, WLOG, it simply stays in $q_{accept}$ for the remaining rows — a harmless padding convention.)

4. Transition clauses ($\phi_{move}$). This is the heart of the construction, enforcing that each row follows from the previous one by a legal move of $N$. The trick is locality: whether cell $(i,j)$'s value is consistent with row $i-1$ depends only on the $2\times 3$ window of cells directly above and around it — positions $(i-1,j-1), (i-1,j), (i-1,j+1)$ in the previous row and $(i,j-1),(i,j),(i,j+1)$ in the current row (with boundary handling at the tape edges). Because the head moves by at most one cell per step, any cell not adjacent to the head cannot change, and any cell adjacent to the head changes only according to $\delta$. For every $2\times3$ window position, enumerate the (finitely many, machine-dependent) combinations of six symbols that are legal — i.e., that could actually arise from applying some transition in $\delta$ (including the "no head here, nothing changes" case) — and forbid all windows that are not on this legal list:

Each such clause has at most 6 literals, and the number of illegal windows is a constant depending only on $|C|$ (hence only on $N$, not on $n$). ```pseudocode function COOK_LEVIN(N, w): n := length(w) p := polynomial time bound for N # from NP definition C := Gamma ∪ (Q × Gamma) # tableau alphabet

# 1. Create variables for i in 0..p(n)-1: for j in 0..p(n)-1: for s in C: create boolean variable x[i][j][s] phi_cell := TRUE for i, j: phi_cell &= AT_LEAST_ONE(x[i][j][]) phi_cell &= AT_MOST_ONE(x[i][j][]) # pairwise negated conjunctions phi_start := TRUE for j in 0..p(n)-1: s := start_symbol_at_position(w, j) # from w, blanks, head marker at j=0 phi_start &= x[0][j][s] # unit clause: forces the value phi_accept := OR over all i, j, a in Gamma of x[i][j][(q_accept, a)] phi_move := TRUE for i in 1..p(n)-1: for j in 0..p(n)-1: window_vars := neighbors_2x3(i, j) # 6 cell positions, boundary-aware for combo in ALL_ASSIGNMENTS(window_vars, C): if not LEGAL_WINDOW(combo, delta): phi_move &= NOT(AND of the 6 literals in combo) return phi_cell AND phi_start AND phi_move AND phi_accept ```

Why satisfiability captures acceptance

Read the formula as a conjunction of independent requirements: $\phi_{cell}$ makes any satisfying assignment describe an actual grid of symbols; $\phi_{start}$ pins row 0 to the true starting configuration; $\phi_{move}$ pins every subsequent row to be reachable from the one above by some legal transition (nondeterminism is exactly the freedom to choose which legal window appears at the active cell — the formula doesn't force a specific choice, only a legal one); $\phi_{accept}$ demands that an accepting marker appear somewhere. A satisfying assignment is therefore exactly an encoding of a legal computation history of $N$ on $w$ that reaches $q_{accept}$ — i.e., an accepting branch. Conversely, every accepting branch of $N$ on $w$ literally is such a tableau, and setting the variables accordingly satisfies every clause. This is the two-way correspondence the theorem needs.

Size of the formula. Let $p(n)$ be the time bound. The tableau has $p(n)^2$ cells, each with $|C|$ variables, giving $O(p(n)^2)$ variables (constant $|C|$ absorbed into the big-$O$, since it depends only on $N$, not on $n$). The clause count:

• $\phi_{cell}$: $O(p(n)^2)$ cells, each contributing $O(|C|^2)$ clauses (pairwise exclusions) — total $O(p(n)^2)$.
• $\phi_{start}$: $p(n)$ unit clauses.
• $\phi_{accept}$: one clause of size $O(p(n)^2)$.
• $\phi_{move}$: $O(p(n)^2)$ window positions, each contributing $O(|C|^6)$ clauses (all illegal 6-tuples over a constant alphabet) — total $O(p(n)^2)$.

Altogether, $\phi_{N,w}$ has $O(p(n)^2)$ variables and $O(p(n)^2)$ clauses, each of constant length (at most 6 literals per clause, ignoring the accept clause and the "at least one" cell clauses, which have length $|C|$, still constant). The whole formula has size polynomial in $n$. This is the crux: nondeterminism in the machine becomes plain unforced disjunction in the formula — we never had to enumerate the exponentially many nondeterministic branches, only the polynomially many tableau positions.

Time to build the formula. Writing down all variables and clauses is a direct enumeration over $i, j$ (and small constant-size local combinations), so the reduction itself runs in time polynomial in $n$ — in fact $O(p(n)^2)$ up to alphabet-dependent constants, comfortably polynomial. This satisfies the requirement of a Karp (polynomial-time, many-one) reduction.

Correctness (the actual proof). We must show $N$ accepts $w$ iff $\phi_{N,w}$ is satisfiable. ($\Rightarrow$) Suppose $N$ accepts $w$. Then there is some sequence of nondeterministic choices leading to an accepting configuration within $p(n)$ steps (padding with idle steps in $q_{accept}$ if it halts early). This accepting run defines, row by row, an actual tableau: row $i$ is the machine's configuration after $i$ steps. Assign $x_{i,j,s} = \text{true}$ exactly when the tableau's cell $(i,j)$ is symbol $s$. Every clause is satisfied: $\phi_{cell}$ holds because each cell has one true symbol; $\phi_{start}$ holds because row 0 is the genuine start configuration; $\phi_{move}$ holds because consecutive rows of a real run are, by definition, related by legal windows (this is precisely what "the machine executed a transition" means locally); $\phi_{accept}$ holds because some cell holds $q_{accept}$. ($\Leftarrow$) Suppose $\phi_{N,w}$ is satisfiable. Take a satisfying assignment. By $\phi_{cell}$, it defines an unambiguous grid of symbols — a genuine table, one symbol per cell. By $\phi_{start}$, row 0 equals the true start configuration. By $\phi_{move}$, every $2\times 3$ window matches a window realizable by some transition of $\delta$ — meaning row $i$ is obtainable from row $i-1$ by applying $\delta$ at the (unique, since only one cell has a head marker per row — a fact itself enforceable/derivable from the window constraints) active head position. Inductively, then, the whole tableau is a legitimate computation history of $N$ starting from $w$. By $\phi_{accept}$, this history reaches $q_{accept}$. Hence $N$ has an accepting computation on $w$, i.e., $N$ accepts $w$. This biconditional is exactly the definition of a valid reduction from $L(N)$ to SAT. Since $N$ was an arbitrary polynomial-time NTM deciding an arbitrary $L \in \mathrm{NP}$, every language in NP reduces to SAT in polynomial time. Combined with SAT $\in$ NP (trivial verification), SAT is NP-complete. $\blacksquare$

Honest tradeoffs. The construction is a worst-case theoretical reduction: the formulas it produces are enormous (though polynomial) and not meant to be solved directly by this route in practice — real SAT solvers work on formulas arising from application domains (hardware verification, scheduling) that are far more structured. Also, the Cook-Levin proof does not, by itself, say anything about whether SAT (hence NP) has a polynomial-time algorithm; it only establishes SAT's maximal difficulty within NP relative to polynomial-time reductions, leaving the P vs. NP question entirely open.

To make the abstract tableau concrete, trace a tiny (contrived but illustrative) NTM $N$ that decides whether a binary string contains the substring `11`, using nondeterminism to "guess" the starting position of the match, on input $w = 010$ ($n = 3$). Assume a time bound $p(n) = 4$ suffices (guess a position, check two cells, accept/reject — small constant overhead). The tableau is $4 \times 4$. One nondeterministic branch: guess "match starts at position 1" (0-indexed), check tape[1] and tape[2].

This particular branch's tableau would satisfy $\phi_{cell}, \phi_{start}, \phi_{move}$ but fails $\phi_{accept}$ — it never contains a $q_{accept}$ marker, so this specific tableau does not by itself witness satisfiability. But $\phi_{N,w}$ doesn't ask for this branch to accept; it asks whether some assignment to all the tableau variables (i.e., some branch, since nondeterministic choices are exactly what's unconstrained beyond legality) reaches accept. Trying the branch that guesses "match starts at position... " — wait, $w=010$ actually has no `11` substring at all, so every branch rejects, and correctly, $\phi_{N,010}$ should be unsatisfiable, matching $N$ rejecting $010$. Now contrast with $w' = 011$: the branch guessing a match starting at position 1 produces the tableau

Setting the variables to encode exactly this grid: $x_{0,0,(q_0,0)}=1$, $x_{0,1,1}=1$, $x_{0,2,1}=1$, $x_{0,3,\_}=1$, and so on through row 3 with $x_{3,3,(q_{accept},\_)} = 1$, all other $x_{i,j,s}$ for this cell set false — this assignment satisfies $\phi_{cell}$ (one symbol/cell), $\phi_{start}$ (row 0 matches $w'$), $\phi_{move}$ (each consecutive pair of rows is a legal $\delta$-window: e.g., row 0→1 is the "move right, enter $q_1$" window; nothing outside the head's neighborhood changes, satisfying the "unchanged" legal windows elsewhere), and $\phi_{accept}$ (cell $(3,3)$ holds $q_{accept}$). Hence $\phi_{N,011}$ is satisfiable — matching $N$ accepting $011$, which does contain `11`. This end-to-end correspondence, scaled up to arbitrary $N$ and $w$, is exactly the content of the theorem.

From SAT to 3-SAT

The clauses above are not automatically in 3-CNF: cell clauses can have length $|C|$ (constant, but maybe $> 3$), and window clauses can have up to 6 literals. The standard fix converts any clause into an equivalent conjunction of 3-literal clauses by introducing fresh auxiliary variables, preserving satisfiability: For a clause $(\ell_1 \vee \ell_2 \vee \cdots \vee \ell_k)$ with $k > 3$, introduce new variables $y_1, \dots, y_{k-3}$ and replace it with

Why this preserves satisfiability. If the original clause is true because some $\ell_i$ is true, set $y_1 = \cdots = y_{i-2} = \text{true}$ (propagating "satisfied so far" forward) and $y_{i-1} = \cdots = y_{k-3} = \text{false}$; every new clause is then satisfied — either by the surviving literal or by the chosen truth value of a $y$. Conversely, if every $y$-assignment fails to make some original literal true, the chain of implications forces a contradiction, so some $\ell_i$ must be true for the chain to be satisfiable. Each original clause of length $k$ becomes $k-2$ clauses of length exactly 3, adding $k-3$ variables — still a polynomial blow-up overall, since $k \le \max(|C|, 6)$ is a constant here. Applying this uniformly to every clause of $\phi_{N,w}$ yields an equisatisfiable 3-CNF formula of polynomial size, proving 3-SAT is also NP-complete.

The Cook-Levin Theorem is the load-bearing wall of complexity theory: every NP-hardness proof in existence — for scheduling, packing, graph problems, logic puzzles, cryptographic assumptions — ultimately traces back, through a chain of reductions, to this single simulation-to-formula argument. Modern industrial SAT solvers (used in hardware verification, software model checking, and AI planning) exist because engineers accepted that SAT is "the" canonical hard problem and built enormously optimized heuristic solvers for it, benefiting every problem reducible to SAT. Automated theorem provers and constraint solvers (SMT solvers like Z3) build directly atop SAT technology, layering richer theories over the Boolean core the theorem establishes as universal. In practice, when a company's scheduling or verification tool encodes its problem "as a SAT instance," it is literally invoking the Cook-Levin correspondence between combinatorial structure and formula satisfiability. Understanding this proof is also the standard gateway to the reduction toolkit used to classify problems like Classic NP-Complete Problems: Clique and Vertex Cover and Hamiltonian Path and Circuit Problems, both of which are shown hard via polynomial-time reductions from 3-SAT rather than by repeating the tableau construction.

Ask the tutor: How does the clause-splitting gadget for 3-SAT actually preserve satisfiability in both directions — can you walk through why forcing a failure in the chain forces some original literal true?