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?
• Function.HasMaxCutProperty: Can given binary function express the Max-Cut problem?
• FractionalOperation: Multiset of operations on given domain of the same arity.
• FractionalOperation.IsSymmetricFractionalPolymorphismFor: Is given fractional operation a symmetric fractional polymorphism for given VCSP template?

References

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

@[reducible, inline]

abbrev ValuedCSP (D : Type u_1) (C : Type u_2) [AddCommMonoid C] [PartialOrder C] [IsOrderedAddMonoid 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.

structure ValuedCSP.Term {D : Type u_1} {C : Type u_2} [AddCommMonoid C] [PartialOrder C] [IsOrderedAddMonoid 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Γ : ⟨self.n, 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} [AddCommMonoid C] [PartialOrder C] [IsOrderedAddMonoid C] {Γ : ValuedCSP D C} {ι : Type u_3} (t : Γ.Term ι) (x : ι → D) : C

Evaluation of a Γ term t for given solution x.

@[reducible, inline]

abbrev ValuedCSP.Instance {D : Type u_1} {C : Type u_2} [AddCommMonoid C] [PartialOrder C] [IsOrderedAddMonoid 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 ι.

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

Evaluation of a Γ instance I for given solution x.

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

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

def Function.HasMaxCutPropertyAt {D : Type u_1} {C : Type u_2} [PartialOrder C] (f : (Fin 2 → D) → C) (a b : D) : Prop

Function f has Max-Cut property at labels a and b when argmin f is exactly { ![a, b] , ![b, a] }.

def Function.HasMaxCutProperty {D : Type u_1} {C : Type u_2} [PartialOrder C] (f : (Fin 2 → D) → C) : Prop

Function f has Max-Cut property at some two non-identical labels.

@[reducible, inline]

abbrev FractionalOperation (D : Type u_3) (m : ℕ) : Type u_3

Fractional operation is a finite unordered collection of D^m → D possibly with duplicates.

def FractionalOperation.size {D : Type u_1} {m : ℕ} (ω : FractionalOperation D m) : ℕ

Arity of the "output" of the fractional operation.

def FractionalOperation.IsValid {D : Type u_1} {m : ℕ} (ω : FractionalOperation D m) : Prop

Fractional operation is valid iff nonempty.

theorem FractionalOperation.IsValid.contains {D : Type u_1} {m : ℕ} {ω : FractionalOperation D m} (valid : ω.IsValid) : ∃ (g : (Fin m → D) → D), g ∈ ω

Valid fractional operation contains an operation.

def FractionalOperation.tt {D : Type u_1} {m : ℕ} {ι : Type u_3} (ω : FractionalOperation D m) (x : Fin m → ι → D) : Multiset (ι → D)

Fractional operation applied to a transposed table of values.

def Function.AdmitsFractional {D : Type u_1} {C : Type u_2} [AddCommMonoid C] [PartialOrder C] {m n : ℕ} (f : (Fin n → D) → C) (ω : FractionalOperation D m) : Prop

Cost function admits given fractional operation, i.e., ω improves f in the ≤ sense.

def FractionalOperation.IsFractionalPolymorphismFor {D : Type u_1} {C : Type u_2} [AddCommMonoid C] [PartialOrder C] [IsOrderedAddMonoid C] {m : ℕ} (ω : FractionalOperation D m) (Γ : ValuedCSP D C) : Prop

Fractional operation is a fractional polymorphism for given VCSP template.

def FractionalOperation.IsSymmetric {D : Type u_1} {m : ℕ} (ω : FractionalOperation D m) : Prop

Fractional operation is symmetric.

def FractionalOperation.IsSymmetricFractionalPolymorphismFor {D : Type u_1} {C : Type u_2} [AddCommMonoid C] [PartialOrder C] [IsOrderedAddMonoid C] {m : ℕ} (ω : FractionalOperation D m) (Γ : ValuedCSP D C) : Prop

Fractional operation is a symmetric fractional polymorphism for given VCSP template.

theorem Function.HasMaxCutPropertyAt.rows_lt_aux {D : Type u_1} {C : Type u_3} [PartialOrder C] {f : (Fin 2 → D) → C} {a b : D} (mcf : HasMaxCutPropertyAt f a b) (hab : a ≠ b) {ω : FractionalOperation D 2} (symmega : ω.IsSymmetric) {r : Fin 2 → D} (rin : r ∈ ω.tt ![![a, b], ![b, a]]) : f ![a, b] < f r

theorem Function.HasMaxCutProperty.forbids_commutativeFractionalPolymorphism {D : Type u_1} {C : Type u_3} [AddCommMonoid C] [PartialOrder C] [IsOrderedCancelAddMonoid C] {f : (Fin 2 → D) → C} (mcf : HasMaxCutProperty f) {ω : FractionalOperation D 2} (valid : ω.IsValid) (symmega : ω.IsSymmetric) : ¬AdmitsFractional f ω