Fourier-Motzkin Elimination for Integer Systems
1 Some Quick Examples
2 Linear Expressions
lexp
lexp?
lexp-coeff
lexp-const
lexp-vars
lexp-has-var?
lexp-scalars
lexp-scale
lexp-set
lexp-set-const
lexp-zero?
lexp-minus
lexp-plus
lexp-add1
3 Linear Inequalities
leq
leq?
leq-lexps
lexp-contains-var?
leq-negate
leq-isolate-var
leq-join
leq-trivially-valid?
4 Systems of Linear Inequalities
sli?
sli-vars
sli-partition
5 Fourier-Motzkin Operations
fme-elim-var
fme-sat?
fme-imp-leq?
fme-imp?
7.1

Fourier-Motzkin Elimination for Integer Systems

Andrew Kent <[email protected]>

 (require fme) package: fme

This package is a simple functional, algebraic implementation of the Fourier-Motzkin elimination method (as opposed to the more common matrix-based approach). It reasons about systems of linear inequalties (SLIs) over integers and currently has two primary functions:

  1. Decide the satisfiability of a SLI.

  2. Decide if one SLI implies another.

The linear inequalities are of the form (L1 ≤ L2), where L1 and L2 are simple linear combinations of the form ax + by + ... + c.

    1 Some Quick Examples

    2 Linear Expressions

    3 Linear Inequalities

    4 Systems of Linear Inequalities

    5 Fourier-Motzkin Operations

1 Some Quick Examples

