The Cook--Levin Theorem

Use as certificate a truth assignment $a\in \{0,1{\}}^n$ for the variables of $\phi$. Its length is $n$, so it is linearly bounded by the input size of $<mi\; mathvariant="normal">⌜</mi>\phi <mi\; mathvariant="normal">⌝</mi>$.

A deterministic verifier can evaluate $\phi$ under $a$ by traversing the parse tree of $\phi$ once. That takes time polynomial in $\mathrm{\mid }<mi\; mathvariant="normal">⌜</mi>\phi <mi\; mathvariant="normal">⌝</mi>\mathrm{\mid }$, and by [L1] it accepts exactly when $\phi$ is satisfiable. Therefore [L2] gives $SAT\in NP$.

A tableau cell either lies away from the head, in which case it stores only a tape symbol from $\mathrm{\Gamma }$, or it is the unique scanned cell of that row, in which case it must record both the scanned tape symbol and the current state, hence an element of $Q\times \mathrm{\Gamma }$. By [L1], these are the only possibilities.

Therefore every cell value lies in ${\mathrm{\Delta }}_N=\mathrm{\Gamma }\cup (Q\times \mathrm{\Gamma })$. Because the machine $N$ is fixed before any input is considered, both $Q$ and $\mathrm{\Gamma }$ are fixed finite sets, so $\mathrm{\mid }{\mathrm{\Delta }}_N\mathrm{\mid }=\mathrm{\mid }\mathrm{\Gamma }\mathrm{\mid }+\mathrm{\mid }Q\mathrm{\mid }\mathrm{\mid }\mathrm{\Gamma }\mathrm{\mid }$ is a constant independent of the input length.

If $T$ is an actual computation history, then its first row is the start configuration. Each pair of adjacent rows is either one legal transition or a repeated halting row, so every padded $2\times 3$ window is legal by [L2].

Conversely, assume the two bullet conditions in the statement hold. In particular, every local window is legal in the sense of [L2].

Fix adjacent rows $r$ and $r+1$. If row $r$ is already halting, [L2] forces row $r+1$ to repeat it exactly. Otherwise row $r$ has a unique head neighborhood, and the overlapping legal windows force every cell outside that neighborhood to stay unchanged while the local neighborhood realizes exactly one allowed transition of $N$. So row $r+1$ is either the same halting configuration or the one-step successor of row $r$.

Because the first row is correct and every later row follows the previous one in one of the two ways allowed by step 2.1, the whole tableau is a valid branch computation history in the sense of [L1]. Hence [L1] gives the converse implication.

Introduce a variable $X_{r,c,a}$ for each row $r$, column $c$, and symbol $a\in {\mathrm{\Delta }}_N$, intended to mean that cell $(r,c)$ carries $a$. By [L1], the number of choices for $a$ is a fixed constant, so the total number of such variables is $O(T^2)$.

For each cell, add one at-least-one clause ${\bigvee }_{a\in {\mathrm{\Delta }}_N}{X}_{r,c,a}$ and one pairwise-exclusion clause $\mathrm{\neg }{X}_{r,c,a}\vee \mathrm{\neg }{X}_{r,c,b}$ for each distinct pair $a\mathrm{\ne }b$. Because $\mathrm{\mid }{\mathrm{\Delta }}_N\mathrm{\mid }$ is constant by [L1], each cell contributes only constantly many literals and clauses.

There are $(T+1{)}^2$ cells, and step 2.1 attaches only constant-size data to each one. Therefore the full exactly-one-symbol family has size polynomial in $T$, hence polynomial in the input length once $T$ is polynomially bounded.

The start constraint fixes each cell of the first row to its predetermined initial symbol, so it contributes one constant-size literal condition per column and therefore $O(T)$ total size. The accept constraint is the disjunction over all cells that one of them carries an accepting-state tag, so it has $O(T^2)$ size.

For each adjacent-row position and each illegal $2\times 3$ pattern, add a clause forbidding that pattern. By [L1] and [L2], there are $O(T^2)$ window positions and only constantly many patterns to inspect at each position, each producing a constant-size clause.

