Documentation

CslibFrontier.Computability.Complexity.Problems.CSP.Majority

Native tractability from a common majority polymorphism #

Each majority-preserved Boolean relation has a defining width-two CNF. For a fixed finite language these formulas are fixed templates, so their instantiation is a native polynomial-time reduction to 2SAT. Exact-arity guards reject malformed instances. Empty/nullary relations and repeated variables are allowed. Native 2SAT membership in NL and NL ⊆ P give native P.

This proves the majority case of [Che06], Theorem 3.20, under the library's explicit framed CSP encoding and binary variable labels. The normal-form equivalence is [Bod26], Lemma 6.32; no uniform complexity bound in a supplied language is asserted.

Main results #

source
theorem Cslib.Complexity.CSPSAT.exists_twoCNF_templates {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (h : Logic.PL.CSP.HasPolymorphism arity sem (majority 3)) :
∃ (template : Rel → Logic.PL.CNF ℕ), Logic.PL.CSP.CNFTemplates arity sem template ∧ ∀ (R : Rel), ∀ c ∈ template R, List.length c ≤ 2

A common majority polymorphism supplies correct fixed width-two CNF templates.

source
theorem Cslib.Complexity.CSPSAT.polyTimeReducible_TwoSAT_of_templates {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (template : Rel → Logic.PL.CNF ℕ) (ht : Logic.PL.CSP.CNFTemplates arity sem template) (hw : ∀ (R : Rel), ∀ c ∈ template R, List.length c ≤ 2) :
PolyTimeReducible (encCSP encRel Turing.MultiTapeTM.encNat) encCNF (CSPSAT arity sem) TwoSAT

Fixed correct width-two templates induce a native polynomial-time reduction to 2SAT.

source
theorem Cslib.Complexity.CSPSAT.mem_P_of_majority {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (h : Logic.PL.CSP.HasPolymorphism arity sem (majority 3)) :
CSPSAT arity sem ∈ P (encCSP encRel Turing.MultiTapeTM.encNat)

Native polynomial-time tractability of a fixed finite majority-preserved language.