skip to content

How does the Cook-Levin proof turn an arbitrary polynomial-time verifier's whole run into one Boolean formula?

level: seniorimportance: must knowfreq 50%

answer

  1. draw the run as a grid
  2. one variable per cell per symbol
  3. start, step and accept clauses
  4. a step is checkable locally
  5. grid is the time bound squared

basics

~20 s

It writes the run out as a grid with one row per step and one column per tape square, gives each cell a Boolean variable for every symbol it could hold, and adds clauses forcing a legal, accepting history.

solid answer

~50 s

Picture the run as a rectangular grid, one row per step of the time bound and one column per tape square the machine could reach. Each cell gets one Boolean variable per possible content, so `x[i][j][s]` means `at step i, square j holds s`. Four groups of clauses pin the grid down: every cell holds **exactly one** symbol; the first row spells the start configuration, with the input forced and the **certificate cells deliberately left free**; every step is legal; and an accepting state appears somewhere. Legality of a step is checked **locally** - a step changes the tape only around the head, so it is enough to require that every small window of two rows by three columns matches one of a fixed set of legal patterns. With a time bound `t`, the grid has order `t` squared cells, so the formula stays polynomial in the input length.

code

pseudocode · 21 lines
pseudocode
// x[i][j][s] is true when the cell in row i, column j holds content s
formula := TRUE

// 1. cell: exactly one content per cell
for each row i, for each column j:
    formula := formula AND exactly_one( x[i][j][s] for s in contents )

// 2. start: row 0 spells the start configuration
for each column j in input_region:
    formula := formula AND x[0][j][ input_symbol(j) ]
for each column j in blank_region:
    formula := formula AND x[0][j][ BLANK ]
// columns in certificate_region get NO start clause: the assignment chooses them

// 3. move: every 2-by-3 window matches some legal pattern
for each row i from 0 to lastRow - 1, for each column j:
    window := cells (i, j..j+2) and (i+1, j..j+2)
    formula := formula AND ( OR over legal patterns p: window_equals(window, p) )

// 4. accept: an accepting marker appears somewhere
formula := formula AND ( OR over i, j: x[i][j][ACCEPT] )

go deeper

for a junior

Hold on to the picture: an entire computation is written out as a grid of cells, and a Boolean formula says the grid is a legal run that accepts.

for a middle

Be able to name the variables and the four clause groups, and say which one carries the input and which leaves room for a guess. That structure is the whole construction.

for a senior

Explain why the step check is local and why that keeps the formula polynomial, and be precise that the first row forces the input but not the certificate - that freedom is where the difficulty lives.

for a principal

Treat it as the canonical example of encoding a process as constraints: a state grid, local consistency rules, and free variables for the unknowns. That shape recurs far beyond this theorem.

