Fourier–Motzkin elimination

From Wikipedia, the free encyclopedia
Jump to: navigation, search

Fourier–Motzkin elimination, also known as the FME method, is a mathematical algorithm for eliminating variables from a system of linear inequalities. It can output real solutions.

The algorithm is named after Joseph Fourier and Theodore Motzkin.

Elimination[edit]

The elimination of a set of variables, say V, from a system of relations (here linear inequalities) refers to the creation of another system of the same sort, but without the variables in V, such that both systems have the same solutions over the remaining variables.

If all variables are eliminated from a system of linear inequalities, then one obtains a system of constant inequalities. It is then trivial to decide whether the resulting system is true or false. It is true if and only if the original system has solutions. As a consequence, elimination of all variables can be used to detect whether a system of inequalities has solutions or not.

Consider a system S of n inequalities with r variables x_1 to x_r, with x_r the variable to be eliminated. The linear inequalities in the system can be grouped into three classes depending on the sign (positive, negative or null) of the coefficient for x_r.

  • those inequalities that are of the form x_r \geq b_i-\sum_{k=1}^{r-1} a_{ik} x_k; denote these by x_r \geq A_j(x_1, \dots, x_{r-1}), for j ranging from 1 to n_A where n_A is the number of such inequalities;
  • those inequalities that are of the form x_r \leq b_i-\sum_{k=1}^{r-1} a_{ik} x_k; denote these by x_r \leq B_j(x_1, \dots, x_{r-1}), for j ranging from 1 to n_B where n_B is the number of such inequalities;
  • those inequalities in which x_r plays no role, grouped into a single conjunction \phi.

The original system is thus equivalent to

\max(A_1(x_1, \dots, x_{r-1}), \dots, A_{n_A}(x_1, \dots, x_{r-1})) \leq x_r \leq \min(B_1(x_1, \dots, x_{r-1}), \dots, B_{n_B}(x_1, \dots, x_{r-1})) \wedge \phi.

Elimination consists in producing a system equivalent to \exists x_r~S. Obviously, this formula is equivalent to

\max(A_1(x_1, \dots, x_{r-1}), \dots, A_{n_A}(x_1, \dots, x_{r-1})) \leq \min(B_1(x_1, \dots, x_{r-1}), \dots, B_{n_B}(x_1, \dots, x_{r-1})) \wedge \phi.

The inequality

\max(A_1(x_1, \dots, x_{r-1}), \dots, A_{n_A}(x_1, \dots, x_{r-1})) \leq \min(B_1(x_1, \dots, x_{r-1}), \dots, B_{n_B}(x_1, \dots, x_{r-1}))

is equivalent to n_A n_B inequalities A_i(x_1, \dots, x_{r-1}) \leq B_j(x_1, \dots, x_{r-1}), for 1 \leq i \leq n_A and 1 \leq j \leq n_B.

We have therefore transformed the original system into another system where x_r is eliminated. Note that the output system has (n-n_A-n_B)+n_A n_B inequalities. In particular, if n_A = n_B = n/2, then the number of output inequalities is n^2/4.

Complexity[edit]

Running an elimination step over n inequalities can result in at most n^2/4 inequalities in the output, thus running d successive steps can result in at most 4(n/4)^{2^d}, a double exponential complexity. This is due to the algorithm producing many unnecessary constraints (constraints that are implied by other constraints). The number of necessary constraints grows as a single exponential.[1] Unnecessary constraints may be detected using linear programming.

See also[edit]

  • Real closed field: the cylindrical algebraic decomposition algorithm performs quantifier elimination over polynomial inequalities, not just linear.

References[edit]

  1. ^ David Monniaux, Quantifier elimination by lazy model enumeration, Computer aided verification (CAV) 2010.

External links[edit]