# Documentation

Mathlib.Combinatorics.Optimization.ValuedCSP

# 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) :
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
Instances For
structure ValuedCsp.Term {D : Type u_1} {C : Type u_2} (Γ : ) (ι : 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.nD)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

Instances For
def ValuedCsp.Term.evalSolution {D : Type u_1} {C : Type u_2} {Γ : } {ι : Type u_3} (t : ) (x : ιD) :
C

Evaluation of a Γ term t for given solution x.

Equations
Instances For
@[inline, reducible]
abbrev ValuedCsp.Instance {D : Type u_1} {C : Type u_2} (Γ : ) (ι : Type u_3) :
Type (max (max u_1 u_2) u_3)

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

Equations
Instances For
def ValuedCsp.Instance.evalSolution {D : Type u_1} {C : Type u_2} {Γ : } {ι : Type u_3} (I : ) (x : ιD) :
C

Evaluation of a Γ instance I for given solution x.

Equations
Instances For
def ValuedCsp.Instance.IsOptimumSolution {D : Type u_1} {C : Type u_2} {Γ : } {ι : Type u_3} (I : ) (x : ιD) :

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

Equations
• = ∀ (y : ιD),
Instances For