Every problem whose answer you can check fast is a Boolean formula in disguise. Cook (1971) and, independently, Levin (1973) proved SAT is NP-complete: they showed how to compile the running of a verifier into one giant AND-of-ORs that is satisfiable exactly when the verifier would accept some certificate. Down the center a tiny verifier's computation is compiled to CNF live — feed an input in, the clauses come out, and the formula is SAT iff the machine accepts. The blue team builds the encoding; the red team rips out its wiring.
source S. A. Cook, "The Complexity of Theorem-Proving Procedures," Proc. 3rd ACM STOC (1971) 151–158 — doi:10.1145/800157.805047. L. A. Levin, "Universal Sequential Search Problems," Problemy Peredachi Informatsii 9(3) (1973) no stable link. Rendered, not quoted.
The encoding is not asserted — it is built, gate by gate. Each wire of the verifier becomes a variable, and a fixed packet of clauses forces that variable to equal its gate's output. These are the consistency (transition) clauses: they pin every wire to a legal value, so the only satisfying assignments are real computations.
Tseitin templates (g is the gate's output variable):
¬a → (g∨a)(¬g∨¬a) a∧b → (¬g∨a)(¬g∨b)(g∨¬a∨¬b) a∨b → (g∨¬a)(g∨¬b)(¬g∨a∨b). One final unit clause (gout) demands the machine accept.
| current x | count |
|---|
Before 1971 "hard" had no anchor. Cook — and independently Levin, behind the Iron Curtain — pinned it: every language with a polynomial-time verifier reduces to SAT by exactly this construction. SAT is the universal target.
That single fact is what the-p-vs-np question hangs on — is this one universal problem in P? — and it is the root every the-karp-reduction (1972) extends outward: clique, vertex-cover, Hamiltonian-cycle all inherit hardness through SAT. Each sphere is the next one's premise.
The blue team's live check: re-run the compiler over all four inputs and confirm SAT ⇔ ACCEPT, both directions. If red rips out the consistency clauses, a rejected input goes spuriously SAT and this badge turns red.
A verifier M reads an input x and guesses a certificate w ∈ {0,1}². It accepts iff a fixed poly-time check C(x,w) passes — that is exactly what "in NP" means: a short proof you can verify fast.
"Exactly one of w0,w1 is set, and each x-bit that is 0 forces its own w-bit on." What you feed the panel is the input x; the certificate is what the compiled formula hands back.
The verifier is compiled fresh for the chosen x; the formula is solved by exhaustive search over every assignment — never looked up.
the compiled formula φx, clause by clause:
What the machine proves: over all four inputs the compiled CNF is satisfiable exactly when the verifier accepts some certificate — and every satisfying assignment is an accepting computation (the consistency clauses forbid fakes). SAT is in NP; SAT is NP-hard; therefore SAT is NP-complete.
| input x | machine | φx | ⇔ |
|---|
The blue team's witness (left) confirms this equivalence live; the red team (right) tries to snap it.
That generality is real but is asserted here, not exhausted — no finite panel ranges over all of NP. And NP-completeness is a statement of relative hardness: it does not, by itself, prove SAT needs exponential time.
"Cook–Levin proves SAT is unsolvable." Cut. It proves SAT is as hard as all of NP; whether that is easy (P=NP) is open. Undecidable ≠ NP-complete.
"Cook and Levin wrote it together." Cut. Independent: Cook 1971 (Toronto), Levin 1973 (Moscow), different formalisms; the joint name is retroactive.
"NP-complete means exponential time." Cut. No sub-exponential lower bound is proven; the hardness is relative to NP, not an absolute clock.
"3-SAT is the same theorem." Kept, corrected. 3-SAT is a Karp corollary — clause-splitting one step past Cook–Levin.
The red team's move: rip out the consistency clauses and keep only the final (gout) that demands "accept." Now nothing forces the wires to compute anything.
With the wiring gone, the solver just sets the accept-bit true: the CNF turns satisfiable for every input, including x=00 which the verifier rejects. SAT ⇔ ACCEPT snaps, and the witness (window 7) catches it. Nothing is faked; the attack is real.