Constraint satisfaction problems

A constraint satisfaction problem (CSP) instance F : CSP Rel V over a relation alphabet Rel and variable type V is a conjunction (list) of constraints (R, vs) : Rel × List V, interpreted over a domain D under a family of relations sem : Rel → List D → Bool by requiring sem R (vs.map σ) = true for every (R, vs) ∈ F.

Relations are not assigned fixed arities at the type level: sem R is evaluated at the length of each constraint's scope c.2. Under a uniform scope-length bound c.2.length ≤ k, each relation symbol induces a relation of arity at most k.

For any finite inhabited domain D, CSP.modelCountOn sem F declared counts assignments on a declared finite set of variables declared : Finset V (extended by default outside declared) that satisfy F, and CSP.modelCount sem F counts satisfying assignments on the occurring variables F.vars.toFinset. In the Boolean case D = Bool, default = false, matching CNF.modelCountOn and CNF.modelCount.

Main definitions

• Cslib.Logic.PL.Constraint, Cslib.Logic.PL.CSP: constraints and CSP instances.
• Cslib.Logic.PL.Constraint.eval, Cslib.Logic.PL.CSP.eval, Cslib.Logic.PL.CSP.Satisfiable: evaluation and satisfiability over an arbitrary domain D.
• Cslib.Logic.PL.CSP.vars, Cslib.Logic.PL.CSP.numVars, Cslib.Logic.PL.CSP.distinctVars: variable occurrences, count of distinct variables, and first-occurrence variable list.
• Cslib.Logic.PL.Constraint.relabel, Cslib.Logic.PL.CSP.relabel, Cslib.Logic.PL.CSP.denseRelabel: variable renaming and dense 0, …, numVars - 1 relabeling.
• Cslib.Logic.PL.CSP.modelCountOn, Cslib.Logic.PL.CSP.modelCount: declared-variable and occurring-variable model counts over a finite inhabited domain D.
• Cslib.Logic.PL.CSP.validDeclaredCSP: executable guard checking scope lengths ≤ k and variable indices < N.
• Cslib.Logic.PL.CSP.KCSP: the bounded-arity CSP decision problem.

Main results

• Cslib.Logic.PL.CSP.vars_denseRelabel_toFinset, Cslib.Logic.PL.CSP.numVars_denseRelabel: dense relabeling maps occurring variables onto Finset.range F.numVars.
• Cslib.Logic.PL.CSP.modelCountOn_denseRelabel, Cslib.Logic.PL.CSP.modelCount_denseRelabel: dense relabeling preserves declared and occurring model counts.
• Cslib.Logic.PL.CSP.modelCount_pos_iff: a CSP instance is satisfiable iff its model count is positive.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• OpenAI, The Exponential Time Hypothesis is False, Appendix C.

@[reducible, inline]

abbrev Cslib.Logic.PL.Constraint (Rel : Type u_1) (V : Type u_2) : Type (max u_2 u_1)

A constraint over relation alphabet Rel and variable type V pairs a relation symbol R : Rel with its scope of variables vs : List V. Relations are not assigned fixed arities at the type level; a semantics sem : Rel → List D → Bool is read at the length of each scope vs.

@[reducible, inline]

abbrev Cslib.Logic.PL.CSP (Rel : Type u_1) (V : Type u_2) : Type (max u_2 u_1)

A constraint satisfaction problem (CSP) instance over relation alphabet Rel and variable type V is a conjunction (list) of constraints.

def Cslib.Logic.PL.Constraint.eval {Rel : Type u_1} {V : Type u_2} {D : Type u_4} (sem : Rel → List D → Bool) (σ : V → D) (c : Constraint Rel V) : Bool

Evaluate a constraint (R, vs) under assignment σ : V → D and semantics sem : Rel → List D → Bool.

def Cslib.Logic.PL.Constraint.relabel {Rel : Type u_1} {V : Type u_2} {W : Type u_3} (f : V → W) (c : Constraint Rel V) : Constraint Rel W

Rename variables in a constraint's scope.

@[simp]

theorem Cslib.Logic.PL.Constraint.eval_relabel {Rel : Type u_1} {V : Type u_2} {W : Type u_3} {D : Type u_4} (sem : Rel → List D → Bool) (f : V → W) (σ : W → D) (c : Constraint Rel V) : eval sem σ (relabel f c) = eval sem (σ ∘ f) c

