The Cook–Levin reduction is parsimonious

The Cook–Levin tableau tableau tm u L T has exactly one satisfying assignment for each certificate w of length L that makes tm, started on u ++ w, halt within T steps with output [true] (modelCount_tableau). Consequently the Cook–Levin reduction of a verifier V maps an instance a to a formula with exactly as many satisfying assignments as there are certificates of the verifier's length that V accepts with a (modelCount_reduce): it is parsimonious Valiant, Arora and Barak, Section 17.3.

Every variable of the tableau is determined (Determined): it is a certificate bit j < L, a basic feature at a time t ≤ T, or a symbol read or a situation at a time t < T (determined_of_mem_vars_tableau). A satisfying assignment σ agrees on the determined variables with the assignment read off the run on its own certificate (eq_runAssignment_of_eval_tableau): on the basic features by the soundness of the tableau (agrees_of_eval_tableau), on the symbols read since the read clauses make the actual symbol true and the uniqueness clauses allow only one, and on the situations since the situation clauses and the uniqueness clauses make a situation true exactly when its state and its symbols read are. Two satisfying assignments with the same certificate therefore agree on every variable of the tableau. Conversely, when T > 0 the input clauses mention every certificate bit, so two satisfying assignments that agree on the variables of the tableau have the same certificate; when T = 0 no run has halted and the tableau is unsatisfiable.

Main definitions

• Cslib.Complexity.CookLevin.Determined: the variables determined by the certificate.

Main results

• Cslib.Complexity.CookLevin.determined_of_mem_vars_tableau: the variables of the tableau are determined.
• Cslib.Complexity.CookLevin.eq_runAssignment_of_eval_tableau: a satisfying assignment is determined by its certificate.
• Cslib.Complexity.CookLevin.modelCount_tableau: the number of satisfying assignments of the tableau is the number of accepted certificates.
• Cslib.Complexity.CookLevin.modelCount_reduce: the Cook–Levin reduction is parsimonious.

References

• L. Valiant, The complexity of computing the permanent
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 17.3.

def Cslib.Complexity.CookLevin.Determined {k : ℕ} {State : Type} [Fintype State] (n L T : ℕ) (v : Var k State) : Prop

The variables of the tableau for inputs of length n, certificates of length L and T steps that a satisfying assignment determines from its certificate: the certificate bits j < L, the basic features at times t ≤ T, and the symbols read and the situations at times t < T.

The variables of the tableau

theorem Cslib.Complexity.CookLevin.determined_of_mem_vars_tableau {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] {tm : Turing.MultiTapeTM k Bool State} {u : List Bool} {L T : ℕ} {v : Var k State} (hv : v ∈ (tableau tm u L T).vars) : Determined (u.length + L) L T v

The variables of the tableau are determined by the certificate.

Satisfying assignments are determined by their certificates

theorem Cslib.Complexity.CookLevin.eq_runAssignment_of_eval_tableau {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] {tm : Turing.MultiTapeTM k Bool State} {u : List Bool} {L T : ℕ} {σ : Var k State → Bool} (h : Logic.PL.CNF.eval σ (tableau tm u L T) = true) {v : Var k State} (hv : Determined (u.length + L) L T v) : σ v = runAssignment tm u (certWord σ L) v

A satisfying assignment is determined by its certificate: on the determined variables it agrees with the assignment read off the run on its certificate.

Counting satisfying assignments

theorem Cslib.Complexity.CookLevin.modelCount_tableau {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] {tm : Turing.MultiTapeTM k Bool State} {u : List Bool} {L T : ℕ} : (tableau tm u L T).modelCount = {w : Fin L → Bool | (Turing.MultiTapeTM.runFrom (tm.initCfg (u ++ List.ofFn w)) T).state = none ∧ (Turing.MultiTapeTM.runFrom (tm.initCfg (u ++ List.ofFn w)) T).output = [true]}.card

The Cook–Levin tableau is parsimonious: its satisfying assignments correspond one to one to the certificates w of length L that make tm, started on u ++ w, halt within T steps with output [true].

theorem Cslib.Complexity.CookLevin.modelCount_reduce {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] {tm : Turing.MultiTapeTM k Bool State} {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × List Bool → Bool} {c d : ℕ} (a : α) (hrun : ∀ (w : List Bool), w.length = Polynomial.eval (enc a).length p → (Turing.MultiTapeTM.runFrom (tm.initCfg ((Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) (a, w))) (c * (((Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) (a, w)).length + 1) ^ d)).state = none ∧ (Turing.MultiTapeTM.runFrom (tm.initCfg ((Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) (a, w))) (c * (((Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) (a, w)).length + 1) ^ d)).output = [V (a, w)]) : (reduce tm p c d enc a).modelCount = acceptCount V a (Polynomial.eval (enc a).length p)

The Cook–Levin reduction is parsimonious. Under the hypotheses of reduce_mem_SAT_iff, the formula reduce tm p c d enc a has exactly as many satisfying assignments as there are certificates w of length p (enc a).length with V (a, w) = true.