The Cook--Levin Theorem: Examples and Counterexamples

The bare tape-symbol options contribute the three symbols $0,1,\bigsqcup$. The state-tagged options contribute one pair $(q,a)$ for each $q\in Q$ and $a\in \mathrm{\Gamma }$, so there are $4\cdot 3=12$ such tagged symbols.

By [L1], the total extended alphabet size is therefore $3+12=15$, independent of the input length. This is the concrete constant hidden in the general lemma.

The Tseitin clauses are $(\mathrm{\neg }a\vee x)$, $(\mathrm{\neg }a\vee y)$, $(a\vee \mathrm{\neg }x\vee \mathrm{\neg }y)$ for $a\leftrightarrow (x\wedge y)$, together with $(b\vee \mathrm{\neg }a)$, $(b\vee \mathrm{\neg }z)$, $(\mathrm{\neg }b\vee a\vee z)$ for $b\leftrightarrow (a\vee z)$, and the root clause $(b)$.

If $\phi$ is satisfiable, set $a$ and $b$ to the truth values of their subformulas; then all clauses in step 1.1 are satisfied. Conversely, any satisfying assignment of those clauses forces $b=1$ and hence $(x\wedge y)\vee z=1$. So step 1.1 is an explicit equisatisfiable $3$-CNF encoding of $\phi$, illustrating [L1] and therefore [L2].

The formula for $N$ is produced from the fixed constraint families in [L3] by iterating over tableau cells and local windows. This construction never generates either computation branch.

The left branch has an accepting tableau of constant size, so assigning the tableau variables according to that branch satisfies the formula. By [L1], this assignment encodes only the accepting branch; the rejecting branch is not encoded by it. Together with the branch-free construction in step 1.1, this refutes the enumeration slogan [L2].