Boolean Schaefer dichotomy

For every fixed finite Boolean constraint language of arbitrary fixed relation arities, its exact-arity satisfiability problem is in native P when a common unary constant, AND, OR, ternary majority or ternary parity preserves the language, and is native NP-complete otherwise. All solvers, fixed-template compilers, clone classification, gadgets and hardness reductions are proved in the imported stack. Variable labels are binary; malformed scopes are rejected. Empty and nullary relations are allowed. No uniform bound on language preprocessing is claimed.

This is [Che06], Theorem 3.20 (arXiv v1, p. 12), with explicit binary instance encoding and an extension allowing empty/nullary relations under standard unary constant operations. No separation assumption between P and NP is used.

Main results

• Cslib.Complexity.CSPSAT.mem_P_of_hasSchaeferPolymorphism: all six tractable cases.
• Cslib.Complexity.CSPSAT.schaefer_dichotomy: the full criterion-based Boolean dichotomy.
• Cslib.Complexity.CSPSAT.mem_P_or_npComplete: its unconditional P-or-NP-complete corollary.

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

All six common-polymorphism cases have native polynomial-time decision procedures.

theorem Cslib.Complexity.CSPSAT.schaefer_dichotomy {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) : (Logic.PL.CSP.HasSchaeferPolymorphism arity sem → CSPSAT arity sem ∈ P (encCSP encRel Turing.MultiTapeTM.encNat)) ∧ (¬Logic.PL.CSP.HasSchaeferPolymorphism arity sem → NPComplete (encCSP encRel Turing.MultiTapeTM.encNat) (CSPSAT arity sem))

The full Boolean Schaefer dichotomy. The six common operations give native P; otherwise the exact-arity CSP is native NP-complete under its explicit binary encoding.

theorem Cslib.Complexity.CSPSAT.mem_P_or_npComplete {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) : CSPSAT arity sem ∈ P (encCSP encRel Turing.MultiTapeTM.encNat) ∨ NPComplete (encCSP encRel Turing.MultiTapeTM.encNat) (CSPSAT arity sem)

Each fixed finite Boolean CSP is in native P or is native NP-complete, without assuming these complexity classes differ. schaefer_dichotomy supplies the explicit operation criterion.