Correctness of the Cook–Levin tableau

tableau tm u L T is satisfiable exactly when some certificate w of length L makes tm, started on u ++ w, halt within T steps with output [true]. More precisely, for a fixed certificate z, it has a satisfying assignment encoding z exactly when tm, started on u ++ z, has halted after T steps with output [true] (exists_eval_tableau_iff).

Each family of clauses is first characterised semantically (eval_initClauses, eval_readClauses, eval_stepClauses, …). The uniqueness clauses (eval_uniqueClauses) are not needed for soundness; they make the satisfying assignments unique for each certificate (Complexity/Computability/Complexity/CookLevin/Parsimonious.lean), and completeness checks that the assignment read off the run satisfies them. Soundness then shows, by induction on time, that a satisfying assignment describes the run on the certificate it encodes (Agrees, agrees_of_eval_tableau): by the one-hot clauses it suffices that the basic features holding at time t + 1 are true (Agrees.of_oneHot), and each of them follows from a term of its step equation (Turing.MultiTapeTM.Feature.holds_step_iff_exists_stepTerms) through a step clause. Completeness reads an assignment off the run (runAssignment); its step clauses hold by the same step equation.

Main results

• Cslib.Complexity.CookLevin.exists_eval_tableau_iff: the tableau with fixed certificate bits.
• Cslib.Complexity.CookLevin.tableau_satisfiable_iff: the tableau is correct.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 2.3.

def Cslib.Complexity.CookLevin.certWord {k : ℕ} {State : Type} (σ : Var k State → Bool) (L : ℕ) : List Bool

The certificate encoded by an assignment.

@[simp]

theorem Cslib.Complexity.CookLevin.length_certWord {k : ℕ} {State : Type} (σ : Var k State → Bool) (L : ℕ) : (certWord σ L).length = L

theorem Cslib.Complexity.CookLevin.certWord_eq_ofFn {k : ℕ} {State : Type} (σ : Var k State → Bool) (L : ℕ) : certWord σ L = List.ofFn fun (j : Fin L) => σ (Var.cert ↑j)

Semantics of the clause families

theorem Cslib.Complexity.CookLevin.eval_initClauses {k : ℕ} {State : Type} {tm : Turing.MultiTapeTM k Bool State} {T : ℕ} {σ : Var k State → Bool} : Logic.PL.CNF.eval σ (initClauses tm T) = true ↔ σ (Var.holds 0 (Turing.MultiTapeTM.Feature.state (some tm.q₀))) = true ∧ σ (Var.holds 0 (Turing.MultiTapeTM.Feature.inPos 1)) = true ∧ σ (Var.holds 0 (Turing.MultiTapeTM.Feature.out Turing.OutView.empty)) = true ∧ ∀ (i : Fin k), σ (Var.holds 0 (Turing.MultiTapeTM.Feature.head i 0)) = true ∧ ∀ (z : ℤ), |z| ≤ ↑T → σ (Var.holds 0 (Turing.MultiTapeTM.Feature.cell i z none)) = true

The initial clauses fix the initial configuration.

theorem Cslib.Complexity.CookLevin.eval_readClauses {k : ℕ} {State : Type} {u : List Bool} {L T : ℕ} {σ : Var k State → Bool} (t : ℕ) : Logic.PL.CNF.eval σ (readClauses u L T t) = true ↔ (∀ (i : Fin k) (z : ℤ) (s : Option Bool), |z| ≤ ↑T → σ (Var.holds t (Turing.MultiTapeTM.Feature.head i z)) = true → σ (Var.holds t (Turing.MultiTapeTM.Feature.cell i z s)) = true → σ (Var.holds t (Turing.MultiTapeTM.Feature.read i s)) = true) ∧ ∀ j < u.length + L + 2, σ (Var.holds t (Turing.MultiTapeTM.Feature.inPos j)) = true → σ (Var.holds t (Turing.MultiTapeTM.Feature.inRead (Turing.inputAt (u ++ certWord σ L) j))) = true

The read clauses: the symbol a head reads, from its position and the cell there, is true.

