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 #

@[inline, reducible]
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 s.nD)C

      Which cost function is instantiated

    • inΓ : { fst := s.n, snd := s.f } Γ

      The cost function comes from the template

    • app : Fin s.nι

      Which variables are plugged as arguments to the cost function

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

      Evaluation of a Γ term t for given solution x.

      Equations
      Instances For
        @[inline, reducible]
        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 : ValuedCsp.Instance Γ ι) (x : ιD) :
          C

          Evaluation of a Γ instance I for given solution x.

          Equations
          Instances For
            def ValuedCsp.Instance.IsOptimumSolution {D : Type u_1} {C : Type u_2} [OrderedAddCommMonoid C] {Γ : ValuedCsp D C} {ι : Type u_3} (I : ValuedCsp.Instance Γ ι) (x : ιD) :

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

            Equations
            Instances For