Fourier-Motzkin Elimination

Fourier-Motzkin elimination is an algorithm for eliminating real variables from a finite system of linear inequalities. Geometrically, it computes a description of a coordinate projection of the solution set (Dantzig and Eaves 1973, Williams 1986).

To eliminate a variable , divide the inequalities with nonzero coefficients of by those coefficients, reversing an inequality when the coefficient is negative. This gives lower bounds and upper bounds , where the and are affine functions of the remaining variables . An satisfying all these bounds exists iff

for every lower-bound and upper-bound pair. Retain all inequalities that already do not involve . If there are no lower bounds or no upper bounds, there are no paired conditions to add (Williams 1986, p. 683).

For example,

where . The four pairwise comparisons are , , , and , of which only the middle two restrict .

A pair involving a strict inequality produces a strict comparison between its bounds. An equation can be replaced by two opposite non-strict inequalities. Repeating the elimination gives a quantifier elimination procedure for systems of linear inequalities over the real numbers. If a step has lower bounds, upper bounds, and inequalities independent of , it produces inequalities before redundant conditions are removed, so the intermediate systems can grow rapidly. The same bound comparisons do not suffice over the integers. For example, the interval is nonempty but contains no integer.