1971 Canada NP-complete

The Complexity of Theorem-Proving Procedures

Stephen Cook, 1971 — Boolean satisfiability is the canonical hard problem. Every NP problem reduces to it. The bottleneck has a name.

Stephen Cook, at the University of Toronto, defined polynomial-time reduction and proved that the Boolean satisfiability problem (SAT) — given a Boolean formula, decide whether there exists an assignment of true/false values to its variables that makes the formula true — is NP-complete. The proof showed that any non-deterministic Turing machine running in polynomial time can be encoded as a SAT instance whose satisfying assignment corresponds to an accepting computation. This established the existence of a single problem to which every problem in NP can be reduced in polynomial time. Leonid Levin proved the same result independently in the Soviet Union in 1973, and the result is now known as the Cook–Levin theorem. Every later NP-hardness proof in this book — for test suite minimization, package dependency resolution, module clustering, register allocation — descends from Cook 1971.

In plain terms

Edmonds drew the line between polynomial and exponential. Cook found the bottleneck. A reduction is a translation. If I can take any instance of problem A and quickly translate it into an instance of problem B, such that solving B gives me the answer to A, then B is at least as hard as A. Cook's insight was that every problem in NP — every problem whose solution can be checked in polynomial time — can be translated, in polynomial time, into a Boolean satisfiability instance. Every one. Test suite minimization. Package dependency resolution. Optimal register allocation. All of them, when you strip the domain language, are SAT problems wearing different hats. This is why the book uses NP-completeness as a unit of measurement. Saying "module clustering is NP-hard" is shorthand for: there is a polynomial-time translation from SAT to module clustering, so a fast solver for module clustering would give us a fast solver for SAT, and a fast solver for SAT would give us a fast solver for every problem in NP. We do not believe such a solver exists. Fifty-five years of trying have produced nothing. The practical consequence is everywhere. When apt or dnf resolves your package dependencies, it is running a SAT solver, because Di Cosmo's reduction (chapter eight) shows the dependency problem is NP-complete. When a static analyzer asks whether a piece of code can ever reach a certain state, it reduces the question to SAT. When a compiler decides which variables get to live in registers, it is solving an instance of a problem reducible to SAT. When a model checker verifies that a hardware circuit meets its specification, same. The world's hardest problems all turn out to be the same problem in different costumes, and that one problem is SAT. One problem. Every other hard problem reduces to it. The bottleneck has a name.