Combining steps 1.1 and 1.2 shows that the start, accept, and transition families together have polynomial total size.

If an accepting bounded tableau exists, assign each variable $X_{r,c,a}$ the value $1$ exactly when the tableau places symbol $a$ in cell $(r,c)$. The tableau then satisfies ${\psi }_{\mathrm{c}\mathrm{e}\mathrm{l}\mathrm{l}}$ by construction, while [L2] and [L3] show that it also satisfies ${\psi }_{\mathrm{s}\mathrm{t}\mathrm{a}\mathrm{r}\mathrm{t}}$, ${\psi }_{\mathrm{m}\mathrm{o}\mathrm{v}\mathrm{e}}$, and ${\psi }_{\mathrm{a}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{p}\mathrm{t}}$. Hence ${\psi }_{N,w}$ is satisfiable.

Conversely, suppose ${\psi }_{N,w}$ is satisfiable. By [L1], the satisfying assignment determines one symbol in every tableau cell.

The tableau extracted in step 1.2 satisfies the required start, accept, and local transition conditions by [L2]. Therefore [L3] turns it into a genuine branch computation history for $N$ on $w$, with later rows allowed to repeat once a halting configuration has appeared, and the accept part of [L2] makes that history accepting.

Steps 1.1 and 2.1 prove both implication directions, so ${\psi }_{N,w}$ is satisfiable exactly when an accepting bounded tableau exists.

On an input $w$ of length $n$, [L3] gives a tableau side length $T+1$ with $T\le p(n)$. A deterministic transducer can loop over all cells, all alphabet symbols, and all local windows in lexicographic order and print the corresponding clauses of ${\psi }_{N,w}$.

By [L1] and [L2], the number of printed variables and clauses is polynomial in $T$, hence polynomial in $n$ because $T\le p(n)$. Each loop iteration performs only constant-size bookkeeping for the fixed machine $N$.

Therefore the transducer from step 1.1 halts after polynomially many steps and outputs ${\psi }_{N,w}$. So the Cook-Levin map $w\mapsto {\psi }_{N,w}$ is polynomial-time computable.

By [L1], $SAT$ is in $NP$. To prove NP-completeness via [L4], it remains to prove NP-hardness.

Because $L\in NP$, [L2] supplies a nondeterministic polynomial-time machine $N$ deciding $L$. For an input $x$, let $f(x)$ be the Cook-Levin formula ${\psi }_{N,x}$ for a polynomial bound on computations of $N$ on $x$.

By [L3], the formula $f(x)$ is satisfiable exactly when $N$ has an accepting bounded tableau on $x$; with the bounded-tableau convention that later rows may repeat a halting configuration, this happens exactly when $x\in L$. The same citation shows that $f$ is computable in polynomial time. Therefore $L{\le }_{p}SAT$.

Since $L\in NP$ was arbitrary, step 2.1 proves that every language in $NP$ reduces to $SAT$. Together with step 1.1, [L4] gives that $SAT$ is NP-complete.

For each subformula $\theta$ of $\phi$, introduce the extension variable from [L1]. If $\theta$ is a literal $\mathrm{\ell }$, add $(\mathrm{\neg }{y}_{\theta }\vee \mathrm{\ell })$ and $(y_{\theta }\vee \mathrm{\neg }\mathrm{\ell })$. If $\theta =\alpha \wedge \beta$, add $(\mathrm{\neg }{y}_{\theta }\vee y_{\alpha })$, $(\mathrm{\neg }{y}_{\theta }\vee y_{\beta })$, and $(y_{\theta }\vee \mathrm{\neg }{y}_{\alpha }\vee \mathrm{\neg }{y}_{\beta })$. If $\theta =\alpha \vee \beta$, add $(y_{\theta }\vee \mathrm{\neg }{y}_{\alpha })$, $(y_{\theta }\vee \mathrm{\neg }{y}_{\beta })$, and $(\mathrm{\neg }{y}_{\theta }\vee y_{\alpha }\vee y_{\beta })$. If $\theta =\mathrm{\neg }\alpha$, add $(\mathrm{\neg }{y}_{\theta }\vee \mathrm{\neg }{y}_{\alpha })$ and $(y_{\theta }\vee y_{\alpha })$. If $\theta =\mathrm{\top }$ or $\theta =\mathrm{\perp }$, add the unit clause $(y_{\theta })$ or $(\mathrm{\neg }{y}_{\theta })$ respectively. Finally add the unit clause $(y_{\phi })$. Every clause has at most three literals.

