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 s.n → D) → C

  Which cost function is instantiated

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

  The cost function comes from the template

• app : Fin s.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 = ValuedCsp.Term.f t (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