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) [UsableInSimplexAlgorithm matType] (α : Type) :
    Type

    The monad for the Simplex Algorithm.

    Equations
      Instances For
        source
        def Linarith.SimplexAlgorithm.doPivotOperation {matType : Nat → Nat → Type} [UsableInSimplexAlgorithm matType] (exitIdx enterIdx : Nat) :
        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
          Instances For
            source
            def Linarith.SimplexAlgorithm.checkSuccess {matType : Nat → Nat → Type} [UsableInSimplexAlgorithm matType] :
            SimplexAlgorithmM matType Bool

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

            Equations
              Instances For
                source
                def Linarith.SimplexAlgorithm.chooseEnteringVar {matType : Nat → Nat → Type} [UsableInSimplexAlgorithm matType] :
                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
                  Instances For
                    source
                    def Linarith.SimplexAlgorithm.chooseExitingVar {matType : Nat → Nat → Type} [UsableInSimplexAlgorithm matType] (enterIdx : Nat) :
                    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
                      Instances For
                        source
                        def Linarith.SimplexAlgorithm.choosePivots {matType : Nat → Nat → Type} [UsableInSimplexAlgorithm matType] :
                        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} [UsableInSimplexAlgorithm matType] :
                            SimplexAlgorithmM matType Unit

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

                            Equations
                              Instances For