We have a class, \mathsf{NP}, holding thousands of problems that all share the "easy to check, seemingly hard to solve" flavour. A natural suspicion forms: maybe they are hard for the same underlying reason — maybe there is one problem so central that solving it fast would solve every one of them fast. In 1971 Stephen Cook (and independently Leonid Levin) proved exactly that, and named the culprit: Boolean satisfiability, SAT.

The Cook–Levin theorem is the founding result of NP-completeness. It shows that SAT is a universal \mathsf{NP} problem — every other problem in the class quietly reduces to it. It is the bedrock every later reduction stands on.

Two definitions: NP-hard and NP-complete

Before the theorem we need the vocabulary of "hardest problems in a class", built from polynomial-time mapping reductions. Write A \le_p B ("A reduces to B") when there is a polynomial-time function mapping every instance of A to an instance of B with the same yes/no answer. Intuitively: "if I could solve B, I could solve A", so B is at least as hard as A.

This is a wonderful lever. To show \mathsf{P} = \mathsf{NP} you would only need one fast algorithm for one NP-complete problem. And to believe a problem is intractable, showing it NP-complete is the strongest practical evidence we have.

The theorem

The hard part is the word every. Membership (\text{SAT} \in \mathsf{NP}) is the easy half — a satisfying assignment is a certificate, checked in linear time. The genius is the NP-hardness: a single construction that works for all \mathsf{NP} problems at once, whatever they happen to be about.

The proof idea: a computation is a formula

Here is the trick that makes universality possible. Any problem A \in \mathsf{NP} has, by definition, a nondeterministic Turing machine M that decides it in p(n) steps. We don't need to know what M computes — only that its run is a mechanical, local process. So we build a Boolean formula \Phi_x that is satisfiable exactly when M has an accepting computation on input x. A satisfying assignment is an accepting run.

Picture the computation as a tableau: a grid with one row per time step and one column per tape cell. In a p(n)-step computation the head never travels further than p(n) cells, so the grid is (p(n)+1) \times p(n) — polynomial in size. Each cell records what is written there, whether the head is present, and (if so) the machine's state.

Now introduce Boolean variables for the contents of every cell — one bunch of variables per grid square, encoding its symbol/head/state. The whole formula \Phi_x is a conjunction of four kinds of clauses, each purely local:

Each family has only polynomially many clauses, each of constant size, and the map from x to \Phi_x is computable in polynomial time. And \Phi_x is satisfiable \iff a legal accepting tableau exists \iff M accepts x \iff x \in A. That is a reduction from an arbitrary A to SAT — so SAT is NP-hard.

Why locality is the whole game

The reason a global fact ("this is a valid computation of a complex machine") can be pinned down by a pile of tiny, independent clauses is that computation is local. Between one step and the next, almost nothing changes: only the cell under the head, and its immediate neighbours, can be affected. So "row t+1 legally follows row t" is really just "every little window is legal" — a conjunction of local constraints. Boolean formulas are built for exactly this: expressing a big AND of small local conditions. That correspondence, computation ↔ formula, is the engine of the entire theory.