Élimination de Fourier-Motzkin

De testwiki
Aller à la navigation Aller à la recherche

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 x1,,xr. L'élimination des variables xj+1,,xr consiste à calculer un nouveau système S ayant les mêmes solutions que S sur les variables restantes x1,,xj.

L'algorithme de Fourier-Motzkin procède en éliminant une à une les variables du système initial. Éliminer toutes les variables x1,,xr 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 xr du système S. Les inégalités de S peuvent être groupées en trois catégories selon le signe du coefficient de xr :

  • celles de la forme xrbik=1r1aikxk, que nous noterons xrAj(x1,,xr1), où j est un indice entre 1 et nA avec nA le nombre de telles inégalités ;
  • celles de la forme xrbik=1r1aikxk, que nous noterons xrBj(x1,,xr1), où j est un indice entre 1 et nB avec nB le nombre de telles inégalités ;
  • enfin, celles où xr n'apparaît pas, qui ne jouent aucun rôle et que nous noterons ϕ.

Le système initial est alors équivalent à :

max(A1(x1,,xr1),,AnA(x1,,xr1))  xr  min(B1(x1,,xr1),,BnB(x1,,xr1))ϕ.

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

max(A1(x1,,xr1),,AnA(x1,,xr1))  min(B1(x1,,xr1),,BnB(x1,,xr1))ϕ.

L'inégalité :

max(A1(x1,,xr1),,AnA(x1,,xr1))  min(B1(x1,,xr1),,BnB(x1,,xr1))

est équivalente à un nouvel ensemble de nAnB inégalités Ai(x1,,xr1)Bj(x1,,xr1), pour 1inA et 1jnB.

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

Complexité

Dans le pire des cas où nA=nB=n/2, la taille du système après élimination passe de n à n2/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)2d, 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

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 Hi 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 iS du système initial vérifient tout d'abord Hi={i}. Lors de l'ajout d'une nouvelle inégalité k:Ai(x1,,xr1)Bj(x1,,xr1) (par élimination de xr), l'historique Hk est ensuite construite comme Hk=HiHj.

Supposons que les variables Ok={xr,,xrk+1} ont été éliminées du système. Chaque inégalité i du système actuel partitionne l'ensemble des variables éliminées Ok en :

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

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

Modèle:Théorème

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 :

Modèle:Théorème

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

  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. 3,0 et 3,1 Jean-Louis Imbert, Fourier Elimination: Which to Choose?.

Sources

Modèle:Portail