Any satisfying assignment of $\phi$ extends to the new variables by setting each $y_{\theta }$ equal to the truth value of $\theta$ under that assignment. Then every local clause from step 1.1 is satisfied, including the negation and constant clauses, and $y_{\phi }=1$ because $\phi$ itself is true. So satisfiability of $\phi$ implies satisfiability of $T(\phi )$.

Conversely, suppose $T(\phi )$ is satisfiable. The clauses of step 1.1 force each $y_{\theta }$ to agree with the Boolean value prescribed by its immediate subformulas, and an induction on subformula complexity shows that every extension variable equals the value of its subformula under the restricted assignment to the original variables. Since the clause $(y_{\phi })$ is satisfied, the original formula $\phi$ is true.

Each subformula of $\phi$ contributes one fresh variable and only constantly many clauses, so the total size of $T(\phi )$ is linear in $\mathrm{\mid }\phi \mathrm{\mid }$. Together with steps 2.1 and 3.1, this proves the statement.

A truth assignment for a $3$-CNF formula can be checked clause by clause in polynomial time, exactly as for SAT. So $3$-SAT lies in $NP$.

By [L1], it is enough to reduce $SAT$ to $3$-SAT. Start from $\phi$ and apply [L2] to obtain an equisatisfiable CNF formula $T(\phi )$ whose clauses have size at most three.

Replace every $2$-clause $({\mathrm{\ell }}_1\vee {\mathrm{\ell }}_2)$ by $({\mathrm{\ell }}_1\vee {\mathrm{\ell }}_2\vee z)\wedge ({\mathrm{\ell }}_1\vee {\mathrm{\ell }}_2\vee \mathrm{\neg }z)$ with a fresh variable $z$, and replace every $1$-clause $(\mathrm{\ell })$ by $(\mathrm{\ell }\vee u\vee v)\wedge (\mathrm{\ell }\vee u\vee \mathrm{\neg }v)\wedge (\mathrm{\ell }\vee \mathrm{\neg }u\vee v)\wedge (\mathrm{\ell }\vee \mathrm{\neg }u\vee \mathrm{\neg }v)$ with fresh variables $u,v$. These replacements preserve satisfiability and produce only $3$-clauses.

Steps 1.2 and 2.1 give a polynomial-time many-one reduction from $SAT$ to $3$-SAT, because [L2] is linear-size and the padding in step 2.1 adds only constantly many clauses per short clause. Therefore $3$-SAT is NP-hard. Combined with step 1.1, [L3] yields that $3$-SAT is NP-complete.

By [L1], one satisfying assignment describes one tableau, hence one branch. There is no requirement that the encoding simultaneously list all other branches.

By [L2], the reduction asks only whether some accepting tableau exists. Existence of one accepting branch is enough, so explicit enumeration of every branch is unnecessary. Therefore the statement is false.

Fully distributing ${\phi }_n$ into CNF chooses one literal from each conjunctive pair $(a_i\wedge b_i)$, so the resulting CNF has one clause for every function $\{1,\dots ,n\}\to \{a_i,b_i\}$. That is $2^n$ distinct clauses.

Since the original formula has size $O(n)$ but the distributed CNF has $2^n$ clauses, the size blowup is exponential, not polynomial. Step 1.1 is exactly why [L2] keeps Tseitin variables available. Therefore the statement is false.