[Merged by Bors] - General valued constraint satisfaction problem defined

Mathlib.lean

@@ -1264,6 +1264,7 @@ import Mathlib.Combinatorics.HalesJewett
 import Mathlib.Combinatorics.Hall.Basic
 import Mathlib.Combinatorics.Hall.Finite
 import Mathlib.Combinatorics.Hindman
+import Mathlib.Combinatorics.Optimization.ValuedCSP
 import Mathlib.Combinatorics.Partition
 import Mathlib.Combinatorics.Pigeonhole
 import Mathlib.Combinatorics.Quiver.Arborescence

Mathlib/Combinatorics/Optimization/ValuedCSP.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2023 Martin Dvorak. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Martin Dvorak
+-/
+import Mathlib.Algebra.Order.Monoid.Defs
+import Mathlib.Algebra.BigOperators.Multiset.Basic
+
+/-!
+
+# 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.OptimumSolution`: 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]
+
+-/
+
+/-- 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. -/
+@[reducible, nolint unusedArguments]
+def ValuedCsp (D C : Type*) [OrderedAddCommMonoid C] :=
+  Set (Σ (n : ℕ), (Fin n → D) → C) -- Cost functions `D^n → C` for any `n`
+
+variable {D C : Type*} [OrderedAddCommMonoid C]
+
+/-- A term in a valued CSP instance over the template `Γ`. -/
+structure ValuedCsp.Term (Γ : ValuedCsp D C) (ι : Type*) where
+  /-- Arity of the function -/
+  n : ℕ
+  /-- Which cost function is instantiated -/
+  f : (Fin n → D) → C
+  /-- The cost function comes from the template -/
+  inΓ : ⟨n, f⟩ ∈ Γ
+  /-- Which variables are plugged as arguments to the cost function -/
+  app : Fin n → ι
+
+/-- Evaluation of a `Γ` term `t` for given solution `x`. -/
+def ValuedCsp.Term.evalSolution {Γ : ValuedCsp D C} {ι : Type*}
+    (t : Γ.Term ι) (x : ι → D) : C :=
+  t.f (x ∘ t.app)
+
+/-- A valued CSP instance over the template `Γ` with variables indexed by `ι`.-/
+def ValuedCsp.Instance (Γ : ValuedCsp D C) (ι : Type*) :=
+  Multiset (Γ.Term ι)
+
+/-- Evaluation of a `Γ` instance `I` for given solution `x`. -/
+def ValuedCsp.Instance.evalSolution {Γ : ValuedCsp D C} {ι : Type*}
+    (I : Γ.Instance ι) (x : ι → D) : C :=
+  (I.map (·.evalSolution x)).sum
+
+/-- Condition for `x` being an optimum solution (min) to given `Γ` instance `I`.-/
+def ValuedCsp.Instance.OptimumSolution {Γ : ValuedCsp D C} {ι : Type*}
+    (I : Γ.Instance ι) (x : ι → D) : Prop :=
+  ∀ y : ι → D, I.evalSolution x ≤ I.evalSolution y

docs/references.bib

@@ -645,6 +645,22 @@ @Book{            clark_gon
   url           = {http://alpha.math.uga.edu/~pete/geometryofnumbers.pdf}
 }
 
+@Article{         cohen2012,
+  author        = {David A. Cohen and Martin C. Cooper and Páidí Creed and
+                  Peter G. Jeavons and Stanislav Živný},
+  title         = {An Algebraic Theory of Complexity for Discrete
+                  Optimisation},
+  journal       = {CoRR},
+  volume        = {abs/1207.6692},
+  year          = {2012},
+  url           = {http://arxiv.org/abs/1207.6692},
+  eprinttype    = {arXiv},
+  eprint        = {1207.6692},
+  timestamp     = {Mon, 03 Aug 2020 17:29:56 +0200},
+  biburl        = {https://dblp.org/rec/journals/corr/abs-1207-6692.bib},
+  bibsource     = {dblp computer science bibliography, https://dblp.org}
+}
+
 @Book{            conrad2000,
   author        = {Conrad, Brian},
   title         = {Grothendieck duality and base change},