Polynomial-time forbidden-pattern compilation of Boolean CSPs

The existing width-guarded compiler Cslib.Logic.PL.CSP.toCNFBounded is polynomial-time for fixed width when its finite relation tables can be evaluated in polynomial time. These certificates serve both exact counting and approximation-preserving reductions.

Main definitions

• Cslib.Complexity.encConstraint, Cslib.Complexity.encCSP: framed binary encodings of constraints and their lists.

Main results

• Cslib.Complexity.CSP.computableInPolyTime_toCNFBounded_of_forall: compilation from polynomial-time evaluations of the finitely many relevant local patterns.
• Cslib.Complexity.CSP.computableInPolyTime_toCNFBounded: compilation from a polynomial-time relation evaluator.
• Cslib.Complexity.CSP.computableInPolyTime_toCNFBounded_of_finite: compilation for a finite relation alphabet.

@[reducible, inline]

abbrev Cslib.Complexity.encConstraint {Rel V : Type} (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) : Logic.PL.Constraint Rel V ↪ List Bool

Binary encoding of a constraint (R, vs) : Constraint Rel V.

@[reducible, inline]

abbrev Cslib.Complexity.encCSP {Rel V : Type} (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) : Logic.PL.CSP Rel V ↪ List Bool

Binary encoding of a CSP instance F : CSP Rel V.

theorem Cslib.Complexity.CSP.computableInPolyTime_toCNFBounded_of_forall {Rel V : Type} (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) (k : ℕ) (sem : Rel → List Bool → Bool) (hsem : ∀ (w : List Bool), w.length ≤ k → Turing.MultiTapeTM.ComputableInPolyTime (fun (R : Rel) => sem R w) encRel Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (Logic.PL.CSP.toCNFBounded k sem) (encCSP encRel encV) (Logic.PL.encCNFOver encV)

Width-guarded compilation of a Boolean CSP instance to a k-CNF formula is computable in polynomial time whenever fun R => sem R w is computable in polynomial time for each bit pattern w of length at most k.

theorem Cslib.Complexity.CSP.computableInPolyTime_toCNFBounded {Rel V : Type} (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) (k : ℕ) (sem : Rel → List Bool → Bool) (hsem : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Rel × List Bool) => sem p.1 p.2) (Turing.MultiTapeTM.encPair encRel Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (Logic.PL.CSP.toCNFBounded k sem) (encCSP encRel encV) (Logic.PL.encCNFOver encV)

Width-guarded compilation of a Boolean CSP instance to a k-CNF formula is computable in polynomial time whenever sem is computable in polynomial time.

theorem Cslib.Complexity.CSP.computableInPolyTime_toCNFBounded_of_finite {Rel V : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) (k : ℕ) (sem : Rel → List Bool → Bool) : Turing.MultiTapeTM.ComputableInPolyTime (Logic.PL.CSP.toCNFBounded k sem) (encCSP encRel encV) (Logic.PL.encCNFOver encV)

Width-guarded compilation of a Boolean CSP instance to a k-CNF formula is computable in polynomial time for any finite relation alphabet Rel.