Fourier–Motzkin elimination
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) for integer solutions.
The operation is named after Joseph Fourier and Theodore Motzkin.
Contents |
Elimination [edit]
Elimination (or ∃-elimination) of variables V from a system of relations (here, linear inequalities) consists in 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.
Let us consider a system
of
inequalities with
variables
to
, with
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
:
- those that are equivalent to some inequalities of the form
; let us note these as
, for
ranging from 1 to
where
is the number of such inequalities; - those that are equivalent to some inequalities of the form
; let us note these as
, for
ranging from
to
where
is the number of such inequalities; - those in which
plays no role, grouped into a single conjunction
.
The original system is thus equivalent to
.
Elimination consists in producing a system equivalent to
. Obviously, this formula is equivalent to
.
The inequality
is equivalent to
inequalities
, for
and
.
We have therefore transformed the original system into another system where
is eliminated. Note that the output system has
inequalities. In particular, if
, then the number of output inequalities is
.
Complexity [edit]
Running an elimination step over
inequalities can result in at most
inequalities in the output, thus running
successive steps can result in at most
, a double exponential complexity. This is due to the algorithm producing many unnecessary constraints (constraints that are implied by the other ones). 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]
- ^ David Monniaux, Quantifier elimination by lazy model enumeration, Computer aided verification (CAV) 2010
- Fourier, Joseph (1827). "Histoire de l'Académie, partie mathématique (1824)". 7. Gauthier-Villars. Text "Mémoires de l'Académie des sciences de l'Institut de France" ignored (help)
- Schrijver, Alexander (1998). Theory of Linear and Integer Programming. John Wiley & sons. pp. 155–156. ISBN 0-471-98232-6.
- Keßler, Christoph W. "Parallel Fourier–Motzkin Elimination". Universität Trier. CiteSeerX: 10.1.1.54.657.
- Williams, H. P. (1986). "Fourier's Method of Linear Programming and its Dual". American Mathematical Monthly 93: 681–695.
External links [edit]
- Lectures on Convex Sets, notes by Niels Lauritzen, at Aarhus University, March 2010.
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
; let us note these as
, for
ranging from 1 to
where
; let us note these as
, for
to
where
is the number of such inequalities;
.