É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

modifier

Considérons un système   de   inégalités sur   variables  . L'élimination des variables   consiste à calculer un nouveau système   ayant les mêmes solutions que   sur les variables restantes  .

L'algorithme de Fourier-Motzkin procède en éliminant une à une les variables du système initial. Éliminer toutes les variables   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   admet ou pas des solutions.

Considérons l'élimination de la dernière variable   du système S. Les inégalités de S peuvent être groupées en trois catégories selon le signe du coefficient de   :

  • celles de la forme  , que nous noterons  , où   est un indice entre 1 et   avec   le nombre de telles inégalités ;
  • celles de la forme  , que nous noterons  , où   est un indice entre 1 et   avec   le nombre de telles inégalités ;
  • enfin, celles où   n'apparaît pas, qui ne jouent aucun rôle et que nous noterons  .

Le système initial est alors équivalent à :

 .

où la conjonction finale   indique que les inégalités où   n'apparaît pas sont conservées dans le système réduit. L'élimination consiste alors à produire le système équivalent  , dont la formule est, d'après la double inégalité ci-dessus :

 .

L'inégalité :

 

est équivalente à un nouvel ensemble de   inégalités  , pour   et  .

Nous avons ainsi transformé le système initial S en un nouveau système S' dans lequel la variable   a été éliminée. Ce nouveau système compte   inégalités.

Complexité

modifier

Dans le pire des cas où  , la taille du système après élimination passe de   à  . Ainsi, après   éliminations successives, la taille du système obtenu dans le pire des cas est de l'ordre de  , 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[1].

Extension : accélération de Imbert

modifier

Deux théorèmes d'« accélération » dus à Imbert[2] 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   d'une inégalité   du système est définie comme l'ensemble des indices des inégalités du système initial ayant servi à générer  . Les inégalités   du système initial vérifient tout d'abord  . Lors de l'ajout d'une nouvelle inégalité   (par élimination de  ), l'historique   est ensuite construite comme  .

Supposons que les variables   ont été éliminées du système. Chaque inégalité   du système actuel partitionne l'ensemble des variables éliminées   en :

  •  , l'ensemble des variables effectivement éliminées. Une variable   est effectivement éliminée pour   dès lors qu'au moins une des inégalités dans l'historique   a été obtenue par élimination de  .
  •  , 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  , sans apparaître dans   ni être effectivement éliminée.
  •  , les variables restantes.

Toute inégalité non-redondante a la propriété que son historique est minimale[3].

Premier théorème d'accélération de Imbert — Si l'historique   d'une inégalité   est minimale, alors  .

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é   vérifie  , alors   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[3].

Notes et références

modifier
  1. David Monniaux, Quantifier elimination by lazy model enumeration, Computer aided verification (CAV) 2010.
  2. Jean-Louis Imbert, About Redundant Inequalities Generated by Fourier's Algorithm, Artificial Intelligence IV: Methodology, Systems, Applications, 1990.
  3. a et b Jean-Louis Imbert, Fourier Elimination: Which to Choose?.

Sources

modifier