The Cook–Levin tableau

Given a deterministic multi-tape machine tm over the binary alphabet, a fixed input prefix u, a certificate length L and a number of steps T, tableau tm u L T is a formula in conjunctive normal form that is satisfiable exactly when some certificate w of length L makes tm, started on u ++ w, halt within T steps with output [true] (Cslib.Complexity.CookLevin.tableau_satisfiable_iff, in CslibFrontier/Computability/Complexity/CookLevin/Correctness.lean). It has exactly one satisfying assignment (of its variables) for each such certificate (Cslib.Complexity.CookLevin.modelCount_tableau, in CslibFrontier/Computability/Complexity/CookLevin/Parsimonious.lean).

The formula describes the first T + 1 configurations of the run directly, in the model of Turing.MultiTapeTM: a read-only input tape, k two-way infinite work tapes, and a write-only output tape. Its variables say which features (Turing.MultiTapeTM.Feature) hold at which time: the state, the input head, the work heads and work cells in the window |z| ≤ T (a head moves at most one cell per step), the view of the output, the symbols read and the situation of a step. The only other variables are the certificate bits.

The clauses fix the initial configuration, ask that exactly one basic feature of each group hold at each time (Turing.MultiTapeTM.Feature.groups), force the symbols read and the situation that actually hold to be true, and impose the step equation: each term of Turing.MultiTapeTM.Feature.stepTerms at time t implies its feature at time t + 1. For satisfiability, forcing the symbols read and the situations in one direction suffices, because situations occur only positively in the terms (Turing.MultiTapeTM.Feature.mem_basic_of_mem_stepTerms). The uniqueness clauses force the converse: each head reads at most one symbol, and a true situation has its state and symbols read true. Every variable of the tableau is then determined by the certificate bits, which makes the reduction parsimonious (Cslib.Complexity.CookLevin.modelCount_tableau, in CslibFrontier/Computability/Complexity/CookLevin/Parsimonious.lean). No conversion to a single-tape or oblivious machine is needed: the action of a step depends on the situation only, and every tape applies its part of the action locally.

The definitions are noncomputable: the transition function of Turing.MultiTapeTM is chosen from its transition relation, and the states and situations are enumerated through Finset.toList in an arbitrary order. Both depend on the machine only, so a machine producing the tableau can store them in a table; the enumerations that depend on the input (Turing.windowList, List.range) are explicit lists. Only the set of satisfying assignments matters for correctness.

Main definitions

• Cslib.Complexity.CookLevin.Var.
• Cslib.Complexity.CookLevin.tableau.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 2.3.
• C. H. Papadimitriou, Computational Complexity, Theorem 8.2.

inductive Cslib.Complexity.CookLevin.Var (k : ℕ) (State : Type) : Type

The variables of the tableau for a machine with k work tapes and states in State.

• holds {k : ℕ} {State : Type} (t : ℕ) (φ : Turing.MultiTapeTM.Feature k State) : Var k State

  The feature φ holds at time t.

• cert {k : ℕ} {State : Type} (j : ℕ) : Var k State

  The j-th bit of the certificate.

@[instance_reducible]

instance Cslib.Complexity.CookLevin.instDecidableEqVar {k✝ : ℕ} {State✝ : Type} [DecidableEq State✝] : DecidableEq (Var k✝ State✝)

def Cslib.Complexity.CookLevin.instDecidableEqVar.decEq {k✝ : ℕ} {State✝ : Type} [DecidableEq State✝] (x✝ x✝¹ : Var k✝ State✝) : Decidable (x✝ = x✝¹)

theorem Cslib.Complexity.CookLevin.Var.holds_right_injective {k : ℕ} {State : Type} (t : ℕ) : Function.Injective (holds t)

Clauses

def Cslib.Complexity.CookLevin.initClauses {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) (T : ℕ) : Logic.PL.CNF (Var k State)

The initial configuration: state q₀, input head on the first input cell, every work head on cell 0, blank work tapes, empty output.

noncomputable def Cslib.Complexity.CookLevin.oneHotClauses {k : ℕ} {State : Type} (u : List Bool) (L T : ℕ) [Fintype State] [DecidableEq State] (t : ℕ) : Logic.PL.CNF (Var k State)

Exactly one basic feature of each group holds at time t.

def Cslib.Complexity.CookLevin.inputClauses {k : ℕ} {State : Type} (u : List Bool) (L t j : ℕ) : Logic.PL.CNF (Var k State)

The input head at position j reads the input symbol there: a fixed symbol of u or a blank end marker, or a certificate bit.

def Cslib.Complexity.CookLevin.readClauses {k : ℕ} {State : Type} (u : List Bool) (L T t : ℕ) : Logic.PL.CNF (Var k State)

The symbols under the heads at time t: the symbol a head reads, from its position and the cell there, is true.

noncomputable def Cslib.Complexity.CookLevin.sitClauses {k : ℕ} {State : Type} [Fintype State] (t : ℕ) : Logic.PL.CNF (Var k State)

The situation at time t: a situation whose state and symbols read are true is true.

noncomputable def Cslib.Complexity.CookLevin.uniqueClauses {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (t : ℕ) : Logic.PL.CNF (Var k State)

The symbols read and the situation at time t are unique: each work head and the input head read at most one symbol, and a true situation has its state and symbols read true. With the read and situation clauses, the symbols read and the situation that are true are then exactly those that hold.

noncomputable def Cslib.Complexity.CookLevin.stepClauses {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) (u : List Bool) (L T : ℕ) [Fintype State] [DecidableEq State] (t : ℕ) : Logic.PL.CNF (Var k State)

The step equation from time t to time t + 1: each term of the step equation of a basic feature, at time t, implies the feature at time t + 1.

def Cslib.Complexity.CookLevin.acceptClauses {k : ℕ} {State : Type} (T : ℕ) : Logic.PL.CNF (Var k State)

The run has halted by time T with output [true].

noncomputable def Cslib.Complexity.CookLevin.tableau {k : ℕ} {State : Type} (tm : Turing.MultiTapeTM k Bool State) (u : List Bool) (L T : ℕ) [Fintype State] [DecidableEq State] : Logic.PL.CNF (Var k State)

The Cook–Levin tableau of tm on inputs u ++ w with |w| = L, unrolled for T steps.