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 #

References #

@[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
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.nD)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} [OrderedAddCommMonoid C] {Γ : ValuedCSP D C} {ι : Type u_3} (t : Γ.Term ι) (x : ιD) :
C

Evaluation of a Γ term t for given solution x.

Equations
@[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
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
def ValuedCSP.Instance.IsOptimumSolution {D : Type u_1} {C : Type u_2} [OrderedAddCommMonoid C] {Γ : ValuedCSP D C} {ι : Type u_3} (I : Γ.Instance ι) (x : ιD) :

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

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

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

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

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

Equations
@[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
def FractionalOperation.size {D : Type u_1} {m : } (ω : FractionalOperation D m) :

Arity of the "output" of the fractional operation.

Equations

Fractional operation is valid iff nonempty.

Equations
theorem FractionalOperation.IsValid.contains {D : Type u_1} {m : } {ω : FractionalOperation D m} (valid : ω.IsValid) :
∃ (g : (Fin mD)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
def Function.AdmitsFractional {D : Type u_1} {C : Type u_2} [OrderedAddCommMonoid C] {m n : } (f : (Fin nD)C) (ω : FractionalOperation D m) :

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

Equations

Fractional operation is a fractional polymorphism for given VCSP template.

Equations

Fractional operation is symmetric.

Equations

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

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