Computing the Cook–Levin parameters

The reduction in CslibFrontier/Computability/Complexity/CookLevin/Reduction.lean builds a tableau from a framed input prefix, a certificate length and a time bound. This module certifies their joint computation, with the two bounds in unary so that enumerating times and tape positions has polynomial cost. The certificate polynomial and the constants in the verifier's time bound are fixed parameters.

The clause and variable-numbering certificates in CslibFrontier/Computability/Complexity/CookLevin/Clauses.lean and CslibFrontier/Computability/Complexity/CookLevin/Encoding.lean compose with this result in CslibFrontier/Computability/Complexity/CookLevin/PolyTime.lean.

Main results

• Cslib.Complexity.CookLevin.computableInPolyTime_parameters: computing the exact prefix and bounds used by the reduction.

References

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

theorem Cslib.Complexity.CookLevin.computableInPolyTime_parameters {α : Type} (p : Polynomial ℕ) (c d : ℕ) (enc : α ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime (parameters p c d enc) enc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary))

The input prefix, certificate length and verifier time bound used by the Cook–Levin reduction are jointly computable in polynomial time, with the bounds in unary.