2.8. Boolean Constraint Languages🔗

Schaefer's full Boolean dichotomy is proved for fixed finite constraint languages over Bool, with arbitrary fixed relation arities and explicit binary instance encoding. The six common-polymorphism cases are native P; otherwise the problem is native NP-complete. Its structural ingredients include majority preservation being equivalent to definability by clauses of width at most two, with no auxiliary variables (Cslib.Logic.PL.isPolymorphism_majority_iff_exists_twoCNF).

open Cslib.Logic Cslib.Logic.PL in
example {V : Type} [Finite V] (R : Set (V → Bool))
    (h : IsPolymorphism (Cslib.majority 3) R) :
    ∃ φ : CNF V, (∀ c ∈ φ, c.length ≤ 2) ∧
      ∀ a, a ∈ R ↔ φ.eval a = true :=
  (isPolymorphism_majority_iff_exists_twoCNF R).mp h

Here preservation applies the operation coordinatewise to satisfying tuples. Cslib.Logic.IsPolymorphism.project preserves it under existential projection, and Cslib.Logic.IsPolymorphism.substitute covers repeated variables. Empty and nullary relations are allowed. This characterization alone does not supply a polynomial-time certificate for constructing the formula.

For native complexity, CSPSAT fixes a relation alphabet, arities and list semantics, and rejects input scopes with incorrect lengths. Variable labels are arbitrary natural numbers encoded in binary by encCSP with encNat. Every fixed finite Boolean language is in NP (CSPSAT.mem_NP). Common unary constants and majority give native P via CSPSAT.mem_P_of_constant and CSPSAT.mem_P_of_majority. Empty relations are handled explicitly.

open Cslib.Logic.PL in
example {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool)
    (arity : Rel → ℕ) (sem : Rel → List Bool → Bool)
    (h : CSP.HasPolymorphism arity sem (Cslib.majority 3)) :
    CSPSAT arity sem ∈ P (encCSP encRel encNat) :=
  CSPSAT.mem_P_of_majority encRel arity sem h

The language is fixed: template lookup is finite preprocessing. The reduction instantiates its local clauses in native polynomial time and uses the existing native 2SAT theorem; no solver hypothesis is needed.

The positive-arity Boolean clone classification is proved in CslibFrontier.Logics.BooleanClone.Classification: Cslib.Logic.BooleanClone.classification covers every positive arity. For a language lacking the six common operations, Cslib.Logic.PL.CSP.projection_or_negation_of_not_hasSchaeferPolymorphism identifies every polymorphism as a projection or negated projection. This supplies the algebraic ingredient used by the native hardness application below.

Post's functional-completeness criterion shares this same classification: Cslib.Logic.BooleanClone.functionallyComplete_iff characterizes generating families by witnesses outside the five closed classes. Its completeness notion quantifies over positive input arities, with unary constant functions. In particular, NAND is complete in that sense; the stronger circuit notion also requires zero-input functions. No circuit-size bound is asserted by this criterion.

For reductions between fixed Boolean languages, Cslib.Logic.PL.CSP.exists_ppGadget_of_polymorphisms constructs equality-free primitive-positive gadgets for nonempty target relations with separating columns. Cslib.Complexity.CSP.computableInPolyTime_replaceGadgetsGuarded certifies fixed-gadget replacement with binary labels, fresh auxiliaries and exact-arity rejection. The hardness application must discharge nonemptiness, separation and polymorphism invariance; general equality elimination is outside this gadget API. The shared guard certificate is Cslib.Complexity.CSP.computableInPolyTime_validArity in CslibFrontier.Computability.PolyTime.CSP.Boolean.

The hard branch is native and unconditional: CSPSAT.npComplete_of_not_hasSchaeferPolymorphism proves NP-completeness for any fixed finite language lacking all six common operations. The proof imports the proved clone classification, constructs gadgets for the eight self-dual reference lifts of signed ternary clauses, and compiles them in native polynomial time. Their nonemptiness and separating columns are proved internally. Empty and nullary language relations remain allowed.

open Cslib.Logic.PL in
example {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool)
    (arity : Rel → ℕ) (sem : Rel → List Bool → Bool)
    (h : ¬ CSP.HasSchaeferPolymorphism arity sem) :
    NPComplete (encCSP encRel encNat) (CSPSAT arity sem) :=
  CSPSAT.npComplete_of_not_hasSchaeferPolymorphism encRel arity sem h

CSPSAT.exists_linear_size_reduction_from_threeSAT gives the actual hardness reduction together with correctness, native polynomial-time computation and output.numVars + output.length ≤ C * input.length. Thus the number of distinct output variables plus constraints is at most a fixed constant times the number of input clauses, and hence at most C * (input.numVars + input.length). The constant depends only on the fixed language. The bound holds on all raw CNFs, including malformed and empty inputs; it concerns combinatorial counts rather than encoded bit length or running time.

