How Did the Cook-Levin Theorem Prove SAT Is NP-Complete?

The Cook-Levin theorem, proved independently by Stephen Cook in 1971 and Leonid Levin in 1973, established that the Boolean satisfiability problem, known as SAT, is NP-complete. Before this result, computer scientists knew many problems belonged to the class NP, meaning their solutions could be verified quickly, but they had no way to prove that a single problem captured the hardest possible cases in that class. By showing that any problem solvable by a nondeterministic Turing machine in polynomial time can be translated into a Boolean formula, the theorem created the foundation for modern computational complexity theory.

Understanding NP and NP-Completeness

In classical computing, the complexity class \(\text{NP}\) consists of decision problems for which a proposed solution can be verified by a deterministic Turing machine in polynomial time. Equivalently, \(\text{NP}\) is the set of problems solvable by a nondeterministic Turing machine in polynomial time, meaning the machine can explore multiple computational paths simultaneously and accept if at least one path reaches an accepting state within \(p(n)\) steps for an input of size \(n\).

A problem \(L\) is \(\text{NP}\)-complete if it satisfies two conditions:

  1. \(L \in \text{NP}\).
  2. \(L\) is \(\text{NP}\)-hard, meaning every problem \(A \in \text{NP}\) can be reduced to \(L\) in polynomial time (written \(A \le_p L\)).

Proving that SAT is in \(\text{NP}\) is straightforward: given a Boolean formula \(\phi\) and a truth assignment to its variables, a deterministic algorithm can evaluate \(\phi\) in polynomial time to check whether it outputs true. The breakthrough of the Cook-Levin theorem was proving the second condition—that every problem in \(\text{NP}\) reduces to SAT.

Encoding a Turing Machine Computation

To show that any language \(A \in \text{NP}\) reduces to SAT, the Cook-Levin proof constructs a polynomial-time reduction that takes an arbitrary input string \(w\) of length \(n\) and produces a Boolean formula \(\phi_{M,w}\) such that \(w \in A\) if and only if \(\phi_{M,w}\) is satisfiable. Here, \(M\) is a nondeterministic Turing machine that decides \(A\) in at most \(p(n)\) steps, where \(p(n)\) is a polynomial.

Because \(M\) runs for at most \(p(n)\) steps, its tape head can visit at most \(p(n)\) tape cells. We can therefore represent the entire computation of \(M\) on input \(w\) as a two-dimensional grid, called a tableau, of size \(p(n) \times p(n)\). Each row \(i\) (from \(0\) to \(p(n) - 1\)) represents the configuration of \(M\) at time step \(i\), and each column \(j\) (from \(0\) to \(p(n) - 1\)) represents tape cell \(j\).

Building the Boolean Formula

The formula \(\phi_{M,w}\) uses Boolean variables to describe the contents of every cell in the tableau. Specifically, for each row \(i\), column \(j\), and symbol \(s\) (which can be a tape symbol, a blank, or a state-symbol pair indicating the head's position and current state), we define a variable \(x_{i,j,s}\) that is true if and only if cell \((i, j)\) contains \(s\).

The formula \(\phi_{M,w}\) is a conjunction of four subformulas:

\[\phi_{M,w} = \phi_{\text{cell}} \land \phi_{\text{start}} \land \phi_{\text{move}} \land \phi_{\text{accept}}\]

Each part enforces a specific rule of a valid computation:

  • \(\phi_{\text{cell}}\): Ensures that every cell \((i, j)\) in the tableau contains exactly one symbol.
  • \(\phi_{\text{start}}\): Forces row \(0\) to match the initial configuration of \(M\) on input \(w\), with the tape head at cell \(0\) in the start state \(q_0\), followed by the symbols of \(w\) and blanks.
  • \(\phi_{\text{move}}\): Guarantees that every row \(i+1\) follows legally from row \(i\) according to the transition function of \(M\). Because a Turing machine only modifies the cell under its head and moves one step left or right, each \(2 \times 3\) window of cells between rows \(i\) and \(i+1\) must match a valid local transition.
  • \(\phi_{\text{accept}}\): Requires that the accepting state \(q_{\text{accept}}\) appears somewhere in the tableau.

Why the Reduction Works

If \(M\) accepts \(w\), there exists a valid sequence of configurations ending in \(q_{\text{accept}}\), which directly gives a truth assignment that satisfies all four parts of \(\phi_{M,w}\). Conversely, any satisfying assignment to \(\phi_{M,w}\) forces the variables to describe a valid, accepting computation of \(M\) on \(w\).

Crucially, the size of the tableau is \(O(p(n)^2)\), and the number of variables and clauses in \(\phi_{M,w}\) is polynomial in \(n\). Constructing \(\phi_{M,w}\) also takes polynomial time. Thus, \(A \le_p \text{SAT}\) holds for every \(A \in \text{NP}\), proving that SAT is \(\text{NP}\)-complete.

Impact on Complexity Theory

Once SAT was established as \(\text{NP}\)-complete, proving other problems \(\text{NP}\)-complete became much easier. Instead of encoding Turing machine tableaus from scratch, researchers only needed to show a polynomial-time reduction from SAT—or from any already known \(\text{NP}\)-complete problem—to the new problem. This chain of reductions, famously expanded by Richard Karp in 1972 to 21 classic problems including 3-SAT, Clique, and Hamiltonian Cycle, established \(\text{NP}\)-completeness as a central concept in computer science.