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) [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 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

theorem ValuedCSP.Term.inΓ {D : Type u_1} {C : Type u_2} [OrderedAddCommMonoid C] {Γ : ValuedCSP D C} {ι : Type u_3} (self : Γ.Term ι) : ⟨self.n, self.f⟩ ∈ Γ

The cost function comes from the template

def ValuedCSP.Term.evalSolution {D : Type u_1} {C : Type u_2} [OrderedAddCommMonoid C] {Γ : ValuedCSP D C} {ι : Type u_3} (t : Γ.Term ι) (x : ι → D) : C

Evaluation of a Γ term t for given solution x.

Equations

• t.evalSolution x = t.f (x ∘ t.app)

@[reducible, inline]

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

• Γ.Instance ι = Multiset (Γ.Term ι)

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

Evaluation of a Γ instance I for given solution x.

Equations

• I.evalSolution x = (Multiset.map (fun (x_1 : Γ.Term ι) => x_1.evalSolution x) I).sum

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

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

Equations

• I.IsOptimumSolution x = ∀ (y : ι → D), I.evalSolution x ≤ I.evalSolution y

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

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

Equations

• Function.HasMaxCutPropertyAt f a b = (f ![a, b] = f ![b, a] ∧ ∀ (x y : D), f ![a, b] ≤ f ![x, y] ∧ (f ![a, b] = f ![x, y] → a = x ∧ b = y ∨ a = y ∧ b = x))

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

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

Equations

• Function.HasMaxCutProperty f = ∃ (a : D) (b : D), a ≠ b ∧ Function.HasMaxCutPropertyAt f a b

@[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.

Equations

• FractionalOperation D m = Multiset ((Fin m → D) → D)

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

Arity of the "output" of the fractional operation.

Equations

• ω.size = (↑Multiset.card).toFun ω

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

Fractional operation is valid iff nonempty.

Equations

• ω.IsValid = (ω ≠ ∅)

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.

Equations

• ω.tt x = Multiset.map (fun (g : (Fin m → D) → D) (i : ι) => g (Function.swap x i)) ω

def Function.AdmitsFractional {D : Type u_1} {C : Type u_2} [OrderedAddCommMonoid 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.

Equations

• Function.AdmitsFractional f ω = ∀ (x : Fin m → Fin n → D), m • (Multiset.map f (ω.tt x)).sum ≤ ω.size • ∑ i : Fin m, f (x i)

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

Fractional operation is a fractional polymorphism for given VCSP template.

Equations

• ω.IsFractionalPolymorphismFor Γ = ∀ f ∈ Γ, Function.AdmitsFractional f.snd ω

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

Fractional operation is symmetric.

Equations

• ω.IsSymmetric = ∀ (x y : Fin m → D), (List.ofFn x).Perm (List.ofFn y) → ∀ g ∈ ω, g x = g y

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

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

Equations

• ω.IsSymmetricFractionalPolymorphismFor Γ = (ω.IsFractionalPolymorphismFor Γ ∧ ω.IsSymmetric)

theorem Function.HasMaxCutPropertyAt.rows_lt_aux {D : Type u_1} {C : Type u_3} [OrderedCancelAddCommMonoid C] {f : (Fin 2 → D) → C} {a : D} {b : D} (mcf : Function.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} [OrderedCancelAddCommMonoid C] {f : (Fin 2 → D) → C} (mcf : Function.HasMaxCutProperty f) {ω : FractionalOperation D 2} (valid : ω.IsValid) (symmega : ω.IsSymmetric) : ¬Function.AdmitsFractional f ω