## The picture: a run written down as a grid Fix a language `L` in NP, its verifier, and a polynomial time bound `t`. For an input `x` of length `n`, the verifier reading a certificate runs for at most `t(n)` steps, and in `t(n)` steps it can touch at most `t(n)` tape squares. So a whole run fits in a rectangle - conventionally called the **computation tableau** - of about `t(n) + 1` rows by `t(n) + 2` columns. Row `i` is a snapshot of the tape after `i` steps, with one extra marker showing where the head is and which state the machine is in. The whole trick of the theorem is that this rectangle is a *finite object*, so it can be described by Boolean variables, and that being a *legal* rectangle is a *local* property, so it can be described by short clauses. ## The variables Let the alphabet of possible cell contents be the tape symbols together with one marker per machine state. Introduce one variable per (row, column, content) triple: - `x[i][j][s]` is true exactly when the cell in row `i`, column `j` holds content `s`. - The number of contents is a **constant** fixed by the machine, not by the input, so the variable count is a constant multiple of the number of cells. Note what the variables do *not* encode: they do not encode an answer, and they do not encode a chosen certificate. They describe an arbitrary filled-in rectangle, and the clauses are what separate the rectangles that are genuine accepting runs from the rest. ## The four clause groups | Group | What it forces | Rough size | |---|---|---| | cell | each cell holds exactly one content | one small clause set per cell | | start | row 0 spells the start configuration: input forced, certificate region free, the rest blank | linear in the row width | | move | every two-by-three window matches a legal pattern | a constant number of clauses per window | | accept | an accepting state marker appears somewhere in the grid | one long clause | The **start** group is where the certificate enters, and it is the subtlety most often missed. The cells holding the input are forced to spell `x`. The cells reserved for the certificate are constrained only by the cell group - they must hold *one* symbol each, but *which* one is left to the assignment. That freedom is the existential quantifier of NP, expressed as free variables. ## Why a small window is enough One step of a machine changes the tape in only one place - the square under the head - and moves the head one square. Everything else in the row is copied down unchanged. Therefore any illegal transition shows up as a local anomaly, and a fixed-size window centred on it will contain the evidence: - A window spanning **two rows and three columns** contains six cells; with a constant alphabet, the number of possible window contents is a constant, and so is the number of them that are legal. - Requiring each window to match one of the legal patterns costs a constant number of clauses per window, and there are order `t` squared windows. - The key lemma: **if row 0 is a correct start configuration and every window is legal, then each row genuinely follows from the row above it.** Local correctness everywhere plus a correct start gives global correctness - which is why no clause ever has to compare two whole rows. ## The size arithmetic Let `n` be the input length and let the time bound be `t(n) = n^k`. The grid has order `n^(2k)` cells, hence order `n^(2k)` variables and order `n^(2k)` clauses. That is polynomial in `n` for each fixed language, which is exactly what a polynomial-time reduction requires - and emitting the clauses is a mechanical walk over indices, with no search, so the construction itself runs in polynomial time. ## Why the construction proves what it claims Run the correspondence in both directions: 1. If `x` is a yes-instance, some certificate makes the verifier accept; write that accepting run into the grid, read off the variable values, and every clause group is satisfied by construction. 2. If the formula is satisfiable, take a satisfying assignment: the cell clauses make it a well-formed grid, the start clauses make row 0 a legal start on input `x`, the move clauses make each row follow from the last, and the accept clause puts an accepting state in it. The certificate cells of row 0 spell a certificate that the verifier accepts, so `x` is a yes-instance. Nothing in this argument assumed the machine was deterministic, and nothing assumed the certificate was known in advance. That generality is the point: the same scheme is instantiated for every language in NP, which is how one construction discharges a quantifier over an entire class.

  • Where does the certificate actually live in the grid?
    In the first row, next to the input. Those cells get no start clause, so the only constraint on them is that each holds one symbol; the assignment picks the contents. Reading them off a satisfying assignment gives a certificate the verifier accepts, which is what makes the correspondence exact.
  • What does the formula look like if the machine is deterministic and reads no certificate?
    The first row is fully forced and every later row is determined by the windows, so the formula has at most one satisfying assignment - it computes rather than searches, and asking whether it is satisfiable is no harder than running the machine. The free certificate cells are where the difficulty comes from.
  • Why is the clause count polynomial rather than exponential in the input length?
    Because the grid is sized by the time bound, not by the number of possible runs. With a bound of `n^k` steps, there are order `n^(2k)` cells and one constant-size clause set per cell or window. The exponentially many candidate runs are represented by assignments to those variables, never enumerated.

Proof-reading a flip-book by checking each pair of neighbouring frames only in the small patch around the pencil: if every such patch is a legal change and the first page is right, the whole animation is consistent, and you never had to watch it play.

saying these in an interview costs you the question

  • Thinks the construction simulates the machine and reads off an answer.
  • Says the builder must know the certificate before writing the formula.
  • Believes the formula's size grows exponentially with the input length.
  • Assumes the encoding only works for a deterministic machine.
  • Thinks each row must be compared against the previous row in full.