Examples:
> (let ([assumptions (set (leq (lexp '(7 x))
                               (lexp 29)))]
        [goal (leq (lexp '(1 x))
                   (lexp 4))])
    (begin (printf "Does ~a imply ~a?"
                   (sli->string assumptions)
                   (leq->string goal))
           (fme-imp-leq? assumptions goal)))

Does 7(x) ≤ 29) imply (x) ≤ 4?

#t

> (let ([assumptions (set (leq (lexp '(7 x))
                               (lexp 29)))]
        [goal (leq (lexp '(1 x)) (lexp 3))])
    (begin (printf "Does ~a imply ~a?"
                   (sli->string assumptions)
                   (leq->string goal))
           (fme-imp-leq? assumptions goal)))

Does 7(x) ≤ 29) imply (x) ≤ 3?

#f

> (let ([assumptions (set (leq (lexp '(1 x) '(1 y))
                               (lexp '(1 z)))
                          (leq (lexp)
                               (lexp '(1 y)))
                          (leq (lexp)
                               (lexp '(1 x))))]
        [goals (set (leq (lexp '(1 x))
                         (lexp '(1 z)))
                    (leq (lexp '(1 y))
                         (lexp '(1 z)))
                    (leq (lexp)
                         (lexp '(1 z))))])
    (begin (printf "Does ~a \n imply \n~a?"
                   (sli->string assumptions)
                   (sli->string goals))
           (fme-imp? assumptions goals)))

Does 0 ≤ (x) ∧ (x) + (y) ≤ (z) ∧ 0 ≤ (y))

 imply

(x) ≤ (z) ∧ (y) ≤ (z) ∧ 0 ≤ (z))?

#t

2 Linear Expressions

procedure

(lexp term ...)  lexp?

  term : 
(or/c integer?
      (list integer? any/c))
Builds a linear expression from the given terms. Each term is either a constant exact-integer? or a list of length two representing an integer coefficient and it’s associated variable (which can be anything, comparisons are done using equal?).

procedure

(lexp? e)  boolean?

  e : any/c
Returns #t if e is a linear expression constructed with lexp.

procedure

(lexp-coeff e x)  integer?

  e : lexp?
  x : any/c
Returns the scalar coefficient for the variable x in e, returning 0 if x is not present.

procedure

(lexp-const e)  integer?

  e : lexp?
Returns the scalar constant for e.

procedure

(lexp-vars e)  (listof any/c)

  e : lexp?
Returns a list of the variables in this linear expression (in no particular order).

procedure

(lexp-has-var? e x)  boolean?

  e : lexp?
  x : any/c
Equivalent to (not (zero? (lexp-coefficient e x))).

procedure

(lexp-scalars e)  (listof exact-integer?)

  e : lexp?
Returns the list of coefficients and the scalar constant in e.

procedure

(lexp-scale e n)  lexp?

  e : lexp?
  n : integer?
Returns an lexp? equivalent to multiplying all scalars (coefficients and constants) in e by n.

procedure

(lexp-set e x n)  lexp?

  e : lexp?
  x : any/c
  n : integer?
Returns a linear expression equal to e except the coefficient for x is n.

procedure

(lexp-set-const e n)  lexp?

  e : lexp?
  n : integer?
Returns a linear expression equal to e but with the constant set to n.

procedure

(lexp-zero? e)  boolean?

  e : lexp?
Returns #t if the linear expression is mathematically equivalent to 0.

procedure

(lexp-minus e1 e2)  lexp?

  e1 : lexp?
  e2 : lexp?
Returns the result of e1 - e1. For example (shown below), (2x + 3y - 1) - (2x + 42z - 1) = 3y - 42z

Example:
> (lexp->string (lexp-minus (lexp '(2 x) '(3 y) -1)
                            (lexp '(2 x) -1 '(42 z))))

"3(y) + -42(z)"

procedure

(lexp-plus e1 e2)  lexp?

  e1 : lexp?
  e2 : lexp?
Adds e1 and e2.

Example:
> (lexp->string (lexp-plus (lexp '(2 x) '(3 y) -1)
                           (lexp '(2 x) -1 '(42 z))))

"-2 + 4(x) + 3(y) + 42(z)"

procedure

(lexp-add1 e)  lexp?

  e : lexp?
Equivalent to (lexp-set-const e (add1 (lexp-const e))).

Example:
> (lexp->string (lexp-add1 (lexp 1 '(5 x))))

"2 + 5(x)"

3 Linear Inequalities

procedure

(leq lhs rhs)  lexp?

  lhs : lexp?
  rhs : lexp?
Builds structure representing a less-than-or-equal-to inequality of the form lhs ≤ rhs. When constructed, the leq is normalized, based on the gcd of all scalars in the leq:

Example:
> (equal? (leq (lexp 4 '(8 x))
               (lexp '(16 x) '(12 z)))
          (leq (lexp 1 '(2 x))
               (lexp '(4 x) '(3 z))))

#t

procedure

(leq? e)  boolean?

  e : any/c
Returns #t if e is a linear inequality constructed with leq.

procedure

(leq-lexps ineq)  
lexp? lexp?
  ineq : leq?
Returns the lhs and rhs of the inequality.

procedure

(lexp-contains-var? ineq x)  boolean?

  ineq : leq?
  x : any/c
Returns #t if x is in the lhs or rhs of ineq, else #f.

procedure

(leq-negate ineq)  leq?

  ineq : leq?
Negates ineq based on integer arithmetic (e.g. not (x ≤ y) implies (y+1 ≤ x)).

procedure

(leq-isolate-var ineq x)  leq?

  ineq : leq?
  x : any/c
Converts an inequality into either (ax ≤ by + cz + ...) or (by + cz + ... ≤ ax) such that a is a positive integer and x appears on at most one side of the inequality. If x is not in ineq, it is a no-op.

procedure

(leq-join ineq1 ineq2 x)  leq?

  ineq1 : leq?
  ineq2 : leq?
  x : any/c
Takes a pair of inequalities of the forms (a1x ≤ l1) and (l2 ≤ a2x) and returns a2l1 ≤ a1l2.

procedure

(leq-trivially-valid? ineq1 ineq2)  boolean

  ineq1 : leq?
  ineq2 : leq?
Checks if (ineq1ineq2) is trivially true (i.e. they must both be constants or equal).

4 Systems of Linear Inequalities

procedure

(sli? a)  boolean?

  a : any/c
Equivalent to (set/c leq?).

procedure

(sli-vars sys)  (listof any/c)

  sys : sli?
Returns a list of all of the variables in the inequalities of this system, with duplicates removed.

procedure

(sli-partition sys x)  
sli? sli? sli?
  sys : sli?
  x : any/c
3-way partitions sys based on how leq-isolate-var would re-order the inequality in terms of x:
  1. Inequalities of the form (ax ≤ by + cz + ...)

  2. Inequalities of the form (by + cz + ... ≤ ax)

  3. Inequalities which do not contain x

5 Fourier-Motzkin Operations

procedure

(fme-elim-var sys x)  sli?

  sys : sli?
  x : any/c
Returns an SLI without x such that it possesses the same set of satisfying solutions with respect to the remaining variables.

It relies on sli-partition and leq-join.

procedure

(fme-sat? sys)  boolean?

  sys : sli?
Reports if a given system of linear inequalities is satisfiable (i.e. does a real number solution exist) using Fourier-Motzkin elimination.

procedure

(fme-imp-leq? sys ineq)  boolean?

  sys : sli?
  ineq : leq?
Reports if a given system of linear inequalities, sys, implies the constraint ineq (this is valid for the integer domain of inequalities only, since we utilize integer inequality negation and then test for satisfiability).

procedure

(fme-imp? sys1 sys2)  boolean?

  sys1 : sli?
  sys2 : sli?
Reports if sys1 implies all of the constraints contained in sys2 (again, this is valid for the integer domain of inequalities only, since we utilize integer inequality negation).