Polynomial time for the complete Cook–Levin reduction

The existing tableau is constructed from a bit-string prefix and unary certificate/time bounds. All clause families and intermediate lists are charged by the polynomial-time machine calculus. Composing with the exact parameter computation and binary variable relabelling certifies reduce itself. The verifier, tape count, finite state type and polynomial bounds are fixed; one resulting machine and polynomial work for every encoded instance.

Main results

• Cslib.Complexity.CookLevin.computableInPolyTime_tableau: the entire original tableau.
• Cslib.Complexity.CookLevin.computableInPolyTime_reduce: the complete SAT reduction.

References

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

theorem Cslib.Complexity.CookLevin.computableInPolyTime_tableau {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : List Bool × ℕ × ℕ) => tableau tm q.1 q.2.1 q.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) (Logic.PL.encCNFOver encVar)

Construct the whole tableau from its prefix and unary certificate/time bounds.

theorem Cslib.Complexity.CookLevin.computableInPolyTime_reduce {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) (p : Polynomial ℕ) (c d : ℕ) {α : Type} (enc : α ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime (reduce tm p c d enc) enc encCNF

The existing Cook–Levin reduction is polynomial-time for every fixed verifier and bounds.