# 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 Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmException :
Type

An exception in the `SimplexAlgorithmM` monad.

- infeasible : SimplexAlgorithmException

  The solution is infeasible.

Instances For

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

The monad for the Simplex Algorithm.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.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

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.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

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.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

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.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

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.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

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.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

- One or more equations did not get rendered due to their size.

Instances For