linarith certificate search a LP problem

linarith certificate search can easily be reduced to this LP problem: given the matrix A and the list strictIndexes, find the non-negative vector v such that some of its coordinates from the strictIndexes are positive and A v = 0.

The function findPositiveVector solves this problem.

def Linarith.SimplexAlgorithm.stateLP {n : Nat} {m : Nat} (A : Linarith.SimplexAlgorithm.Matrix n m) (strictIndexes : List Nat) : Linarith.SimplexAlgorithm.Matrix (n + 2) (m + 3)

Given matrix A and list strictIndexes of strict inequalities' indexes, we want to state the Linear Programming problem which solution produces solution for the initial problem (see findPositiveVector).

As an objective function (that we are trying to maximize) we use sum of coordinates from strictIndexes: it suffices to find the non-negative vector that makes this function positive.

We introduce two auxiliary variables and one constraint:

• The variable y is interpreted as "homogenized" 1. We need it because dealing with a homogenized problem is easier, but having some "unit" is necessary.
• To bound the problem we add the constraint x₁ + ... + xₘ + z = y introducing new variable z.

The objective function also interpreted as an auxiliary variable with constraint f = ∑ i ∈ strictIndexes, xᵢ.

The variable f has to always be basic while y has to be free. Our Gauss method implementation greedy collects basic variables moving from left to right. So we place f before x-s and y after them. We place z between f and x because in this case z will be basic and Gauss.getTable produce table with non-negative last column, meaning that we are starting from a feasible point.

Equations

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

def Linarith.SimplexAlgorithm.extractSolution (table : Linarith.SimplexAlgorithm.Table) : Array Rat

Extracts target vector from the table, putting auxilary variables aside (see stateLP).

Equations

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

def Linarith.SimplexAlgorithm.findPositiveVector {n : Nat} {m : Nat} (A : Linarith.SimplexAlgorithm.Matrix n m) (strictIndexes : List Nat) : Array Rat

Finds nonnegative vector v, such that A v = 0 and some of its coordinates from strictCoords are positive, in the case such v exists.

Equations

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