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.

inductive Linarith.SimplexAlgorithm.SimplexAlgorithmException : Type

An exception in the SimplexAlgorithmM monad.

• infeasible: Linarith.SimplexAlgorithm.SimplexAlgorithmException

  The solution is infeasible.

structure Linarith.SimplexAlgorithm.SimplexAlgorithmState : Type

The mutable state for the SimplexAlgorithmM monad.

• table : Linarith.SimplexAlgorithm.Table

  Current table.

@[reducible, inline]

abbrev Linarith.SimplexAlgorithm.SimplexAlgorithmM (α : Type) : Type

The monad for the Simplex Algorithm.

Equations

• Linarith.SimplexAlgorithm.SimplexAlgorithmM = ExceptT Linarith.SimplexAlgorithm.SimplexAlgorithmException (StateM Linarith.SimplexAlgorithm.SimplexAlgorithmState)

def Linarith.SimplexAlgorithm.doPivotOperation (exitIdx : Nat) (enterIdx : Nat) : Linarith.SimplexAlgorithm.SimplexAlgorithmM 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.

def Linarith.SimplexAlgorithm.checkSuccess : Linarith.SimplexAlgorithm.SimplexAlgorithmM 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.

def Linarith.SimplexAlgorithm.chooseEnteringVar : Linarith.SimplexAlgorithm.SimplexAlgorithmM 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.

def Linarith.SimplexAlgorithm.chooseExitingVar (enterIdx : Nat) : Linarith.SimplexAlgorithm.SimplexAlgorithmM 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.

def Linarith.SimplexAlgorithm.choosePivots : Linarith.SimplexAlgorithm.SimplexAlgorithmM (Nat × Nat)

Chooses entering and exiting variables using Bland's rule that guarantees that the Simplex Algorithm terminates.

Equations

• Linarith.SimplexAlgorithm.choosePivots = do let enterIdx ← Linarith.SimplexAlgorithm.chooseEnteringVar let exitIdx ← Linarith.SimplexAlgorithm.chooseExitingVar enterIdx pure (exitIdx, enterIdx)

def Linarith.SimplexAlgorithm.runSimplexAlgorithmImp : Linarith.SimplexAlgorithm.SimplexAlgorithmM Unit

Implementation of runSimplexAlgorithm in SimplexAlgorithmM monad.

Equations

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

def Linarith.SimplexAlgorithm.runSimplexAlgorithm (initTable : Linarith.SimplexAlgorithm.Table) : Linarith.SimplexAlgorithm.Table

Runs Simplex Algorithm starting with initTable. It always terminates, finding solution if such exists. Returns the table obtained at the last step.

Equations

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