= Solution
The <Cook-Levin theorem> states that the <Boolean satisfiability problem> is <NP-complete> under <polynomial-time many-one reductions>. Membership in <NP> follows by guessing an assignment and evaluating the formula in time polynomial in its description length.
For hardness, let $L\in\mathrm{NP}$ have a deterministic polynomial-time verifier $M(x,y)$, with a polynomial witness-length bound. Use a fixed polynomial <certificate (complexity)> length: a short <certificate (complexity)> is encoded by its length followed by padded data, and the verifier checks this encoding. Pad the computation to exactly $T=T(|x|)$ steps, with accepting and rejecting states absorbing. Enlarge $T$ polynomially if necessary to cover input/witness initialization. A standard polynomial slowdown permits a single-tape <Turing machine>, so it suffices to handle that model.
Encode a tape cell by a fixed number of bits recording its alphabet symbol and either no head or the head's finite control state. Starting with one head, a cell's next label depends only on its own label and the two neighboring labels: a head can change the symbol where it sits and can enter only a neighbor. Each such finite local function has a constant-size <Boolean circuit>. The initial row fixes $x$, blanks and the starting head, leaving only the witness bits as <Boolean circuit> inputs. There are $O(T)$ relevant cells with blank margins beyond every possible head position, and $T$ updates. Repeating these local <Boolean circuits> produces a <Boolean circuit> $C_x(y)$ of size $O(T^2)$, with an output detecting an accepting head in the final row. The construction is computable in <polynomial time>. Induction on rows shows that every assignment to $y$ produces exactly the verifier's valid computation; invalid local encodings can be assigned arbitrary <Boolean circuit> behavior because they never arise from the valid initial row.
Convert this <Boolean circuit> to <conjunctive normal form> using a <Tseitin transformation>. Introduce one variable for each wire, and encode each gate output $z$ by:
|| Gate relation
|| <Clauses> imposing equivalence
| $z=x\wedge y$
| $(\neg z\vee x)\wedge(\neg z\vee y)\wedge(z\vee\neg x\vee\neg y)$
| $z=x\vee y$
| $(z\vee\neg x)\wedge(z\vee\neg y)\wedge(\neg z\vee x\vee y)$
| $z=\neg x$
| $(z\vee x)\wedge(\neg z\vee\neg x)$
Unit <clauses> fix constant sources and assert the final output. Each input assignment has exactly one extension to its gate values, so the resulting formula $F_x$ is satisfiable precisely when some witness makes $M(x,y)$ accept. It has $O(T^2)$ <clauses> of bounded length and is produced in <polynomial time>. Thus
$$
\boxed{x\in L\iff F_x\text{ is satisfiable},\qquad\mathrm{SAT}\text{ is NP-complete}}.
$$
This proof also gives hardness for <clauses> of at most three <literals>, without needing a separate satisfiability assumption.
Back to article page
