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
Instances For
    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

    Instances For
      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)
      Instances For
        @[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
        Instances For
          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
          Instances For
            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
            • I.IsOptimumSolution x = ∀ (y : ιD), I.evalSolution x I.evalSolution y
            Instances For
              def Function.HasMaxCutPropertyAt {D : Type u_1} {C : Type u_2} [OrderedAddCommMonoid C] (f : (Fin 2D)C) (a : D) (b : D) :

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

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

                    Arity of the "output" of the fractional operation.

                    Equations
                    • ω.size = (Multiset.card).toFun ω
                    Instances For

                      Fractional operation is valid iff nonempty.

                      Equations
                      Instances For
                        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
                        Instances For
                          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
                          Instances For

                            Fractional operation is a fractional polymorphism for given VCSP template.

                            Equations
                            Instances For

                              Fractional operation is symmetric.

                              Equations
                              Instances For

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

                                Equations
                                • ω.IsSymmetricFractionalPolymorphismFor Γ = (ω.IsFractionalPolymorphismFor Γ ω.IsSymmetric)
                                Instances For
                                  theorem Function.HasMaxCutPropertyAt.rows_lt_aux {D : Type u_1} {C : Type u_3} [OrderedCancelAddCommMonoid C] {f : (Fin 2D)C} {a : D} {b : D} (mcf : Function.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
                                  theorem Function.HasMaxCutProperty.forbids_commutativeFractionalPolymorphism {D : Type u_1} {C : Type u_3} [OrderedCancelAddCommMonoid C] {f : (Fin 2D)C} (mcf : Function.HasMaxCutProperty f) {ω : FractionalOperation D 2} (valid : ω.IsValid) (symmega : ω.IsSymmetric) :