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]
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
Instances For
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)
Instances For
@[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 Γ ι)
Instances For
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)
Instances For
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)
:
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