Evaluating a relabeled constraint composes the assignment with the relabeling.

theorem Cslib.Logic.PL.Constraint.eval_congr {Rel : Type u_1} {V : Type u_2} {D : Type u_4} {sem : Rel → List D → Bool} {c : Constraint Rel V} {σ τ : V → D} (h : ∀ v ∈ c.2, σ v = τ v) : eval sem σ c = eval sem τ c

Constraint evaluation depends only on the values assigned to the variables in its scope.

def Cslib.Logic.PL.CSP.eval {Rel : Type u_1} {V : Type u_2} {D : Type u_4} (sem : Rel → List D → Bool) (σ : V → D) (F : CSP Rel V) : Bool

Evaluate a CSP instance under assignment σ : V → D.

def Cslib.Logic.PL.CSP.Satisfiable {Rel : Type u_1} {V : Type u_2} {D : Type u_4} (sem : Rel → List D → Bool) (F : CSP Rel V) : Prop

A CSP instance is satisfiable if some assignment σ : V → D satisfies all its constraints.

def Cslib.Logic.PL.CSP.vars {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : List V

All variable occurrences across the constraint scopes of F, in order.

def Cslib.Logic.PL.CSP.relabel {Rel : Type u_1} {V : Type u_2} {W : Type u_3} (f : V → W) (F : CSP Rel V) : CSP Rel W

Rename variables across all constraints in F.

@[simp]

theorem Cslib.Logic.PL.CSP.vars_relabel {Rel : Type u_1} {V : Type u_2} {W : Type u_3} (f : V → W) (F : CSP Rel V) : (relabel f F).vars = List.map f F.vars

Relabeling maps CSP.vars by the relabeling function.

@[simp]

theorem Cslib.Logic.PL.CSP.eval_relabel {Rel : Type u_1} {V : Type u_2} {W : Type u_3} {D : Type u_4} (sem : Rel → List D → Bool) (f : V → W) (σ : W → D) (F : CSP Rel V) : eval sem σ (relabel f F) = eval sem (σ ∘ f) F

Evaluating a relabeled CSP instance composes the assignment with the relabeling.

theorem Cslib.Logic.PL.CSP.eval_congr {Rel : Type u_1} {V : Type u_2} {D : Type u_4} {sem : Rel → List D → Bool} {F : CSP Rel V} {σ τ : V → D} (h : ∀ v ∈ F.vars, σ v = τ v) : eval sem σ F = eval sem τ F

CSP evaluation depends only on the values assigned to its occurring variables F.vars.

def Cslib.Logic.PL.CSP.varCNF {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : CNF V

Auxiliary positive-clause CNF formula with the same variable-occurrence list F.vars. Used as a proof device to transfer CNF variable-accounting and polynomial-time lemmas to CSP.

@[simp]

theorem Cslib.Logic.PL.CSP.vars_varCNF {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : F.varCNF.vars = F.vars

The variable occurrences of F.varCNF are identical to F.vars.

def Cslib.Logic.PL.CSP.numVars {Rel : Type u_1} {V : Type u_2} [DecidableEq V] (F : CSP Rel V) : ℕ

Number of distinct variables occurring in F.

def Cslib.Logic.PL.CSP.distinctVars {Rel : Type u_1} {V : Type u_2} [DecidableEq V] (F : CSP Rel V) : List V

Distinct variables of F in order of first occurrence.

@[simp]

theorem Cslib.Logic.PL.CSP.numVars_varCNF {Rel : Type u_1} {V : Type u_2} [DecidableEq V] (F : CSP Rel V) : F.varCNF.numVars = F.numVars

F.varCNF has the same number of distinct variables as F.

@[simp]

theorem Cslib.Logic.PL.CSP.distinctVars_varCNF {Rel : Type u_1} {V : Type u_2} [DecidableEq V] (F : CSP Rel V) : F.varCNF.distinctVars = F.distinctVars

F.varCNF has the same first-occurrence variable list as F.

theorem Cslib.Logic.PL.CSP.mem_distinctVars {Rel : Type u_1} {V : Type u_2} [DecidableEq V] {F : CSP Rel V} {v : V} : v ∈ F.distinctVars ↔ v ∈ F.vars

A variable belongs to F.distinctVars iff it occurs in F.vars.

theorem Cslib.Logic.PL.CSP.length_distinctVars {Rel : Type u_1} {V : Type u_2} [DecidableEq V] (F : CSP Rel V) : F.distinctVars.length = F.numVars

The length of F.distinctVars is F.numVars.

def Cslib.Logic.PL.CSP.denseRelabel {Rel : Type u_1} {V : Type u_2} [DecidableEq V] (F : CSP Rel V) : CSP Rel ℕ

Rename each variable occurring in F by its first-occurrence index in F.distinctVars.

@[simp]

theorem Cslib.Logic.PL.CSP.vars_denseRelabel_toFinset {Rel : Type u_1} {V : Type u_2} [DecidableEq V] (F : CSP Rel V) : F.denseRelabel.vars.toFinset = Finset.range F.numVars

The occurring variables of F.denseRelabel are Finset.range F.numVars.

@[simp]

theorem Cslib.Logic.PL.CSP.numVars_denseRelabel {Rel : Type u_1} {V : Type u_2} [DecidableEq V] (F : CSP Rel V) : F.denseRelabel.numVars = F.numVars

Dense relabeling preserves the number of distinct occurring variables.

theorem Cslib.Logic.PL.CSP.all_length_le_denseRelabel {Rel : Type u_1} {V : Type u_2} [DecidableEq V] {k : ℕ} (F : CSP Rel V) : (∀ c ∈ F.denseRelabel, c.2.length ≤ k) ↔ ∀ c ∈ F, c.2.length ≤ k

Dense relabeling preserves any uniform upper bound on constraint scope lengths.

def Cslib.Logic.PL.CSP.modelCountOn {Rel : Type u_1} {V : Type u_2} {D : Type u_4} [DecidableEq V] [Fintype D] [Inhabited D] (sem : Rel → List D → Bool) (F : CSP Rel V) (declared : Finset V) : ℕ

Count assignments to declared : Finset V (extended by default outside declared) that satisfy F under sem.

def Cslib.Logic.PL.CSP.modelCount {Rel : Type u_1} {V : Type u_2} {D : Type u_4} [DecidableEq V] [Fintype D] [Inhabited D] (sem : Rel → List D → Bool) (F : CSP Rel V) : ℕ

Count satisfying assignments on the occurring variables F.vars.toFinset.

theorem Cslib.Logic.PL.CSP.modelCountOn_denseRelabel {Rel : Type u_1} {V : Type u_2} {D : Type u_4} [DecidableEq V] [Fintype D] [Inhabited D] (sem : Rel → List D → Bool) (F : CSP Rel V) : modelCountOn sem F.denseRelabel (Finset.range F.numVars) = modelCount sem F

Dense variable relabeling preserves the occurring-variable model count on Finset.range F.numVars.

@[simp]

theorem Cslib.Logic.PL.CSP.modelCount_denseRelabel {Rel : Type u_1} {V : Type u_2} {D : Type u_4} [DecidableEq V] [Fintype D] [Inhabited D] (sem : Rel → List D → Bool) (F : CSP Rel V) : modelCount sem F.denseRelabel = modelCount sem F

Dense variable relabeling preserves CSP.modelCount.

theorem Cslib.Logic.PL.CSP.modelCount_pos_iff {Rel : Type u_1} {V : Type u_2} {D : Type u_4} [DecidableEq V] [Fintype D] [Inhabited D] {sem : Rel → List D → Bool} {F : CSP Rel V} : 0 < modelCount sem F ↔ Satisfiable sem F

A CSP instance is satisfiable if and only if its model count is positive.

def Cslib.Logic.PL.CSP.validDeclaredCSP {Rel : Type u_1} (k N : ℕ) (F : CSP Rel ℕ) : Bool

Guard checking that every constraint scope in F has length ≤ k and every occurring variable lies in < N.

theorem Cslib.Logic.PL.CSP.validDeclaredCSP_eq_true_iff {Rel : Type u_1} {k N : ℕ} {F : CSP Rel ℕ} : validDeclaredCSP k N F = true ↔ (∀ c ∈ F, c.2.length ≤ k) ∧ F.vars.toFinset ⊆ Finset.range N

validDeclaredCSP k N F holds iff every constraint scope has length ≤ k and all occurring variables lie in Finset.range N.

def Cslib.Logic.PL.CSP.KCSP {Rel : Type u_1} {V : Type u_2} {D : Type u_4} (k : ℕ) (sem : Rel → List D → Bool) : Set (CSP Rel V)

The bounded-arity CSP decision problem over relation semantics sem.