open Cslib.Logic.PL Turing.MultiTapeTM in
example {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool)
    (arity : Rel → ℕ) (sem : Rel → List Bool → Bool)
    (h : ¬ CSP.HasSchaeferPolymorphism arity sem) :
    ∃ (f : CNF ℕ → CSP Rel ℕ) (C : ℕ),
      ComputableInPolyTime f encCNF (encCSP encRel encNat) ∧
      (∀ φ, φ ∈ ThreeSAT ↔ f φ ∈ CSPSAT arity sem) ∧
      (∀ φ, (f φ).numVars + (f φ).length ≤ C * (φ.numVars + φ.length)) := byRel:Typeinst✝:Finite RelencRel:Rel ↪ List Boolarity:Rel → ℕsem:Rel → List Bool → Boolh:¬CSP.HasSchaeferPolymorphism arity sem⊢ ∃ f C,
  ComputableInPolyTime f encCNF (encCSP encRel encNat) ∧
    (∀ (φ : CNF ℕ), φ ∈ ThreeSAT ↔ f φ ∈ CSPSAT arity sem) ∧
      ∀ (φ : CNF ℕ), (f φ).numVars + List.length (f φ) ≤ C * (φ.numVars + List.length φ)
  obtain ⟨f, C, hp, hm, hs⟩ :=
    CSPSAT.exists_linear_size_reduction_from_threeSAT encRel arity sem hRel:Typeinst✝:Finite RelencRel:Rel ↪ List Boolarity:Rel → ℕsem:Rel → List Bool → Boolh:¬CSP.HasSchaeferPolymorphism arity semf:CNF ℕ → CSP Rel ℕC:ℕhp:ComputableInPolyTime f encCNF (encCSP encRel encNat)hm:∀ (φ : CNF ℕ), φ ∈ ThreeSAT ↔ f φ ∈ CSPSAT arity semhs:∀ (φ : CNF ℕ), (f φ).numVars + List.length (f φ) ≤ C * List.length φ⊢ ∃ f C,
  ComputableInPolyTime f encCNF (encCSP encRel encNat) ∧
    (∀ (φ : CNF ℕ), φ ∈ ThreeSAT ↔ f φ ∈ CSPSAT arity sem) ∧
      ∀ (φ : CNF ℕ), (f φ).numVars + List.length (f φ) ≤ C * (φ.numVars + List.length φ)
  refine ⟨f, C, hp, hm, fun φ => (hs φ).trans ?_⟩Rel:Typeinst✝:Finite RelencRel:Rel ↪ List Boolarity:Rel → ℕsem:Rel → List Bool → Boolh:¬CSP.HasSchaeferPolymorphism arity semf:CNF ℕ → CSP Rel ℕC:ℕhp:ComputableInPolyTime f encCNF (encCSP encRel encNat)hm:∀ (φ : CNF ℕ), φ ∈ ThreeSAT ↔ f φ ∈ CSPSAT arity semhs:∀ (φ : CNF ℕ), (f φ).numVars + List.length (f φ) ≤ C * List.length φφ:CNF ℕ⊢ C * List.length φ ≤ C * (φ.numVars + List.length φ)
  apply Nat.mul_le_mul_leftRel:Typeinst✝:Finite RelencRel:Rel ↪ List Boolarity:Rel → ℕsem:Rel → List Bool → Boolh:¬CSP.HasSchaeferPolymorphism arity semf:CNF ℕ → CSP Rel ℕC:ℕhp:ComputableInPolyTime f encCNF (encCSP encRel encNat)hm:∀ (φ : CNF ℕ), φ ∈ ThreeSAT ↔ f φ ∈ CSPSAT arity semhs:∀ (φ : CNF ℕ), (f φ).numVars + List.length (f φ) ≤ C * List.length φφ:CNF ℕ⊢ List.length φ ≤ φ.numVars + List.length φ
  omegaAll goals completed! 🐙

The remaining tractable normal forms have proved native solvers: Cslib.Logic.PL.isPolymorphism_and_iff_exists_hornCNF and Cslib.Logic.PL.isPolymorphism_or_iff_exists_dualHornCNF characterize AND/OR preservation. HornSAT.mem_P and DualHornSAT.mem_P decide all-width formulas under encCNF. Horn syntax counts positive occurrences, so repeating a positive literal twice is rejected as non-Horn syntax.

Cslib.Logic.PL.isPolymorphism_parity_iff_exists_affineSystem characterizes ternary parity preservation by affine equations. XORSAT.mem_P certifies ordinary sparse XOR-SAT with binary variable names; repeated variables cancel modulo two. The dense Gaussian elimination algorithm and sparse compiler both have native certificates. Their fixed-language compilers give CSPSAT.mem_P_of_and, CSPSAT.mem_P_of_or and CSPSAT.mem_P_of_parity, including repeated scope variables, sparse binary labels and empty/nullary relations. Malformed scopes are rejected before instantiation.

CSPSAT.schaefer_dichotomy assembles all six cases and the hard branch. Its unconditional corollary uses no assumption separating P and NP:

open Cslib.Logic.PL in
example {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool)
    (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) :
    CSPSAT arity sem ∈ P (encCSP encRel encNat) ∨
      NPComplete (encCSP encRel encNat) (CSPSAT arity sem) :=
  CSPSAT.mem_P_or_npComplete encRel arity sem