Native tractability from common AND and OR polymorphisms

Every AND-preserved Boolean relation has a Horn CNF definition; every OR-preserved relation has a dual Horn definition. For each fixed finite language these definitions are fixed templates. Their certified instantiation reduces the original CSP to ordinary native HornSAT or dual HornSAT. The exact-arity guard rejects malformed scopes with an empty clause. No bound on clause width is imposed; repeated variables, empty relations, nullary relations and sparse binary labels are allowed.

These are the AND and OR cases of [Che06], Theorem 3.20, with the original framed CSP encoding, fixed arbitrary relation arities and binary variable names. The normal forms are [Bod26], Lemma 6.31 and its dual; the local normal-form module proves them without auxiliary variables. Template selection is internal and nonuniform in the fixed language: no solver, template or efficiency hypothesis is required, and no uniform bound in a supplied language is claimed.

Main results

• Cslib.Complexity.CSPSAT.exists_hornCNF_templates: fixed Horn templates from AND.
• Cslib.Complexity.CSPSAT.exists_dualHornCNF_templates: fixed dual Horn templates from OR.
• Cslib.Complexity.CSPSAT.mem_P_of_and: native polynomial time from a common AND polymorphism.
• Cslib.Complexity.CSPSAT.mem_P_of_or: native polynomial time from a common OR polymorphism.

theorem Cslib.Complexity.CSPSAT.exists_hornCNF_templates {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (h : Logic.PL.CSP.HasPolymorphism arity sem fun (a : Fin 2 → Bool) => a 0 && a 1) : ∃ (template : Rel → Logic.PL.CNF ℕ), Logic.PL.CSP.CNFTemplates arity sem template ∧ ∀ (R : Rel), (template R).IsHorn

A common AND polymorphism supplies correct fixed Horn templates, with no auxiliaries.

theorem Cslib.Complexity.CSPSAT.exists_dualHornCNF_templates {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (h : Logic.PL.CSP.HasPolymorphism arity sem fun (a : Fin 2 → Bool) => a 0 || a 1) : ∃ (template : Rel → Logic.PL.CNF ℕ), Logic.PL.CSP.CNFTemplates arity sem template ∧ ∀ (R : Rel), (template R).IsDualHorn

A common OR polymorphism supplies correct fixed dual Horn templates, with no auxiliaries.

theorem Cslib.Complexity.CSPSAT.polyTimeReducible_HornSAT_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) (hh : ∀ (R : Rel), (template R).IsHorn) : PolyTimeReducible (encCSP encRel Turing.MultiTapeTM.encNat) encCNF (CSPSAT arity sem) HornSAT

Fixed correct Horn templates give a native polynomial-time reduction to ordinary HornSAT. The guard rejects every malformed scope, regardless of the semantics on lists of wrong length.

theorem Cslib.Complexity.CSPSAT.polyTimeReducible_DualHornSAT_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) (hh : ∀ (R : Rel), (template R).IsDualHorn) : PolyTimeReducible (encCSP encRel Turing.MultiTapeTM.encNat) encCNF (CSPSAT arity sem) DualHornSAT

Fixed correct dual Horn templates give a native polynomial-time reduction to dual HornSAT.

theorem Cslib.Complexity.CSPSAT.mem_P_of_and {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (h : Logic.PL.CSP.HasPolymorphism arity sem fun (a : Fin 2 → Bool) => a 0 && a 1) : CSPSAT arity sem ∈ P (encCSP encRel Turing.MultiTapeTM.encNat)

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

theorem Cslib.Complexity.CSPSAT.mem_P_of_or {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (h : Logic.PL.CSP.HasPolymorphism arity sem fun (a : Fin 2 → Bool) => a 0 || a 1) : CSPSAT arity sem ∈ P (encCSP encRel Turing.MultiTapeTM.encNat)

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