Polynomial-time construction of tableau clauses

All clause families of the existing Cook–Levin tableau are polynomial-time functions of their input word and unary time/window bounds. Variables use encVar, so the certificates compose with Cslib.Complexity.CookLevin.computableInPolyTime_relabel to produce binary SAT instances.

The machine, its tape count and its finite state type are fixed. Traversals of tapes and situations therefore use fixed lists; the tape-cell window is enumerated from the input bound. The step certificate enumerates the original constructor templates, preserving their order and multiplicity. These certificates assemble into the complete reduction in CslibFrontier/Computability/Complexity/CookLevin/PolyTime.lean.

Main results

• Cslib.Complexity.CookLevin.computableInPolyTime_initClauses.
• Cslib.Complexity.CookLevin.computableInPolyTime_acceptClauses.
• Cslib.Complexity.CookLevin.computableInPolyTime_sitClauses.
• Cslib.Complexity.CookLevin.computableInPolyTime_uniqueClauses.
• Cslib.Complexity.CookLevin.computableInPolyTime_oneHotClauses.
• Cslib.Complexity.CookLevin.computableInPolyTime_inputClauses.
• Cslib.Complexity.CookLevin.computableInPolyTime_readClauses.
• Cslib.Complexity.CookLevin.computableInPolyTime_stepClauses.

References

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

theorem Cslib.Complexity.CookLevin.computableInPolyTime_groups {k : ℕ} {State : Type} [Fintype State] : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => Turing.MultiTapeTM.Feature.groups p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList encFeature))

Enumerate the feature groups in polynomial time in the unary input and window bounds.

theorem Cslib.Complexity.CookLevin.computableInPolyTime_oneHotClauses {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] {α : Type} {enc : α ↪ List Bool} {u : α → List Bool} {L T t : α → ℕ} (hu : Turing.MultiTapeTM.ComputableInPolyTime u enc Turing.MultiTapeTM.encBits) (hL : Turing.MultiTapeTM.ComputableInPolyTime L enc Turing.MultiTapeTM.encUnary) (hT : Turing.MultiTapeTM.ComputableInPolyTime T enc Turing.MultiTapeTM.encUnary) (ht : Turing.MultiTapeTM.ComputableInPolyTime t enc Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => oneHotClauses (u a) (L a) (T a) (t a)) enc (Logic.PL.encCNFOver encVar)

Build all exactly-one clauses for one tableau row, including the input-dependent windows.

theorem Cslib.Complexity.CookLevin.computableInPolyTime_initClauses {k : ℕ} {State : Type} [Fintype State] (tm : Turing.MultiTapeTM k Bool State) : Turing.MultiTapeTM.ComputableInPolyTime (initClauses tm) Turing.MultiTapeTM.encUnary (Logic.PL.encCNFOver encVar)

Build the existing initial-configuration clauses from a unary window bound.

theorem Cslib.Complexity.CookLevin.computableInPolyTime_acceptClauses {k : ℕ} {State : Type} [Fintype State] : Turing.MultiTapeTM.ComputableInPolyTime acceptClauses Turing.MultiTapeTM.encUnary (Logic.PL.encCNFOver encVar)

Build the two accepting-configuration clauses from a unary time.

theorem Cslib.Complexity.CookLevin.computableInPolyTime_sitClauses {k : ℕ} {State : Type} [Fintype State] : Turing.MultiTapeTM.ComputableInPolyTime sitClauses Turing.MultiTapeTM.encUnary (Logic.PL.encCNFOver encVar)

Build the situation clauses at a unary time, with the finite machine data fixed.

theorem Cslib.Complexity.CookLevin.computableInPolyTime_uniqueClauses {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] : Turing.MultiTapeTM.ComputableInPolyTime uniqueClauses Turing.MultiTapeTM.encUnary (Logic.PL.encCNFOver encVar)

Build the uniqueness clauses at a unary time, with the finite machine data fixed.

theorem Cslib.Complexity.CookLevin.computableInPolyTime_inputClauses {k : ℕ} {State : Type} [Fintype State] {α : Type} {enc : α ↪ List Bool} {u : α → List Bool} {L t j : α → ℕ} (hu : Turing.MultiTapeTM.ComputableInPolyTime u enc Turing.MultiTapeTM.encBits) (hL : Turing.MultiTapeTM.ComputableInPolyTime L enc Turing.MultiTapeTM.encUnary) (ht : Turing.MultiTapeTM.ComputableInPolyTime t enc Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableInPolyTime j enc Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => inputClauses (u a) (L a) (t a) (j a)) enc (Logic.PL.encCNFOver encVar)

Build input-symbol clauses from computed input, certificate length, time and position.

theorem Cslib.Complexity.CookLevin.computableInPolyTime_readClauses {k : ℕ} {State : Type} [Fintype State] {α : Type} {enc : α ↪ List Bool} {u : α → List Bool} {L T t : α → ℕ} (hu : Turing.MultiTapeTM.ComputableInPolyTime u enc Turing.MultiTapeTM.encBits) (hL : Turing.MultiTapeTM.ComputableInPolyTime L enc Turing.MultiTapeTM.encUnary) (hT : Turing.MultiTapeTM.ComputableInPolyTime T enc Turing.MultiTapeTM.encUnary) (ht : Turing.MultiTapeTM.ComputableInPolyTime t enc Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => readClauses (u a) (L a) (T a) (t a)) enc (Logic.PL.encCNFOver encVar)

Enumerate work-tape and input-symbol clauses, charging the complete input-dependent lists.

theorem Cslib.Complexity.CookLevin.computableInPolyTime_stepClauses {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) {α : Type} {enc : α ↪ List Bool} {u : α → List Bool} {L T t : α → ℕ} (hu : Turing.MultiTapeTM.ComputableInPolyTime u enc Turing.MultiTapeTM.encBits) (hL : Turing.MultiTapeTM.ComputableInPolyTime L enc Turing.MultiTapeTM.encUnary) (hT : Turing.MultiTapeTM.ComputableInPolyTime T enc Turing.MultiTapeTM.encUnary) (ht : Turing.MultiTapeTM.ComputableInPolyTime t enc Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => stepClauses tm (u a) (L a) (T a) (t a)) enc (Logic.PL.encCNFOver encVar)

Build the step constraints by enumerating the fixed constructor templates in their original order. Positions and bounds are unary; the machine's finite transition table is fixed.