Fourier–Motzkin elimination

From Wikipedia, the free encyclopedia

Fourier–Motzkin elimination, also known as the FME method, is a mathematical algorithm for eliminating variables from a system of linear inequalities. It can look for both real and in some cases integer solutions.

The operation is named after Joseph Fourier and Theodore Motzkin.

Elimination

Elimination (or ∃-elimination) of variables V from a system of relations (here, linear inequalities) consists of creating another system of the same kind, but without a subset of variables V, such that both systems have the same solutions over the remaining variables.

If one eliminates all variables from a system of linear inequalities, then one obtains a system of constant inequalities, which can be trivially decided to be true or false, such that this system has solutions (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 eliminate. 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

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

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

References

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

External links

This article is issued from Wikipedia. The text is available under the Creative Commons Attribution/Share Alike; additional terms may apply for the media files.