Instantiating fixed CNF templates for constraint relations

A local CNF template uses natural-number positions, with correctness stated against the tuple of the declared arity. Instantiation replaces each position by the variable at that position of the constraint scope. Repeated variables are allowed. On well-formed inputs this preserves evaluation under every assignment, hence satisfiability, with no auxiliary variables.

Main definitions

• Cslib.Logic.PL.CSP.CNFTemplates: correctness of fixed local CNF formulas.
• Cslib.Logic.PL.Constraint.instantiateCNF: instantiate one relation template.
• Cslib.Logic.PL.CSP.instantiateCNF: concatenate the instantiated constraint templates.

Main results

• Cslib.Logic.PL.CSP.eval_instantiateCNF: exact evaluation equivalence on well-formed inputs.

def Cslib.Logic.PL.CSP.CNFTemplates {Rel : Type u_1} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (template : Rel → CNF ℕ) : Prop

Correct local CNF templates, with natural numbers denoting positions in a relation tuple. Correctness at every assignment also rules out semantic dependence on out-of-range positions.

theorem Cslib.Logic.PL.CSP.cnfTemplates_relabel_fin {Rel : Type u_1} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {φ : (R : Rel) → CNF (Fin (arity R))} (h : ∀ (R : Rel) (a : Fin (arity R) → Bool), a ∈ booleanRelation arity sem R ↔ CNF.eval a (φ R) = true) : CNFTemplates arity sem fun (R : Rel) => CNF.relabel Fin.val (φ R)

Definitions on the declared finite coordinates become natural-position CNF templates by relabeling each finite index by its value.

def Cslib.Logic.PL.Constraint.instantiateCNF {Rel : Type u_1} {V : Type u_2} (fallback : V) (template : Rel → CNF ℕ) (c : Constraint Rel V) : CNF V

Instantiate one relation template at its scope, using fallback outside the scope. The fallback is semantically irrelevant when the scope has the correct arity and the template is correct.

theorem Cslib.Logic.PL.Constraint.eval_instantiateCNF {Rel : Type u_1} {V : Type u_2} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {template : Rel → CNF ℕ} (h : CSP.CNFTemplates arity sem template) (fallback : V) {c : Constraint Rel V} (hc : c.2.length = arity c.1) (σ : V → Bool) : CNF.eval σ (instantiateCNF fallback template c) = eval sem σ c

Exact evaluation equivalence for a well-formed instantiated constraint.

def Cslib.Logic.PL.CSP.instantiateCNF {Rel : Type u_1} {V : Type u_2} (fallback : V) (template : Rel → CNF ℕ) (F : CSP Rel V) : CNF V

Instantiate and concatenate a fixed CNF template for every constraint.

theorem Cslib.Logic.PL.CSP.length_clause_mem_instantiateCNF {Rel : Type u_1} {V : Type u_2} {template : Rel → CNF ℕ} {k : ℕ} (h : ∀ (R : Rel), ∀ c ∈ template R, List.length c ≤ k) (fallback : V) {F : CSP Rel V} {c : Clause V} (hc : c ∈ instantiateCNF fallback template F) : List.length c ≤ k

Instantiation preserves any common clause-width bound of the templates.

theorem Cslib.Logic.PL.CSP.eval_instantiateCNF {Rel : Type u_1} {V : Type u_2} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {template : Rel → CNF ℕ} (h : CNFTemplates arity sem template) (fallback : V) {F : CSP Rel V} (hF : WellFormed arity F) (σ : V → Bool) : CNF.eval σ (instantiateCNF fallback template F) = eval sem σ F

Instantiation preserves evaluation under every assignment to well-formed instances.

theorem Cslib.Logic.PL.CSP.satisfiable_instantiateCNF {Rel : Type u_1} {V : Type u_2} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {template : Rel → CNF ℕ} (h : CNFTemplates arity sem template) (fallback : V) {F : CSP Rel V} (hF : WellFormed arity F) : (instantiateCNF fallback template F).Satisfiable ↔ Satisfiable sem F

Instantiation preserves satisfiability of well-formed instances.