The Fourier-Motzkin elimination procedure

The Fourier-Motzkin procedure is a variable elimination method for linear inequalities. https://en.wikipedia.org/wiki/Fourier%E2%80%93Motzkin_elimination

Given a set of linear inequalities comps = {tᵢ Rᵢ 0}, we aim to eliminate a single variable a from the set. We partition comps into comps_pos, comps_neg, and comps_zero, where comps_pos contains the comparisons tᵢ Rᵢ 0 in which the coefficient of a in tᵢ is positive, and similar.

For each pair of comparisons tᵢ Rᵢ 0 ∈ comps_pos, tⱼ Rⱼ 0 ∈ comps_neg, we compute coefficients vᵢ, vⱼ ∈ ℕ such that vᵢ*tᵢ + vⱼ*tⱼ cancels out a. We collect these sums vᵢ*tᵢ + vⱼ*tⱼ R' 0 in a set S and set comps' = S ∪ comps_zero, a new set of comparisons in which a has been eliminated.

Theorem: comps and comps' are equisatisfiable.

We recursively eliminate all variables from the system. If we derive an empty clause 0 < 0, we conclude that the original system was unsatisfiable.

Datatypes

The CompSource and PComp datatypes are specific to the FM elimination routine; they are not shared with other components of linarith.

inductive Linarith.CompSource : Type

CompSource tracks the source of a comparison. The atomic source of a comparison is an assumption, indexed by a natural number. Two comparisons can be added to produce a new comparison, and one comparison can be scaled by a natural number to produce a new comparison.

• assump: ℕ → Linarith.CompSource
• add: Linarith.CompSource → Linarith.CompSource → Linarith.CompSource
• scale: ℕ → Linarith.CompSource → Linarith.CompSource

instance Linarith.instInhabitedCompSource : Inhabited Linarith.CompSource

Equations

• Linarith.instInhabitedCompSource = { default := Linarith.CompSource.assump default }

def Linarith.CompSource.flatten : Linarith.CompSource → Batteries.HashMap ℕ ℕ

Given a CompSource cs, cs.flatten maps an assumption index to the number of copies of that assumption that appear in the history of cs.

For example, suppose cs is produced by scaling assumption 2 by 5, and adding to that the sum of assumptions 1 and 2. cs.flatten maps 1 ↦ 1, 2 ↦ 6.

Equations

