Documentation

CslibFrontier.Computability.Complexity.Problems.CSP.Affine

Native tractability from a common parity polymorphism #

For each relation, affine normal form on Fin (arity R) supplies a fixed system. Relabeling its local coordinates by natural numbers and substituting constraint scopes gives a polynomial-time reduction to ordinary XORSAT. Malformed arities produce the inconsistent system [([], true)]. All fixed arities, empty/nullary relations and repeated scope variables are supported.

This proves the parity case of [Che06], Theorem 3.20 (arXiv v1, p. 12), using Theorem 4.3 and the ensuing Gaussian-elimination argument, pp. 15–16. The affine characterization is also [Bod26], Definition 26.14 and Lemma 26.15 (arXiv v3 HTML, Section 26.3). The formal input uses framed lists and binary variable labels. The relation alphabet, encoding and templates are fixed; no uniform bound in the size of a supplied language or truth table is asserted.

Main results #

source
theorem Cslib.Complexity.CSPSAT.exists_affine_templates {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (h : Logic.PL.CSP.HasPolymorphism arity sem (parity 3)) :
∃ (template : Rel → Logic.PL.AffineSystem ℕ), Logic.PL.CSP.AffineTemplates arity sem template

A common ternary parity polymorphism supplies correct fixed affine templates, without auxiliary variables or restrictions on arity.

source
def Cslib.Complexity.CSPSAT.toXORSAT {Rel : Type} (arity : Rel → ℕ) (template : Rel → Logic.PL.AffineSystem ℕ) (F : Logic.PL.CSP Rel ℕ) :
XORSAT.System

Compile well-formed scopes to affine equations; reject every malformed instance.

Instances For
    source
    theorem Cslib.Complexity.CSPSAT.polyTimeReducible_XORSAT_of_templates {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (template : Rel → Logic.PL.AffineSystem ℕ) (ht : Logic.PL.CSP.AffineTemplates arity sem template) :
    PolyTimeReducible (encCSP encRel Turing.MultiTapeTM.encNat) XORSAT.encoding (CSPSAT arity sem) XORSAT

    Correct fixed templates give a native polynomial-time reduction to ordinary XORSAT.

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

    Native P membership for every fixed finite parity-preserved Boolean language. The input has exact declared arities and binary natural-number variable labels. Empty and nullary relations are allowed; malformed scopes are rejected.