Partition functions of weighted constraint satisfaction problems

A weighting wt : Rel → List D → R reads each relation symbol as a function from local assignments to a semiring R. The partition function of a CSP instance F : CSP Rel V sums, over the assignments of the variables occurring in F to the finite domain D, the product of the weights of the constraints at their scopes: F.partitionFunction wt = ∑ σ, ∏ (R, vs) ∈ F, wt R (vs.map σ).

With 0/1 weights this is the model count of the relation semantics (CSP.partitionFunction_boole). Weighted counting problems such as the hard-core model, or the number of perfect matchings as a Holant problem with edge variables, are instances with other weightings.

Main definitions

• Cslib.Logic.PL.CSP.weight: the product of the constraint weights at an assignment.
• Cslib.Logic.PL.CSP.partitionFunction: the sum of the weights over the assignments of the occurring variables.

Main results

• Cslib.Logic.PL.CSP.partitionFunction_boole: with 0/1 weights it is CSP.modelCount.
• Cslib.Logic.PL.CSP.map_partitionFunction: semiring homomorphisms commute with the partition function, including evaluation of polynomial weights.
• Cslib.Logic.PL.CSP.partitionFunction_le_prod: a separate bound for each relation gives the product of those bounds times the number of assignments.
• Cslib.Logic.PL.CSP.partitionFunction_le: it is at most |D| ^ n * W ^ m when every weight is at most W, for n variables and m constraints.
• Cslib.Logic.PL.CSP.partitionFunction_eq_zero_of_mem: a constraint of weight zero makes it zero.
• Cslib.Logic.PL.CSP.partitionFunction_eq_sum_powerset: over Bool, it is a sum over the sets of occurring variables that are true.

def Cslib.Logic.PL.CSP.weight {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {R : Type u_4} [Monoid R] (wt : Rel → List D → R) (F : CSP Rel V) (σ : V → D) : R

The weight of an assignment σ: the product over the constraints (R, vs) of F of wt R (vs.map σ).

theorem Cslib.Logic.PL.CSP.map_weight {Rel : Type u_1} {V : Type u_2} {D : Type u_3} {R : Type u_4} {S : Type u_5} [Monoid R] [Monoid S] (f : R →* S) (wt : Rel → List D → R) (F : CSP Rel V) (σ : V → D) : f (weight wt F σ) = weight (fun (r : Rel) (w : List D) => f (wt r w)) F σ

Monoid homomorphisms commute with the weight of an assignment.

def Cslib.Logic.PL.CSP.partitionFunction {Rel : Type u_1} {V : Type u_2} {D : Type u_3} [DecidableEq V] [Fintype D] [Inhabited D] {R : Type u_4} [Semiring R] (wt : Rel → List D → R) (F : CSP Rel V) : R

The partition function of a weighted CSP instance: the sum of F.weight wt σ over the assignments σ of the variables occurring in F (extended by default elsewhere).

theorem Cslib.Logic.PL.CSP.map_partitionFunction {Rel : Type u_1} {V : Type u_2} {D : Type u_3} [DecidableEq V] [Fintype D] [Inhabited D] {R : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] (f : R →+* S) (wt : Rel → List D → R) (F : CSP Rel V) : f (partitionFunction wt F) = partitionFunction (fun (r : Rel) (w : List D) => f (wt r w)) F

Semiring homomorphisms commute with the partition function.

theorem Cslib.Logic.PL.CSP.partitionFunction_boole {Rel : Type u_1} {V : Type u_2} {D : Type u_3} [DecidableEq V] [Fintype D] [Inhabited D] (sem : Rel → List D → Bool) (F : CSP Rel V) : partitionFunction (fun (R : Rel) (w : List D) => if sem R w = true then 1 else 0) F = modelCount sem F

With 0/1 weights the partition function is the model count of the relation semantics.

theorem Cslib.Logic.PL.CSP.partitionFunction_le_prod {Rel : Type u_1} {V : Type u_2} {D : Type u_3} [DecidableEq V] [Fintype D] [Inhabited D] {wt : Rel → List D → ℕ} {F : CSP Rel V} {b : Rel → ℕ} (hb : ∀ c ∈ F, ∀ (w : List D), w.length = c.2.length → wt c.1 w ≤ b c.1) : partitionFunction wt F ≤ Fintype.card D ^ F.numVars * (List.map (fun (c : Constraint Rel V) => b c.1) F).prod

The partition function is at most the number of assignments times the product of the local bounds, which may vary with the relation symbol.

theorem Cslib.Logic.PL.CSP.partitionFunction_le {Rel : Type u_1} {V : Type u_2} {D : Type u_3} [DecidableEq V] [Fintype D] [Inhabited D] {wt : Rel → List D → ℕ} {F : CSP Rel V} {W : ℕ} (hW : ∀ c ∈ F, ∀ (w : List D), w.length = c.2.length → wt c.1 w ≤ W) : partitionFunction wt F ≤ Fintype.card D ^ F.numVars * W ^ List.length F

The partition function is at most |D| ^ n * W ^ m when every weight at a local assignment of the right length is at most W.

theorem Cslib.Logic.PL.CSP.partitionFunction_eq_zero_of_mem {Rel : Type u_1} {V : Type u_2} {D : Type u_3} [DecidableEq V] [Fintype D] [Inhabited D] {wt : Rel → List D → ℕ} {F : CSP Rel V} {c : Constraint Rel V} (hc : c ∈ F) (h0 : ∀ (w : List D), w.length = c.2.length → wt c.1 w = 0) : partitionFunction wt F = 0

A constraint of weight zero makes the partition function zero: if some constraint of F weighs zero at every local assignment of the right length, every assignment weighs zero.

theorem Cslib.Logic.PL.CSP.partitionFunction_eq_sum_powerset {Rel : Type u_1} {V : Type u_2} [DecidableEq V] (wt : Rel → List Bool → ℕ) (F : CSP Rel V) : partitionFunction wt F = ∑ S ∈ F.vars.toFinset.powerset, weight wt F fun (v : V) => decide (v ∈ S)

Boolean partition functions as sums over sets of true variables: an assignment of the occurring variables to Bool is the set of variables it makes true.