General-Valued Constraint Satisfaction Problems

General-Valued CSP is a very broad class of problems in discrete optimization. General-Valued CSP subsumes Min-Cost-Hom (including 3-SAT for example) and Finite-Valued CSP.

Main definitions

• ValuedCSP: A VCSP template; fixes a domain, a codomain, and allowed cost functions.
• ValuedCSP.Term: One summand in a VCSP instance; calls a concrete function from given template.
• ValuedCSP.Term.evalSolution: An evaluation of the VCSP term for given solution.
• ValuedCSP.Instance: An instance of a VCSP problem over given template.
• ValuedCSP.Instance.evalSolution: An evaluation of the VCSP instance for given solution.
• ValuedCSP.Instance.IsOptimumSolution: Is given solution a minimum of the VCSP instance?

References

• [D. A. Cohen, M. C. Cooper, P. Creed, P. G. Jeavons, S. Živný, An Algebraic Theory of Complexity for Discrete Optimisation][cohen2012]

@[inline, reducible]

abbrev ValuedCSP (D : Type u_1) (C : Type u_2) [OrderedAddCommMonoid C] : Type (max u_1 u_2)

A template for a valued CSP problem over a domain D with costs in C. Regarding C we want to support Bool, Nat, ENat, Int, Rat, NNRat, Real, NNReal, EReal, ENNReal, and tuples made of any of those types.

Equations

• ValuedCSP D C = Set ((n : ℕ) × ((Fin n → D) → C))

structure ValuedCSP.Term {D : Type u_1} {C : Type u_2} [OrderedAddCommMonoid C] (Γ : ValuedCSP D C) (ι : Type u_3) : Type (max (max u_1 u_2) u_3)

A term in a valued CSP instance over the template Γ.

• n : ℕ

  Arity of the function

• f : (Fin self.n → D) → C

  Which cost function is instantiated

• inΓ : { fst := self.n, snd := self.f } ∈ Γ

  The cost function comes from the template

• app : Fin self.n → ι

  Which variables are plugged as arguments to the cost function

def ValuedCSP.Term.evalSolution {D : Type u_1} {C : Type u_2} [OrderedAddCommMonoid C] {Γ : ValuedCSP D C} {ι : Type u_3} (t : ValuedCSP.Term Γ ι) (x : ι → D) : C

Evaluation of a Γ term t for given solution x.

Equations

• ValuedCSP.Term.evalSolution t x = t.f (x ∘ t.app)

@[inline, reducible]

abbrev ValuedCSP.Instance {D : Type u_1} {C : Type u_2} [OrderedAddCommMonoid C] (Γ : ValuedCSP D C) (ι : Type u_3) : Type (max (max u_1 u_2) u_3)

A valued CSP instance over the template Γ with variables indexed by ι.

Equations

• ValuedCSP.Instance Γ ι = Multiset (ValuedCSP.Term Γ ι)

def ValuedCSP.Instance.evalSolution {D : Type u_1} {C : Type u_2} [OrderedAddCommMonoid C] {Γ : ValuedCSP D C} {ι : Type u_3} (I : ValuedCSP.Instance Γ ι) (x : ι → D) : C

Evaluation of a Γ instance I for given solution x.

Equations

• ValuedCSP.Instance.evalSolution I x = Multiset.sum (Multiset.map (fun (x_1 : ValuedCSP.Term Γ ι) => ValuedCSP.Term.evalSolution x_1 x) I)

def ValuedCSP.Instance.IsOptimumSolution {D : Type u_1} {C : Type u_2} [OrderedAddCommMonoid C] {Γ : ValuedCSP D C} {ι : Type u_3} (I : ValuedCSP.Instance Γ ι) (x : ι → D) : Prop

Condition for x being an optimum solution (min) to given Γ instance I.

Equations

• ValuedCSP.Instance.IsOptimumSolution I x = ∀ (y : ι → D), ValuedCSP.Instance.evalSolution I x ≤ ValuedCSP.Instance.evalSolution I y