theorem Cslib.Complexity.CookLevin.eval_uniqueClauses {k : ℕ} {State : Type} {σ : Var k State → Bool} [Fintype State] [DecidableEq State] (t : ℕ) : Logic.PL.CNF.eval σ (uniqueClauses t) = true ↔ (∀ (i : Fin k) (s s' : Option Bool), σ (Var.holds t (Turing.MultiTapeTM.Feature.read i s)) = true → σ (Var.holds t (Turing.MultiTapeTM.Feature.read i s')) = true → s = s') ∧ (∀ (s s' : Option Bool), σ (Var.holds t (Turing.MultiTapeTM.Feature.inRead s)) = true → σ (Var.holds t (Turing.MultiTapeTM.Feature.inRead s')) = true → s = s') ∧ ∀ (y : Turing.MultiTapeTM.Situation k State), σ (Var.holds t (Turing.MultiTapeTM.Feature.sit y)) = true → σ (Var.holds t (Turing.MultiTapeTM.Feature.state (some y.1))) = true ∧ σ (Var.holds t (Turing.MultiTapeTM.Feature.inRead y.2.1)) = true ∧ ∀ (i : Fin k), σ (Var.holds t (Turing.MultiTapeTM.Feature.read i (y.2.2 i))) = true

The uniqueness clauses: each head reads at most one symbol, and a true situation has its state and symbols read true.

def Cslib.Complexity.CookLevin.Agrees {k : ℕ} {State : Type} [Fintype State] (σ : Var k State → Bool) (n T t : ℕ) {input : List Bool} (cfg : Turing.Cfg k Bool State input) : Prop

An assignment describes the configuration cfg at time t: the basic features true at time t are those holding of cfg.

theorem Cslib.Complexity.CookLevin.Agrees.sit {k : ℕ} {State : Type} {u : List Bool} {L T : ℕ} {σ : Var k State → Bool} [Fintype State] {cfg : Turing.Cfg k Bool State (u ++ certWord σ L)} {t : ℕ} (hA : Agrees σ (u.length + L) T t cfg) (hb : ∀ (i : Fin k), |cfg.workTapePos i| ≤ ↑T) (hread : Logic.PL.CNF.eval σ (readClauses u L T t) = true) (hsit : Logic.PL.CNF.eval σ (sitClauses t) = true) {y : Turing.MultiTapeTM.Situation k State} (hy : Turing.MultiTapeTM.Feature.Holds cfg (Turing.MultiTapeTM.Feature.sit y)) : σ (Var.holds t (Turing.MultiTapeTM.Feature.sit y)) = true

Under the read and situation clauses, the situation of a configuration that an assignment describes is true.

theorem Cslib.Complexity.CookLevin.eval_stepClauses {k : ℕ} {State : Type} {tm : Turing.MultiTapeTM k Bool State} {u : List Bool} {L T : ℕ} {σ : Var k State → Bool} [Fintype State] [DecidableEq State] (t : ℕ) : Logic.PL.CNF.eval σ (stepClauses tm u L T t) = true ↔ ∀ φ ∈ Turing.MultiTapeTM.Feature.basic (u.length + L) T, ∀ c ∈ Turing.MultiTapeTM.Feature.stepTerms tm (u.length + L) T φ, (∀ l ∈ c, σ (Var.holds t l.1) = l.2) → σ (Var.holds (t + 1) φ) = true

The step clauses impose the step equation of every basic feature.

theorem Cslib.Complexity.CookLevin.eval_tableau {k : ℕ} {State : Type} {tm : Turing.MultiTapeTM k Bool State} {u : List Bool} {L T : ℕ} {σ : Var k State → Bool} [Fintype State] [DecidableEq State] : Logic.PL.CNF.eval σ (tableau tm u L T) = true ↔ Logic.PL.CNF.eval σ (initClauses tm T) = true ∧ (∀ t ≤ T, Logic.PL.CNF.eval σ (oneHotClauses u L T t) = true) ∧ (∀ t < T, Logic.PL.CNF.eval σ (readClauses u L T t) = true ∧ Logic.PL.CNF.eval σ (sitClauses t) = true ∧ Logic.PL.CNF.eval σ (uniqueClauses t) = true ∧ Logic.PL.CNF.eval σ (stepClauses tm u L T t) = true) ∧ Logic.PL.CNF.eval σ (acceptClauses T) = true

The tableau holds when each of its families does, at each time.

Soundness

theorem Cslib.Complexity.CookLevin.Agrees.of_oneHot {k : ℕ} {State : Type} {u : List Bool} {L T : ℕ} {σ : Var k State → Bool} [Fintype State] [DecidableEq State] {input : List Bool} {cfg : Turing.Cfg k Bool State input} {t : ℕ} (hlen : input.length = u.length + L) (hone : Logic.PL.CNF.eval σ (oneHotClauses u L T t) = true) (hb : ∀ (i : Fin k), |cfg.workTapePos i| ≤ ↑T) (h : ∀ φ ∈ Turing.MultiTapeTM.Feature.basic (u.length + L) T, Turing.MultiTapeTM.Feature.Holds cfg φ → σ (Var.holds t φ) = true) : Agrees σ (u.length + L) T t cfg

Under the one-hot clauses at time t, an assignment describes cfg at time t as soon as the basic features holding of cfg are true.

theorem Cslib.Complexity.CookLevin.agrees_of_eval_tableau {k : ℕ} {State : Type} {tm : Turing.MultiTapeTM k Bool State} {u : List Bool} {L T : ℕ} {σ : Var k State → Bool} [Fintype State] [DecidableEq State] (h : Logic.PL.CNF.eval σ (tableau tm u L T) = true) (t : ℕ) : t ≤ T → Agrees σ (u.length + L) T t (Turing.MultiTapeTM.runFrom (tm.initCfg (u ++ certWord σ L)) t)

A satisfying assignment describes the run on the certificate it encodes, up to time T.

Completeness

noncomputable def Cslib.Complexity.CookLevin.runAssignment {k : ℕ} {State : Type} [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) (u w : List Bool) : Var k State → Bool

The assignment read off the run of tm on u ++ w: each feature variable says whether the feature holds of the run, and the certificate variables spell w.

@[simp]

theorem Cslib.Complexity.CookLevin.runAssignment_holds {k : ℕ} {State : Type} {tm : Turing.MultiTapeTM k Bool State} {u : List Bool} [DecidableEq State] {w : List Bool} {t : ℕ} {φ : Turing.MultiTapeTM.Feature k State} : runAssignment tm u w (Var.holds t φ) = true ↔ Turing.MultiTapeTM.Feature.Holds (Turing.MultiTapeTM.runFrom (tm.initCfg (u ++ w)) t) φ

theorem Cslib.Complexity.CookLevin.eval_tableau_runAssignment {k : ℕ} {State : Type} {tm : Turing.MultiTapeTM k Bool State} {u : List Bool} {L T : ℕ} [DecidableEq State] [Fintype State] {w : List Bool} (hw : w.length = L) (hhalt : (Turing.MultiTapeTM.runFrom (tm.initCfg (u ++ w)) T).state = none) (hout : (Turing.MultiTapeTM.runFrom (tm.initCfg (u ++ w)) T).output = [true]) : Logic.PL.CNF.eval (runAssignment tm u w) (tableau tm u L T) = true

The assignment read off an accepting run satisfies the tableau.

theorem Cslib.Complexity.CookLevin.exists_eval_tableau_iff {k : ℕ} {State : Type} {tm : Turing.MultiTapeTM k Bool State} {u : List Bool} {T : ℕ} [DecidableEq State] [Fintype State] {z : List Bool} : (∃ (σ : Var k State → Bool), certWord σ z.length = z ∧ Logic.PL.CNF.eval σ (tableau tm u z.length T) = true) ↔ (Turing.MultiTapeTM.runFrom (tm.initCfg (u ++ z)) T).state = none ∧ (Turing.MultiTapeTM.runFrom (tm.initCfg (u ++ z)) T).output = [true]

The tableau with fixed certificate bits. tableau tm u z.length T has a satisfying assignment whose certificate is z exactly when tm, started on u ++ z, has halted after T steps with output [true].

theorem Cslib.Complexity.CookLevin.tableau_satisfiable_iff {k : ℕ} {State : Type} {tm : Turing.MultiTapeTM k Bool State} {u : List Bool} {L T : ℕ} [DecidableEq State] [Fintype State] : (tableau tm u L T).Satisfiable ↔ ∃ (w : List Bool), w.length = L ∧ (Turing.MultiTapeTM.runFrom (tm.initCfg (u ++ w)) T).state = none ∧ (Turing.MultiTapeTM.runFrom (tm.initCfg (u ++ w)) T).output = [true]

The Cook–Levin tableau is correct. tableau tm u L T is satisfiable exactly when some certificate w of length L makes tm, started on u ++ w, halt within T steps with output [true].