Encode a Computation Tableau as SAT

Build Cook–Levin variables and local constraints, then prove correctness and polynomial size.

Problem

Let $N$ be a one-tape NTM deciding $L$ in time $T(n)\ge n$. Given $x$, construct in polynomial time a Boolean formula $\Phi_{N,x}$ satisfiable exactly when $N$ has an accepting computation on $x$. Specify tableau variables, uniqueness, start, transition, and acceptance constraints, and bound the formula size.

Prerequisites

Know the unit definitions and how resources are measured against encoded input length. Distinguish a conditional theorem, a reduction, and an algorithm.

Hint 1

Use a combined alphabet containing tape symbols and state-marked symbols.

Hint 2

Each cell contains exactly one symbol; express this by one at-least-one clause and pairwise exclusions.

Hint 3

Legality of consecutive rows is local to constant-width windows.

Full solution

Normalize $N$ so it has one accepting state that persists once entered, and pad accepting computations to exactly $T=T(|x|)$ steps. In $T$ steps the head visits only $O(T)$ cells, so use a $(T+1)\times(2T+1)$ tableau. Let $\Gamma'$ contain every tape symbol and every pair $[q,a]$ meaning “the head is here, the state is $q$, and the scanned symbol is $a$.” Introduce $X_{t,i,s}$ for every row $t$, cell $i$, and $s\in\Gamma'$.

Cell constraints require exactly one symbol:

and, for distinct $s,s'$, clauses $(\neg X_{t,i,s}\vee\neg X_{t,i,s'})$. The start constraints are unit clauses fixing row zero to the initial configuration on $x$, blanks elsewhere, and the start-state marker at the first input symbol. Boundary cells may be fixed to blanks with guards wide enough that no $T$-step computation reaches beyond them.

For transitions, observe that the contents of cell $i$ in row $t+1$ depend only on cells $i-1,i,i+1$ in row $t$ and on one chosen transition of $N$. Since $N$ and $\Gamma'$ are fixed, the set of legal constant-size windows is finite. Forbid every illegal pair of neighboring windows by a constant-width CNF clause. Overlapping windows ensure a single globally consistent successor row and exactly one head marker. Nondeterministic alternatives remain as different satisfying assignments; the formula does not choose one in advance.

Acceptance can be required by

or, after making acceptance persistent and padding, by requiring an accepting marker in the final row. A satisfying assignment gives one symbol per cell. Start clauses identify row zero, local clauses make every next row a legal successor, and the acceptance clause yields an accepting computation. Conversely, an accepting computation fills the variables and satisfies every constraint. This proves both directions.

There are $O(T^2|\Gamma'|)$ variables. Exactly-one clauses contribute at most $O(T^2|\Gamma'|^2)$ literals, and local constraints contribute $O(T^2)$ constant-size clauses because the machine is fixed. The direct formula is polynomial in $T(n)$, hence polynomial in $n$ when $T$ is polynomial. If a strict 3CNF output is required, replace long disjunctions by chains of auxiliary variables, increasing size only linearly. The construction algorithm enumerates cells and fixed templates, so its running time is polynomial in the output size.

Checkpoints

Check both logical directions, halting of every relevant branch, and that output length and construction time are polynomial in the encoded input length.

Common mistakes

• Writing only local transition constraints without exact-one cell constraints.
• Assuming a deterministic successor for a nondeterministic machine.
• Counting $T^2$ cells but not the literals needed for exclusivity.

Sources and verification

• Merged summary, pp. 50-54
• 2026 transcripts 12-13
• Sipser 3e, sec. 7.4
• Arora-Barak draft, sec. 2.3
• Catalog mapping: data/exercises.json; statements and solutions are independently written; personal submissions are non-authoritative.

Provenance and confidence

The exercise is an original synthesis. Confidence reflects verification of the mathematical claim against the textbook sources listed above; course sources are used only where direct coverage is identified.

Open in the visualization gallery: Cook–Levin tableau