The Cook–Levin Tableau: Encoding a Computation as a Formula

Satisfiability is the problem of deciding whether a boolean formula in conjunctive normal form has an assignment making it true. Cook’s theorem states that it is NP-complete, and the proof is the only direct completeness argument most people ever read: everything else reduces from it. It also settles the question of what makes a problem complete rather than merely hard, which the reduction machinery treats in general. The argument takes a nondeterministic machine running in polynomial time and writes down a formula that is satisfiable exactly when the machine accepts. The formula’s variables describe a rectangular grid of machine configurations, and its clauses enforce that the grid is a legal computation. Reading the construction closely is worthwhile because it is the template for every later encoding argument, and because the counting shows exactly where the polynomial degree comes from.

The grid and its dimensions

Fix a language $L$ in NP and a nondeterministic machine $M$ that decides it in time $p(n)$, with $p$ a polynomial. Fix an input $x$ of length $n$. The machine’s computation, if it accepts, is a sequence of at most $p(n)$ configurations, each configuration being a description of the tape, the head position, and the state.

Two reductions of the configuration are used to keep the grid small. First, the tape is truncated to $p(n) + 1$ cells. A machine running for $p(n)$ steps cannot visit a cell further than $p(n)$ from the start, so the cells beyond that point are irrelevant and are not represented. Second, the alphabet is encoded in binary, so each tape cell needs a constant number of boolean variables rather than one per symbol. The state is likewise encoded in a constant number of variables, since the machine’s state set is fixed and independent of the input.

The result is a grid of $p(n) + 1$ rows and $p(n) + 1$ columns, where row $i$ is the configuration after $i$ steps and column $j$ is tape cell $j$. The number of cells is $(p(n)+1)^2$, which is a polynomial in $n$, and this is the single most important number in the proof, because the formula’s size is proportional to the number of cells and the formula must be polynomial for the reduction to run in polynomial time.

The variables are indexed accordingly. For a machine with a binary tape encoding of $b$ bits per cell and $s$ bits per state, the variable set is:

