HepLean Documentation

Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm

Simplex Algorithm #

To obtain required vector in Linarith.SimplexAlgorithm.findPositiveVector we run the Simplex Algorithm. We use Bland's rule for pivoting, which guarantees that the algorithm terminates.

source
inductive Linarith.SimplexAlgorithm.SimplexAlgorithmException :
Type

An exception in the SimplexAlgorithmM monad.

Instances For
    source
    @[reducible, inline]
    abbrev Linarith.SimplexAlgorithm.SimplexAlgorithmM (matType : Nat → Nat → Type) [Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] (α : Type) :
    Type

    The monad for the Simplex Algorithm.

    Equations
    Instances For
      source
      def Linarith.SimplexAlgorithm.doPivotOperation {matType : Nat → Nat → Type} [Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] (exitIdx : Nat) (enterIdx : Nat) :
      Linarith.SimplexAlgorithm.SimplexAlgorithmM matType Unit

      Given indexes exitIdx and enterIdx of exiting and entering variables in the basic and free arrays, performs pivot operation, i.e. expresses one through the other and makes the free one basic and vice versa.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Linarith.SimplexAlgorithm.checkSuccess {matType : Nat → Nat → Type} [Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] :
        Linarith.SimplexAlgorithm.SimplexAlgorithmM matType Bool

        Check if the solution is found: the objective function is positive and all basic variables are nonnegative.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Linarith.SimplexAlgorithm.chooseEnteringVar {matType : Nat → Nat → Type} [Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] :
          Linarith.SimplexAlgorithm.SimplexAlgorithmM matType Nat

          Chooses an entering variable: among the variables with a positive coefficient in the objective function, the one with the smallest index (in the initial indexing).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Linarith.SimplexAlgorithm.chooseExitingVar {matType : Nat → Nat → Type} [Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] (enterIdx : Nat) :
            Linarith.SimplexAlgorithm.SimplexAlgorithmM matType Nat

            Chooses an exiting variable: the variable imposing the strictest limit on the increase of the entering variable, breaking ties by choosing the variable with smallest index.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Linarith.SimplexAlgorithm.choosePivots {matType : Nat → Nat → Type} [Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] :
              Linarith.SimplexAlgorithm.SimplexAlgorithmM matType (Nat × Nat)

              Chooses entering and exiting variables using (Bland's rule)[(https://en.wikipedia.org/wiki/Bland%27s_rule)] that guarantees that the Simplex Algorithm terminates.

              Equations
              Instances For
                source
                def Linarith.SimplexAlgorithm.runSimplexAlgorithm {matType : Nat → Nat → Type} [Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] :
                Linarith.SimplexAlgorithm.SimplexAlgorithmM matType Unit

                Runs the Simplex Algorithm inside the SimplexAlgorithmM. It always terminates, finding solution if such exists.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For