The Cook–Levin reduction

Let A be a problem in NP, verified by V with certificates of length p of the instance length, where V is computed by the machine tm in time c * (n + 1) ^ d. The reduction maps an instance a to the tableau of tm on inputs encPair enc encBits (a, w) = frame (enc a) ++ w, for the unknown certificate w of length p (enc a).length, unrolled for exactly the number of steps tm is allowed on such inputs. Its variables are then renamed injectively to natural numbers.

reduce_mem_SAT_iff says that the reduction is correct: reduce tm p c d enc a is satisfiable exactly when a ∈ A. It only uses that the run of tm on frame (enc a) ++ w has halted by the allowed number of steps with output [V (a, w)], so it applies to any machine computing V in that time, tidily (reduce_mem_SAT_iff_of_computesTidily) or not.

The input prefix and unary bounds are jointly computable in polynomial time (computableInPolyTime_parameters in CslibFrontier/Computability/Complexity/CookLevin/Parameters.lean). Variable construction and numbering are certified in CslibFrontier/Computability/Complexity/CookLevin/Encoding.lean, and all clause families in CslibFrontier/Computability/Complexity/CookLevin/Clauses.lean. CslibFrontier/Computability/Complexity/CookLevin/PolyTime.lean certifies the complete reduction; CslibFrontier/Computability/Complexity/CookLevin/Completeness.lean derives unconditional NP-completeness of SAT and coNP-completeness of UNSAT.

Main definitions

• Cslib.Complexity.CookLevin.featureIndex, Cslib.Complexity.CookLevin.Var.index: injective numberings of the features and of the tableau variables.
• Cslib.Complexity.CookLevin.parameters: the input prefix, certificate length and time bound.
• Cslib.Complexity.CookLevin.reduce: the reduction.

Main results

• Cslib.Complexity.CookLevin.reduce_mem_SAT_iff: correctness of the reduction.
• Cslib.Complexity.CookLevin.reduce_mem_SAT_iff_of_computesTidily: the same for a verifier computed tidily.

References

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

Numbering the variables

noncomputable def Cslib.Complexity.CookLevin.stateIndex {State : Type} [Fintype State] (q : Option State) : ℕ

The index of a control state, through Fintype.equivFin, with none first.

theorem Cslib.Complexity.CookLevin.stateIndex_injective {State : Type} [Fintype State] : Function.Injective stateIndex

noncomputable def Cslib.Complexity.CookLevin.featureIndex {k : ℕ} {State : Type} [Fintype State] : Turing.MultiTapeTM.Feature k State → ℕ

The number of a feature: its constructor and its arguments, combined with Nat.pair, with work-tape cells numbered through Equiv.intEquivNat, tape symbols through Encodable.encode (blank, false, true as 0, 1, 2), and situations through Fintype.equivFin.

theorem Cslib.Complexity.CookLevin.featureIndex_injective {k : ℕ} {State : Type} [Fintype State] : Function.Injective featureIndex

noncomputable def Cslib.Complexity.CookLevin.Var.index {k : ℕ} {State : Type} [Fintype State] : Var k State → ℕ

The number of a tableau variable.

theorem Cslib.Complexity.CookLevin.Var.index_injective {k : ℕ} {State : Type} [Fintype State] : Function.Injective index

The reduction

@[reducible]

def Cslib.Complexity.CookLevin.parameters {α : Type} (p : Polynomial ℕ) (c d : ℕ) (enc : α ↪ List Bool) (a : α) : List Bool × ℕ × ℕ

The framed input prefix, certificate length and verifier time bound supplied to the tableau. The verifier is allowed c * (n + 1) ^ d steps on an input of encoded length n. The tuple wrapper is reducible so projection clients can compute its components directly.

noncomputable def Cslib.Complexity.CookLevin.reduce {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] {α : Type} (tm : Turing.MultiTapeTM k Bool State) (p : Polynomial ℕ) (c d : ℕ) (enc : α ↪ List Bool) (a : α) : Logic.PL.CNF ℕ

The Cook–Levin reduction for the verifier computed by tm within c * (n + 1) ^ d steps on inputs of length n, with certificates of length p of the instance length: the tableau of tm on inputs frame (enc a) ++ w, unrolled for exactly the allowed number of steps.

theorem Cslib.Complexity.CookLevin.reduce_mem_SAT_iff {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] {α : Type} {enc : α ↪ List Bool} {A : Set α} {p : Polynomial ℕ} {V : α × List Bool → Bool} (hV : IsVerifier enc p V A) {tm : Turing.MultiTapeTM k Bool State} {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 ∈ SAT ↔ a ∈ A

Correctness of the Cook–Levin reduction. If V verifies A with certificates of length p, and on every input frame (enc a) ++ w with |w| = p (enc a).length the machine tm has halted with output [V (a, w)] after c * (|frame (enc a) ++ w| + 1) ^ d steps, then reduce tm p c d enc a is satisfiable exactly when a ∈ A.

theorem Cslib.Complexity.CookLevin.reduce_mem_SAT_iff_of_computesTidily {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] {α : Type} {enc : α ↪ List Bool} {A : Set α} {p : Polynomial ℕ} {V : α × List Bool → Bool} (hV : IsVerifier enc p V A) {tm : Turing.MultiTapeTM k Bool State} {c d : ℕ} {s : α × List Bool → ℕ} (htm : tm.ComputesFunTidilyInTimeAndSpace (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool V (fun (x : α × List Bool) => c * (((Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) x).length + 1) ^ d) s) (a : α) : reduce tm p c d enc a ∈ SAT ↔ a ∈ A

reduce_mem_SAT_iff for a machine computing the verifier tidily within c * (n + 1) ^ d steps.