Exactly-one constraints

The exactly-one weighting CSP.exactlyOneWeight weighs a local assignment one when exactly one of its values is true, and zero otherwise. Over Bool, the partition function of an instance with these weights counts the sets S of occurring variables that meet every scope in exactly one variable (CSP.partitionFunction_exactlyOne). With one variable per edge of a graph and one constraint per vertex on its incident edges, these sets are the perfect matchings, so perfect matchings and 0/1 permanents are such Holant instances.

Main definitions

• Cslib.Logic.PL.CSP.exactlyOneWeight: the exactly-one weights.

Main results

• Cslib.Logic.PL.CSP.partitionFunction_exactlyOne: the partition function counts the sets of variables that meet every scope exactly once.

def Cslib.Logic.PL.CSP.exactlyOneWeight : Unit → (w : List Bool) → ℕ

The exactly-one weights: one when exactly one entry of the local assignment is true, zero otherwise.

theorem Cslib.Logic.PL.CSP.partitionFunction_exactlyOne {V : Type u_1} [DecidableEq V] (F : CSP Unit V) : partitionFunction exactlyOneWeight F = {S ∈ F.vars.toFinset.powerset | ∀ c ∈ F, (List.filter (fun (v : V) => decide (v ∈ S)) c.2).length = 1}.card

Exactly-one partition functions count exact covers of the scopes: the partition function is the number of sets S of occurring variables such that every scope has exactly one entry in S.