Cook–Levin Theorem¶
The theorem that Boolean satisfiability is NP-complete because every NP decision problem has a polynomial-time truth-preserving reduction to SAT.
Core Idea¶
The Cook–Levin theorem says that Boolean satisfiability (SAT) is NP-complete. SAT is in NP because a proposed satisfying assignment is efficiently checked. Every NP decision language can also be transformed in deterministic polynomial time into a Boolean formula that is satisfiable if and only if the original instance is a yes-instance. The standard proof encodes a bounded accepting computation as Boolean choices constrained by valid start, transition and acceptance rules.[^ref-58b4a5f5d06f]
Scope of Application¶
The theorem supplies the starting NP-complete problem for later hardness proofs. Showing that another decision problem is NP-complete still requires its own polynomial reduction from an already-hard problem and proof of membership in NP. Related stepwise SAT encodings appear in bounded verification or planning, but an encoding of one application is not itself the universal theorem.[^ref-58b4a5f5d06f]
Clarity¶
The reduction does not find a witness. MIT's six-step tableau shows state \(A\), tape \(000000\) at time 0 and halting state \(H\), tape \(011110\) at time 6; variables stand for each bounded row's tape, head and state. In Cook's original construction, a clause \((\neg S_{i,t}\lor\neg S_{j,t})\) for \(i\ne j\) is false if two head positions are simultaneously chosen, so it executes one local consistency rule. Many such constraints plus start and acceptance conditions yield a formula satisfiable iff a valid accepting run exists. The single tableau and clause illustrate, but do not alone prove, universality.[ref-58b4a5f5d06f][ref-43c11047560e]
Manages Complexity¶
Many different NP problems can be compared through a common SAT target. If SAT were solvable in polynomial time, every NP decision problem would be, yielding \(P=NP\). Cook–Levin neither supplies that algorithm nor proves \(P\ne NP\). Cook's 1971 theorem statement used a tautology/oracle formulation, but its proof also explicitly constructed an accepting-iff-satisfiable CNF \(A(w)\); the present SAT/many-one sentence is the standard modern framing.[ref-43c11047560e][ref-58b4a5f5d06f]
Abstract Reasoning¶
State the source decision language and polynomial witness/verification bound. Define a deterministic polynomial transformation to a formula, and prove that yes-instances map exactly to satisfiable formulas. Establish SAT membership separately. For a later completeness proof, check the reduction direction: the known hard problem must reduce to the proposed new target.[^ref-58b4a5f5d06f]
Knowledge Transfer¶
The idea of encoding bounded global behavior through local Boolean constraints can guide other formal models, but a single model encoding lacks the theorem's universal claim. NP-completeness and polynomial reduction are concepts used in the theorem rather than aliases for it; the accepted broad theorem genus does not make either concept a second strict parent.
[^ref-43c11047560e]: Cook's original 1971 paper hosted by its author. [^ref-58b4a5f5d06f]: MIT OpenCourseWare, modern Cook–Levin tableau exposition.
Relationships to Other Abstractions¶
Current abstraction Cook–Levin Theorem Domain-specific
Parents (1) — more general patterns this builds on
-
Cook–Levin Theorem is a kind of Formal theorem Domain-specific
Cook–Levin is a proved formal theorem about SAT membership and NP-hardness under polynomial reductions.
Hierarchy paths (2) — routes to 2 parentless roots
- Cook–Levin Theorem → Formal theorem → Formal System → Formalization → Representation → Abstraction
- Cook–Levin Theorem → Formal theorem → Formal System → Formalization → Transformation → Function (Mapping)
Neighborhood in Abstraction Space¶
Cook–Levin Theorem sits in a sparse region of the domain-specific corpus (86th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.
Family — Computational Complexity & Hardness (17 abstractions)
Nearest neighbors
- NTIME — 0.83
- Pseudo-polynomial transformation — 0.82
- Nonelementary Problem — 0.82
- P versus NP Problem — 0.81
- Complexity Class — 0.81
Computed from structural-signature embeddings · 2026-10-08