The hard branch of Boolean Schaefer

For a fixed finite Boolean language lacking the six common Schaefer polymorphisms, the proved Boolean clone classification implies preservation of every self-dual relation. Apply the proved canonical primitive-positive construction to the eight reference-lifted ternary clause relations: each is nonempty and separates its columns. Their native NP-complete problem then reduces by certified fixed-gadget replacement to the language's exact-arity CSP.

This proves the hard branch of [Che06], Theorem 3.20 (arXiv v1, p. 12), using Theorem 5.1 and Lemma 5.2 (pp. 17–18). The reference lift avoids a general equality-elimination theorem. Empty/nullary language relations are permitted; input variable labels use binary encoding.

Main results

• Cslib.Complexity.CSPSAT.npComplete_of_not_hasSchaeferPolymorphism: unconditional native NP-completeness outside the six cases, with no solver or classification hypothesis.
• Cslib.Complexity.CSPSAT.exists_linear_size_reduction_from_threeSAT: a native reduction whose distinct output variables plus constraints are bounded by a fixed constant times the number of input clauses, hence also by that constant times input variables plus clauses.

theorem Cslib.Complexity.CSPSAT.exists_linear_size_reduction_from_selfDualThreeSAT {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (h : ¬Logic.PL.CSP.HasSchaeferPolymorphism arity sem) : ∃ (f : Logic.PL.CSP SelfDualThreeSAT.SignPattern ℕ → Logic.PL.CSP Rel ℕ) (C : ℕ), Turing.MultiTapeTM.ComputableInPolyTime f SelfDualThreeSAT.enc (encCSP encRel Turing.MultiTapeTM.encNat) ∧ (∀ (F : Logic.PL.CSP SelfDualThreeSAT.SignPattern ℕ), F ∈ SelfDualThreeSAT ↔ f F ∈ CSPSAT arity sem) ∧ ∀ (F : Logic.PL.CSP SelfDualThreeSAT.SignPattern ℕ), (f F).numVars + List.length (f F) ≤ C * List.length F

Fixed-gadget Schaefer hardness has linear combinatorial size. The constant depends on the fixed language and gadgets, not the input or its binary variable names.

theorem Cslib.Complexity.CSPSAT.exists_linear_size_reduction_from_threeSAT {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (h : ¬Logic.PL.CSP.HasSchaeferPolymorphism arity sem) : ∃ (f : Logic.PL.CNF ℕ → Logic.PL.CSP Rel ℕ) (C : ℕ), Turing.MultiTapeTM.ComputableInPolyTime f encCNF (encCSP encRel Turing.MultiTapeTM.encNat) ∧ (∀ (φ : Logic.PL.CNF ℕ), φ ∈ ThreeSAT ↔ f φ ∈ CSPSAT arity sem) ∧ ∀ (φ : Logic.PL.CNF ℕ), (f φ).numVars + List.length (f φ) ≤ C * List.length φ

Linear-size 3SAT hardness in the hard Schaefer cases. The same witness is a native polynomial-time reduction under binary encodings and satisfies n' + m' ≤ C * m, stronger than n' + m' ≤ C * (n + m). Counts mean distinct occurring variables and clauses/constraints, not encoded bit length. The bound and correctness hold for every raw CNF input.

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

The hard branch of Boolean Schaefer's dichotomy, for arbitrary fixed relation arities. The language is fixed, so noncomputable finite gadget selection makes no uniform preprocessing claim. The actual native reduction from 3SAT has the linear combinatorial bound above.