# Élimination de Fourier-Motzkin

L'élimination de Fourier–Motzkin est un algorithme d'élimination des variables dans un système d'inégalités linéaires. Il s'agit d'une méthode de pivot apparentée à l'élimination de Gauss-Jordan, si ce n'est qu'elle s'applique au cas plus général où les relations sont des inégalités plutôt que des égalités. La méthode tire son nom de ses co-découvreurs Joseph Fourier et Theodore Motzkin.

## Principe

Considérons un système $S$ de $n$ inégalités sur $r$ variables $x_{1},\ldots ,x_{r}$. L'élimination des variables $x_{j+1},\ldots ,x_{r}$ consiste à calculer un nouveau système $S'$ ayant les mêmes solutions que $S$ sur les variables restantes $x_{1},\ldots ,x_{j}$.
L'algorithme de Fourier-Motzkin procède en éliminant une à une les variables du système initial. Éliminer toutes les variables $x_{1},\ldots ,x_{r}$ réduit le système à une inégalité triviale : le système initial admet alors des solutions si et seulement si l'inégalité triviale ainsi obtenue est vraie. Cette méthode peut ainsi être utilisée pour déterminer si un système d'inégalités $S$ admet ou pas des solutions.
Considérons l'élimination de la dernière variable $x_{r}$ du système S. Les inégalités de S peuvent être groupées en trois catégories selon le signe du coefficient de $x_{r}$ :
* celles de la forme $x_{r}\geq b_{i}-\sum _{k=1}^{r-1}a_{ik}x_{k}$, que nous noterons $x_{r}\geq A_{j}(x_{1},\dots ,x_{r-1})$, où $j$ est un indice entre 1 et $n_{A}$ avec $n_{A}$ le nombre de telles inégalités ;
* celles de la forme $x_{r}\leq b_{i}-\sum _{k=1}^{r-1}a_{ik}x_{k}$, que nous noterons $x_{r}\leq B_{j}(x_{1},\dots ,x_{r-1})$, où $j$ est un indice entre 1 et $n_{B}$ avec $n_{B}$ le nombre de telles inégalités ;
* enfin, celles où $x_{r}$ n'apparaît pas, qui ne jouent aucun rôle et que nous noterons $\phi$.
Le système initial est alors équivalent à :
    $\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}))\quad \wedge \quad \phi$.
où la conjonction finale $\wedge \phi$ indique que les inégalités où $x_{r}$ n'apparaît pas sont conservées dans le système réduit. L'élimination consiste alors à produire le système équivalent $\exists x_{r}~S$, dont la formule est, d'après la double inégalité ci-dessus :
    $\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}))\quad \wedge \quad \phi$.
L'inégalité :
    $\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}))$
est équivalente à un nouvel ensemble de $n_{A}n_{B}$ inégalités $A_{i}(x_{1},\dots ,x_{r-1})\leq B_{j}(x_{1},\dots ,x_{r-1})$, pour $1\leq i\leq n_{A}$ et $1\leq j\leq n_{B}$.
Nous avons ainsi transformé le système initial S en un nouveau système S' dans lequel la variable $x_{r}$ a été éliminée. Ce nouveau système compte $(n-n_{A}-n_{B})+n_{A}n_{B}$ inégalités.

## Complexité

Dans le pire des cas où $n_{A}=n_{B}=n/2$, la taille du système après élimination passe de $n$ à $n^{2}/4$. Ainsi, après $d$ éliminations successives, la taille du système obtenu dans le pire des cas est de l'ordre de $4(n/4)^{2^{d}}$, ce qui correspond à une complexité en mémoire doublement exponentielle.
Ce phénomène résulte du comportement paresseux de l'algorithme : chaque étape d'élimination produit un nombre potentiellement élevé d'inégalités redondantes, qui peuvent être retirées du système sans changer son ensemble de solutions (c'est-à-dire, de manière équivalente, qu'elles peuvent être déduites par combinaisons convexes d'autres inégalités du système). Les inégalités redondantes peuvent être détectées par programmation linéaire et retirées du système, au prix d'une plus grande complexité en temps.
Le nombre de contraintes nécessaires (non-redondantes) du système croît, quant à la lui, de manière simplement exponentielle.

## Extension : accélération de Imbert

Deux théorèmes d'« accélération » dus à Imbert permettent d'éliminer des inégalités redondantes du système en se basant uniquement sur des propriétés syntaxiques de l'arbre de dérivation des formules, et donc sans recours à la programmation linéaire ou à des calculs de rangs matriciels. Quelques définitions sont nécessaires avant de pouvoir énoncer ces résultats.
L'historique $H_{i}$ d'une inégalité $i$ du système est définie comme l'ensemble des indices des inégalités du système initial ayant servi à générer $i$. Les inégalités $i\in S$ du système initial vérifient tout d'abord $H_{i}=\{i\}$. Lors de l'ajout d'une nouvelle inégalité $k:A_{i}(x_{1},\dots ,x_{r-1})\leq B_{j}(x_{1},\dots ,x_{r-1})$ (par élimination de $x_{r}$), l'historique $H_{k}$ est ensuite construite comme $H_{k}=H_{i}\cup H_{j}$.
Supposons que les variables $O_{k}=\{x_{r},\ldots ,x_{r-k+1}\}$ ont été éliminées du système. Chaque inégalité $i$ du système actuel partitionne l'ensemble des variables éliminées $O_{k}$ en :
* $E_{i}$, l'ensemble des variables effectivement éliminées. Une variable $x_{j}$ est effectivement éliminée pour $i$ dès lors qu'au moins une des inégalités dans l'historique $H_{i}$ a été obtenue par élimination de $x_{j}$.
* $I_{i}$, l'ensemble des variables implicitement éliminées. Une variable est dite implicitement éliminée dès lors qu'elle apparaît dans au moins une des inégalités de l'historique $H_{i}$, sans apparaître dans $i$ ni être effectivement éliminée.
* $A_{i}$, les variables restantes.
Toute inégalité non-redondante a la propriété que son historique est minimale.
Premier théorème d'accélération de Imbert — Si l'historique $H_{i}$ d'une inégalité $i$ est minimale, alors $1+|E_{i}|\ \leq \ |H_{i}|\ \leq 1+\left|E_{i}\cup (I_{i}\cap O_{k})\right|$.
Une inégalité ne satisfaisant pas l'encadrement ci-dessus est nécessairement redondante et peut être éliminée du système sans changer l'ensemble des solutions.
Le second théorème fournit quant à lui un critère pour détecter les historiques minimales :
Second théorème d'accélération de Imbert — Si l'inégalité $i$ vérifie $1+|E_{i}|=|H_{i}|$, alors $H_{i}$ est minimale.
Ce théorème permet d'éviter de calculer d'autres vérifications plus coûteuses, telles que les éliminations basées sur des calculs de rangs matriciels. De plus amples détails d'implémentation sont donnés en référence.