• (Linarith.CompSource.assump n).flatten = Batteries.HashMap.empty.insert n 1
• (c1.add c2).flatten = Batteries.HashMap.mergeWith (fun (x b b' : ℕ) => b + b') c1.flatten c2.flatten
• (Linarith.CompSource.scale n c).flatten = Batteries.HashMap.mapVal (fun (x v : ℕ) => v * n) c.flatten

def Linarith.CompSource.toString : Linarith.CompSource → String

Formats a CompSource for printing.

Equations

• (Linarith.CompSource.assump n).toString = toString n
• (c1.add c2).toString = c1.toString ++ " + " ++ c2.toString
• (Linarith.CompSource.scale n c).toString = toString n ++ " * " ++ c.toString

instance Linarith.instToFormatCompSource : Lean.ToFormat Linarith.CompSource

Equations

• Linarith.instToFormatCompSource = { format := fun (a : Linarith.CompSource) => Std.Format.text a.toString }

structure Linarith.PComp : Type

A PComp stores a linear comparison Σ cᵢ*xᵢ R 0, along with information about how this comparison was derived. The original expressions fed into linarith are each assigned a unique natural number label. The historical set PComp.history stores the labels of expressions that were used in deriving the current PComp. Variables are also indexed by natural numbers. The sets PComp.effective, PComp.implicit, and PComp.vars contain variable indices.

• PComp.vars contains the variables that appear in any inequality in the historical set.
• PComp.effective contains the variables that have been effectively eliminated from PComp. A variable n is said to be effectively eliminated in p : PComp if the elimination of n produced at least one of the ancestors of p (or p itself).
• PComp.implicit contains the variables that have been implicitly eliminated from PComp. A variable n is said to be implicitly eliminated in p if it satisfies the following properties:
  • n appears in some inequality in the historical set (i.e. in p.vars).
  • n does not appear in p.c.vars (i.e. it has been eliminated).
  • n was not effectively eliminated.

We track these sets in order to compute whether the history of a PComp is minimal. Checking this directly is expensive, but effective approximations can be defined in terms of these sets. During the variable elimination process, a PComp with non-minimal history can be discarded.

• c : Linarith.Comp

  The comparison Σ cᵢ*xᵢ R 0.

• src : Linarith.CompSource

  We track how the comparison was constructed by adding and scaling previous comparisons, back to the original assumptions.

• history : Batteries.RBSet ℕ compare

  The set of original assumptions which have been used in constructing this comparison.

• effective : Batteries.RBSet ℕ compare

  The variables which have been effectively eliminated, i.e. by running the elimination algorithm on that variable.

• implicit : Batteries.RBSet ℕ compare

  The variables which have been implicitly eliminated. These are variables that appear in the historical set, do not appear in c itself, and are not in `effective.

• vars : Batteries.RBSet ℕ compare

  The union of all variables appearing in those original assumptions which appear in the history set.

def Linarith.PComp.maybeMinimal (c : Linarith.PComp) (elimedGE : ℕ) : Bool

Any comparison whose history is not minimal is redundant, and need not be included in the new set of comparisons. elimedGE : ℕ is a natural number such that all variables with index ≥ elimedGE have been removed from the system.

This test is an overapproximation to minimality. It gives necessary but not sufficient conditions. If the history of c is minimal, then c.maybeMinimal is true, but c.maybeMinimal may also be true for some c with non-minimal history. Thus, if c.maybeMinimal is false, c is known not to be minimal and must be redundant. See https://doi.org/10.1016/B978-0-444-88771-9.50019-2 (Theorem 13). The condition described there considers only implicitly eliminated variables that have been officially eliminated from the system. This is not the case for every implicitly eliminated variable. Consider eliminating z from {x + y + z < 0, x - y - z < 0}. The result is the set {2*x < 0}; y is implicitly but not officially eliminated.

This implementation of Fourier-Motzkin elimination processes variables in decreasing order of indices. Immediately after a step that eliminates variable k, variable k' has been eliminated iff k' ≥ k. Thus we can compute the intersection of officially and implicitly eliminated variables by taking the set of implicitly eliminated variables with indices ≥ elimedGE.

Equations

• c.maybeMinimal elimedGE = decide (c.history.size ≤ 1 + ((c.implicit.filter fun (x : ℕ) => decide (x ≥ elimedGE)).union c.effective).size)

def Linarith.PComp.cmp (p1 : Linarith.PComp) (p2 : Linarith.PComp) : Ordering

The src : CompSource field is ignored when comparing PComps. Two PComps proving the same comparison, with different sources, are considered equivalent.

Equations

• p1.cmp p2 = p1.c.cmp p2.c

def Linarith.PComp.scale (c : Linarith.PComp) (n : ℕ) : Linarith.PComp

PComp.scale c n scales the coefficients of c by n and notes this in the CompSource.

Equations

• c.scale n = { c := c.c.scale n, src := Linarith.CompSource.scale n c.src, history := c.history, effective := c.effective, implicit := c.implicit, vars := c.vars }

def Linarith.PComp.add (c1 : Linarith.PComp) (c2 : Linarith.PComp) (elimVar : ℕ) : Linarith.PComp

PComp.add c1 c2 elimVar creates the result of summing the linear comparisons c1 and c2, during the process of eliminating the variable elimVar. The computation assumes, but does not enforce, that elimVar appears in both c1 and c2 and does not appear in the sum. Computing the sum of the two comparisons is easy; the complicated details lie in tracking the additional fields of PComp.

• The historical set pcomp.history of c1 + c2 is the union of the two historical sets.
• vars is the union of c1.vars and c2.vars.
• The effectively eliminated variables of c1 + c2 are the union of the two effective sets, with elim_var inserted.
• The implicitly eliminated variables of c1 + c2 are those that appear in vars but not c.vars or effective. (Note that the description of the implicitly eliminated variables of c1 + c2 in the algorithm described in Section 6 of https://doi.org/10.1016/B978-0-444-88771-9.50019-2 seems to be wrong: that says it should be (c1.implicit.union c2.implicit).sdiff explicit. Since the implicitly eliminated sets start off empty for the assumption, this formula would leave them always empty.)

Equations

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

def Linarith.PComp.assump (c : Linarith.Comp) (n : ℕ) : Linarith.PComp

PComp.assump c n creates a PComp whose comparison is c and whose source is CompSource.assump n, that is, c is derived from the nth hypothesis. The history is the singleton set {n}. No variables have been eliminated (effectively or implicitly).

Equations

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

instance Linarith.instToFormatPComp : Lean.ToFormat Linarith.PComp

Equations

• Linarith.instToFormatPComp = { format := fun (p : Linarith.PComp) => Std.format p.c.coeffs ++ Std.Format.text (toString p.c.str) ++ Std.Format.text "0" }

instance Linarith.instToStringPComp : ToString Linarith.PComp

Equations

• Linarith.instToStringPComp = { toString := fun (p : Linarith.PComp) => toString p.c.coeffs ++ toString p.c.str ++ "0" }

@[reducible, inline]

abbrev Linarith.PCompSet : Type

A collection of comparisons.

Equations

• Linarith.PCompSet = Batteries.RBSet Linarith.PComp Linarith.PComp.cmp

Elimination procedure

def Linarith.elimVar (c1 : Linarith.Comp) (c2 : Linarith.Comp) (a : ℕ) : Option (ℕ × ℕ)

If c1 and c2 both contain variable a with opposite coefficients, produces v1 and v2 such that a has been cancelled in v1*c1 + v2*c2.

Equations

• Linarith.elimVar c1 c2 a = let v1 := c1.coeffOf a; let v2 := c2.coeffOf a; if v1 * v2 < 0 then let vlcm := v1.natAbs.lcm v2.natAbs; some (vlcm / v1.natAbs, vlcm / v2.natAbs) else none

def Linarith.pelimVar (p1 : Linarith.PComp) (p2 : Linarith.PComp) (a : ℕ) : Option Linarith.PComp

pelimVar p1 p2 calls elimVar on the Comp components of p1 and p2. If this returns v1 and v2, it creates a new PComp equal to v1*p1 + v2*p2, and tracks this in the CompSource.

Equations

• Linarith.pelimVar p1 p2 a = do let __discr ← Linarith.elimVar p1.c p2.c a match __discr with | (n1, n2) => pure ((p1.scale n1).add (p2.scale n2) a)

def Linarith.PComp.isContr (p : Linarith.PComp) : Bool

A PComp represents a contradiction if its Comp field represents a contradiction.

Equations

• p.isContr = p.c.isContr

def Linarith.elimWithSet (a : ℕ) (p : Linarith.PComp) (comps : Linarith.PCompSet) : Linarith.PCompSet

elimWithSet a p comps collects the result of calling pelimVar p p' a for every p' ∈ comps.

Equations

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

structure Linarith.LinarithData : Type

The state for the elimination monad.

• maxVar: the largest variable index that has not been eliminated.
• comps: a set of comparisons

The elimination procedure proceeds by eliminating variable v from comps progressively in decreasing order.

• maxVar : ℕ

  The largest variable index that has not been (officially) eliminated.

• comps : Linarith.PCompSet

  The set of comparisons.

@[reducible, inline]

abbrev Linarith.LinarithM : Type → Type

The linarith monad extends an exceptional monad with a LinarithData state. An exception produces a contradictory PComp.

Equations

• Linarith.LinarithM = StateT Linarith.LinarithData (ExceptT Linarith.PComp Id)

def Linarith.getMaxVar : Linarith.LinarithM ℕ

Returns the current max variable.

Equations

• Linarith.getMaxVar = Linarith.LinarithData.maxVar <$> get

def Linarith.getPCompSet : Linarith.LinarithM Linarith.PCompSet

Return the current comparison set.

Equations

• Linarith.getPCompSet = Linarith.LinarithData.comps <$> get

def Linarith.validate : Linarith.LinarithM Unit

Throws an exception if a contradictory PComp is contained in the current state.

Equations

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

def Linarith.update (maxVar : ℕ) (comps : Linarith.PCompSet) : Linarith.LinarithM Unit

Updates the current state with a new max variable and comparisons, and calls validate to check for a contradiction.

Equations

• Linarith.update maxVar comps = do StateT.set { maxVar := maxVar, comps := comps } Linarith.validate

def Linarith.splitSetByVarSign (a : ℕ) (comps : Linarith.PCompSet) : Linarith.PCompSet × Linarith.PCompSet × Linarith.PCompSet

splitSetByVarSign a comps partitions the set comps into three parts.

• pos contains the elements of comps in which a has a positive coefficient.
• neg contains the elements of comps in which a has a negative coefficient.
• notPresent contains the elements of comps in which a has coefficient 0.

Returns (pos, neg, notPresent).

Equations

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

def Linarith.elimVarM (a : ℕ) : Linarith.LinarithM Unit

elimVarM a performs one round of Fourier-Motzkin elimination, eliminating the variable a from the linarith state.

Equations

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

def Linarith.elimAllVarsM : Linarith.LinarithM Unit

elimAllVarsM eliminates all variables from the linarith state, leaving it with a set of ground comparisons. If this succeeds without exception, the original linarith state is consistent.

Equations

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

def Linarith.mkLinarithData (hyps : List Linarith.Comp) (maxVar : ℕ) : Linarith.LinarithData

mkLinarithData hyps vars takes a list of hypotheses and the largest variable present in those hypotheses. It produces an initial state for the elimination monad.

Equations

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

def Linarith.CertificateOracle.fourierMotzkin : Linarith.CertificateOracle

An oracle that uses Fourier-Motzkin elimination.

Equations

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