# Stephen Cook

> 1939– · Computer Scientist
>
> **Recorded contribution:** Cook's theorem — NP-completeness; Cook-Levin theorem; P vs NP framing

## How to use this dossier

Read for a causal chain, not a hero story: inherited problem → contribution → mechanism → downstream capability → limit. Then close the page and complete the reconstruction exercise from memory.

## 1. Historical orientation

Stephen Cook (born 1939) proved in 1971 that Boolean satisfiability is NP-complete, independently paralleled by Leonid Levin's work in the Soviet Union. Cook formalized polynomial-time reducibility and showed that every computation whose accepting path can be verified in polynomial time can be encoded as a Boolean formula. The result made P versus NP a central question: if SAT has a polynomial algorithm, every NP problem does. The theorem does not prove P differs from NP or that SAT always takes exponential time. Its transformative mechanism is representation—encode an arbitrary bounded computation as local consistency constraints.

## 2. The problem inherited

Complexity researchers lacked a natural problem representing the full difficulty of efficiently verifiable computation and a reduction framework for transferring that difficulty.

## 3. The central contribution

Cook proved SAT NP-complete by translating any polynomial-time nondeterministic computation into a polynomial-size Boolean formula satisfiable exactly when the machine accepts.

## 4. Reconstruct the mechanism

1. Arrange a bounded computation as a tableau recording time steps, tape cells, symbols, states, and head positions.
2. Create Boolean variables describing each possible local fact at each tableau position.
3. Add clauses enforcing one valid initial configuration, legal local transitions, consistency, and an accepting state.
4. Observe that a satisfying assignment corresponds to an accepting computation and the construction grows only polynomially.

## 5. What changed downstream

- NP-completeness became a foundational classification of computational problems.
- Karp and others rapidly transferred completeness to graphs, scheduling, optimization, and logic.
- SAT solving became a practical engine for hardware verification, planning, synthesis, and security analysis.

## 6. Attribution, limits, and uncertainty

- Levin independently obtained the foundational completeness result; the joint name Cook–Levin preserves this.
- NP-completeness concerns worst-case asymptotic decision complexity, not every instance or optimization heuristic.
- The theorem leaves P versus NP unresolved and says nothing by itself about approximation or parameterized tractability.

## 7. Reconstruction lab

Encode a three-step nondeterministic finite-machine computation as Boolean variables and clauses for exactly-one state and legal transitions. Solve it manually, map the assignment back to a trace, and count formula growth.

## 8. Evidence trail

- [The Complexity of Theorem-Proving Procedures](https://doi.org/10.1145/800157.805047) — ACM Symposium on Theory of Computing
- [Stephen Cook](https://www.cs.toronto.edu/~sacook/) — University of Toronto

---

*Research checked 2026-08-09. Dates, roles, and claims about living people are historical snapshots. Linked sources remain the authority; this dossier is original instructional synthesis.*