Section 4.4 left an open problem: the definition of NP-completeness requires a reduction from every problem in NP, a requirement no proof can satisfy directly problem by problem — and transitivity only makes it practicable if a known NP-complete problem already exists to start from. The Cook–Levin theorem (1971; independently, Levin around the same time) is exactly that starting point: it proves that SAT (satisfiability of Boolean formulas, not necessarily given in conjunctive normal form) is NP-complete, and it is the only result in this whole story proved from the raw definition, without relying on any earlier reduction.
$\text{SAT} \in NP$ is the easy part (Section 1.3: certificate = assignment, verification = evaluate the formula, linear time). The substantial part is showing that every $L \in NP$ satisfies $L \le_p \text{SAT}$. The idea, at a level that makes its structure visible without developing the construction all the way (it is a project of its own, deliberately out of scope here — see the scope note in 5.3):
The result — $f(x) = \varphi_x$ — is, in every respect, a polynomial many-one reduction in the sense of Section 3, with $A = L$ and $B = \text{SAT}$. The difference from every other reduction in this project is what is being reduced: not one concrete combinatorial problem to another, but the entire notion of verifiable computation (any $L \in NP$, via its generic verifier $V$) to a single syntactic structure (a propositional formula). It is the only bridge between the definitional world (verifiers, Turing machines) and the combinatorial world (clauses, graphs, sets) in which every subsequent reduction lives — including the one used as this project’s foundation.
Cook–Levin, in its classical form, produces general SAT — formulas with clauses of arbitrary width. The root problem chosen for this project is 3-SAT (clauses of width exactly 3), which requires one additional step — but of a completely different nature from the previous one: $\text{SAT} \le_p \text{3-SAT}$ is proved with a purely syntactic transformation, touching no computational semantics at all. Every wide clause is split into a chain of 3-literal clauses by introducing auxiliary variables ($(l_1 \lor l_2 \lor l_3 \lor l_4)$ becomes $(l_1 \lor l_2 \lor z) \land (\lnot z \lor l_3 \lor l_4)$, and so on for longer clauses), and clauses that are too short are padded by duplicating a literal. The transformation preserves satisfiability clause by clause and is evidently polynomial.
It is worth noting the contrast explicitly: $\text{SAT} \le_p \text{3-SAT}$ is mechanical, almost administrative — it normalizes one syntactic form into another. Cook–Levin ($L \le_p \text{SAT}$ for every $L \in NP$) is the only reduction in the entire chain that creates difficulty out of nothing, in the sense that it compiles an entire model of computation into combinatorial structure. Every subsequent reduction in this project (Section 6) resembles the second category more than the first in spirit — it moves difficulty that already exists from one combinatorial structure to another, never having to “invent” difficulty from scratch — but this still requires domain-specific structural insight, unlike the purely syntactic transformation just described.
Taken together, Cook–Levin and $\text{SAT} \le_p \text{3-SAT}$ fix a single anchoring fact: 3-SAT is NP-complete. From this point on, every new NP-completeness proof always follows the same two-step recipe (it mirrors exactly the definition in 4.4):
In practice, nobody after Cook and Levin has ever again had to repeat step 2 in its general form (“reduce from every $L \in NP$”): one picks as $A_0$ the already-known problem whose structure most resembles that of the new target — which is why recognizable “families” of reductions exist (graph problems reducing to other graph problems, numeric problems encoding the bits of a formula, and so on), rather than an arbitrary, disconnected collection.
Explicit scope note: this project cites the Cook–Levin theorem as an established fact (Section 5.1 describes its structure, without implementing it) and assumes that 3-SAT is NP-complete as a starting point — it does not prove this constructively in code. Building the Turing-machine-to-CNF compiler described in 5.1 is a separate project (a possible future extension, not a gap in this one). What this project does concretely is everything that comes after that anchoring: the reduction chain $\text{3-SAT} \le_p \text{Independent Set} \le_p \text{Vertex Cover}$ (with Clique nearly free via complementation) plus the branch $\text{3-SAT} \le_p \text{Subset Sum}$, each verified end-to-end against a real SAT solver used as the ground-truth oracle for 3-SAT instances.
With the anchor to 3-SAT established, every reduction function $f$ written in this project’s code is, literally, the concrete witness of one step of the recipe in 5.3: not an isolated exercise, but a link that inherits — by transitivity — the NP-completeness of the entire chain built up to that point.
The distinction already anticipated in 1.6 must be kept in mind, between what the mathematics guarantees and what the code verifies empirically:
This distinction — a written proof for the universal statement, an executable check for the sample — is the thread that connects this report’s theory to the code’s architecture, the subject of the final section.
| ← Previous: 4. What Reductions Are For | README | Next: 6. Pipeline Architecture → |