6.3.90.900
Fourier-Motzkin Elimination for Integer Systems
Andrew Kent <andmkent@indiana.edu>
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:
Decide the satisfiability of a SLI.
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
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 ≤ (y) ∧ 0 ≤ (x) ∧ (x) + (y) ≤ (z)) | imply | 0 ≤ (z) ∧ (y) ≤ (z) ∧ (x) ≤ (z))? |
|
#t |
2 Linear Expressions
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?).
Returns #t if e is a linear expression constructed with lexp.
Returns the scalar coefficient for the variable
x in e,
returning 0 if x is not present.
Returns the scalar constant for e.
Returns a list of the variables in this linear expression (in no particular order).
Equivalent to
(not (zero? (lexp-coefficient e x))).
Returns the list of coefficients and the
scalar constant in e.
(lexp-scale e n) → lexp?
|
| e : lexp? |
| n : integer? |
Returns an lexp? equivalent to multiplying all
scalars (coefficients and constants) in
e by n.
Returns a linear expression equal to e
except the coefficient for
x is n.
(lexp-set-const e n) → lexp?
|
| e : lexp? |
| n : integer? |
Returns a linear expression equal to
e but with the constant set to n.
Returns #t if the linear expression
is mathematically equivalent to 0.
(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)" |
(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)" |
(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
(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 |
Returns #t if e is a linear inequality constructed with leq.
Returns the lhs and rhs of the inequality.
Returns #t if x is in the lhs or rhs of ineq, else #f.
(leq-negate ineq) → leq?
|
| ineq : leq? |
Negates ineq based on integer arithmetic (e.g. not (x ≤ y) implies (y+1 ≤ x)).
(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.
(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.
(leq-trivially-valid? ineq1 ineq2) → boolean
|
| ineq1 : leq? |
| ineq2 : leq? |
Checks if (ineq1 ≤ ineq2) is trivially true
(i.e. they must both be constants or equal).
4 Systems of Linear Inequalities
Equivalent to
(set/c leq?).
Returns a list of all of the variables in the inequalities of this system,
with duplicates removed.
3-way partitions sys based on how leq-isolate-var would
re-order the inequality in terms of x:
Inequalities of the form (ax ≤ by + cz + ...)
Inequalities of the form (by + cz + ... ≤ ax)
Inequalities which do not contain x
5 Fourier-Motzkin Operations
(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.
Reports if a given system of linear inequalities is satisfiable
(i.e. does a real number solution exist) using Fourier-Motzkin
elimination.
(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).
(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).