Variable group	Count	Meaning
tape symbol bits	$O((p(n)+1)^2 \log	\Gamma
head position	$O(p(n) \log p(n))$ per row	which cell the head occupies in row $i$
state bits	$O(p(n) \log	Q

A head position can be encoded in unary with one variable per column, at a cost of $p(n)$ variables per row rather than $\log p(n)$; both encodings are polynomial, and the unary version makes the clauses simpler to state. Textbooks differ on which they use, and the choice changes the degree of the polynomial but not the class.

The four families of clauses

The formula is a conjunction of four families, each enforcing one aspect of a legal computation. The formula is in CNF, so each family is a set of clauses, and the conjunction is their union.

Cell well-formedness. Each cell holds exactly one symbol. With a binary encoding this requires clauses forbidding each pair of distinct symbols from being simultaneously asserted, plus clauses ensuring at least one symbol is asserted. The number of pairs is constant for a fixed machine, so this family contributes $O((p(n)+1)^2)$ clauses.

Initial row. Row 0 must describe the initial configuration: the input $x$ in the first $n$ cells, blanks elsewhere, the head at cell 0, the machine in its start state. This is a set of unit clauses, one per cell, and their number is $O(p(n))$. The input is a constant of the reduction, so these clauses are written directly from $x$.

Acceptance. Some row must contain an accepting state. One clause per row, each a disjunction over the state-encoding variables asserting that the row’s state is accepting, gives $O(p(n))$ clauses of size $O(\log|Q|)$. Since the machine is nondeterministic and the bound is a maximum, the accepting row may be any row up to $p(n)$; the disjunction covers all of them.

Transition legality. For every pair of consecutive rows and every window of three adjacent cells, the local configuration must be consistent with the transition relation. A window of three cells in row $i$ and the corresponding three cells in row $i+1$ determine whether the head moved into, out of, or past the middle cell, so the transition relation forbids certain of these two-row patterns. Each forbidden pattern becomes one clause: the negation of the conjunction of the literals that would assert it.

The number of windows is $O(p(n)^2)$, one per cell per row pair, and the number of clauses per window is bounded by a constant that depends on the machine’s alphabet and state set. So this family contributes $O(p(n)^2)$ clauses, each of constant size.

Why the window spans two rows and three cells

The transition constraint is the part of the construction that is easy to get subtly wrong, and the shape of the window is where the correctness of the whole encoding lives.

A Turing machine’s step changes at most one tape cell: the one under the head. The head moves at most one cell per step. So a cell’s contents in row $i+1$ depend on the contents of cells $j-1$, $j$, and $j+1$ in row $i$: if the head was at $j-1$ and moved right, or at $j$ and wrote, or at $j+1$ and moved left, cell $j$ changes; otherwise it does not. Nothing outside those three cells can affect cell $j$, which is why the pair of rows can be checked window by window.

The window constraint is therefore local, and its locality is what makes the formula’s size quadratic rather than exponential. A machine with a global transition (a random-access machine that can jump to an arbitrary address) would have a window whose width grows with the address size, and the clause count would grow accordingly. The Turing machine’s locality is not an incidental feature of the model; it is what the encoding exploits.

The transition family can be generated directly from the machine’s transition relation, and the generator is short:

from itertools import product

def var(row, col, bit, cols, sym_bits):
    # one integer variable per (row, cell, bit) with a binary tape encoding
    return row * cols * sym_bits + col * sym_bits + bit + 1

def transition_clauses(rows, cols, sym_bits, legal):
    # legal: set of 2x3 bit patterns allowed across one step
    clauses = []
    for i in range(rows - 1):
        for j in range(1, cols - 1):
            for pattern in product(range(2), repeat=6 * sym_bits):
                if pattern in legal:
                    continue
                lits = []
                for cell in range(6):
                    for b in range(sym_bits):
                        bit = pattern[cell * sym_bits + b]
                        row, col = i + cell // 3, j - 1 + cell % 3
                        v = var(row, col, b, cols, sym_bits)
                        lits.append(v if bit else -v)
                clauses.append([-lit for lit in lits])   # forbid this window
    return clauses

The set legal is built once from the machine’s transition relation: a 2x3 pattern is legal when the head position implied by the upper row’s marked cell makes the lower row consistent with one step. A pattern outside legal becomes a single clause forbidding that combination. The clause count is proportional to the number of windows, which is what gives the $O(p(n)^2)$ size.

The window is also why the formula is in CNF without auxiliary variables in the textbook version. Each forbidden local pattern is a conjunction of a constant number of literals, and forbidding it is a single clause, the disjunction of their negations. No Tseitin-style extension variables are needed for the transition family, though they are needed when converting arbitrary formulas to CNF, which is the subject of the clause structure of 3-SAT.

The two directions

Correctness has two halves, and both are constructive.

If $M$ accepts $x$, there is an accepting computation of length at most $p(n)$. Assign each variable according to the corresponding cell, head position, and state in that computation. Every clause in the formula is satisfied by construction: the cells are well formed because the computation is a legal sequence of configurations, the initial row matches because the computation starts there, acceptance holds because some row is accepting, and the transition clauses hold because every step is legal. So the formula is satisfiable.

If the formula is satisfiable, take a satisfying assignment. Read row 0 as a configuration: the initial-row clauses force it to be the start configuration on $x$. Read each subsequent row as a configuration, using the cell well-formedness clauses to extract a unique symbol per cell and the head-position variables to locate the head. The transition clauses force each row to follow from the previous one by a legal step, because any illegal step would violate the constraint on some three-cell window. The acceptance clauses force some row to be accepting. So the assignment describes an accepting computation, and $M$ accepts $x$.

The second direction is where the local-to-global argument happens, and it is worth restating as a lemma: if every three-cell window across a row boundary is consistent with the transition relation, then the whole pair of rows is consistent. The proof is that each cell’s value in the later row is determined by a window, and the windows overlap consistently, so the determined values agree. There is no way for two windows to disagree about a cell, because both include it.

Counting the reduction’s cost

The reduction runs in time polynomial in the formula size, and the formula size is polynomial in $n$. Concretely, the construction has three loops: over cells to write well-formedness clauses, over cells to write initial-row clauses, and over windows to write transition clauses. Each loop iterates $O(p(n)^2)$ times and writes a constant amount of output per iteration, so the total output is $O(p(n)^2)$ symbols and the construction time is $O(p(n)^2)$.

The formula produced has clauses of size at most three for the transition family, but the well-formedness family can produce clauses of size proportional to the number of bits per cell, and the acceptance family produces clauses of size proportional to the state encoding. This is why the Cook–Levin theorem directly gives an NP-completeness result for general CNF satisfiability rather than for 3-SAT. The step from CNF to 3-SAT is a separate reduction, and it is not free: it introduces auxiliary variables.

What the encoding does not do

The tableau is a decision-procedure-independent statement. It does not give an algorithm for satisfiability, and it does not bound the difficulty of finding a satisfying assignment; it only asserts that one exists exactly when the machine accepts. This is the same existential asymmetry that defines NP, and it is why the theorem says nothing about whether P equals NP.

The construction also does not preserve the number of solutions in any meaningful way. Different accepting computations can give different satisfying assignments, and a single accepting computation may correspond to several assignments if the head-position encoding is not injective. For completeness this does not matter; for parsimonious reductions, which preserve solution counts, the encoding has to be tightened, and the tightening is usually done by adding variables that force a canonical form.

The polynomial degree is large but not specified by the theorem. For a machine with a quadratic time bound, the formula has $O(n^4)$ variables and clauses, and the reduction runs in time $O(n^4)$. This is enough to place satisfiability in NP and to place every NP language below it, and no tighter bound is claimed. Reductions designed for practice use far smaller encodings, and the gap between the theorem’s construction and a usable encoding is the gap between an existence proof and an engineering artifact.