Simplifications symboliques

6 Simplifications symboliques

Nous présentons ici la plus forte valeur ajoutée de SPPoC , à savoir le système de calcul formel et en particulier les simplifications d'expressions et de systèmes de contraintes.

6.1 Présentation générale de l'implémentation

Le but poursuivi lors de l'écriture de SPPoC était d'offrir une interface de haut-niveau au calcul polyédrique. Les objectifs que nous nous sommes fixés sont donc les suivants :

avoir un outil complètement symbolique ;
proposer la même interface pour PIP , la PolyLib et l'Omega Library ;
simplifier automatiquement les systèmes d'(in)équations.

La structure de donnée centrale est le système de contraintes affines qui permet à la fois d'exprimer les contraintes des problèmes de programmation entière et de décrire des polyèdres. Comme ces contraintes doivent être affines, la forme affine à coefficients rationnels, somme d'une constante rationnelle et de produits d'une variable symbolique par un rationnel, joue un rôle central.

Comme les données que nous manipulons ont une forme très particulière, l'utilisation d'un système de calcul formel tel que Maple [19] ou Mathematica [25] serait d'une lourdeur inutile. En fait, SPPoC peut-être vu comme un composant spécialisé pour le calcul polyédrique qui pourrait être intégré dans un tel système. Nous avons donc choisi d'écrire un système de simplification adapté qui fait apparaître le plus de formes affines possible.

La suite de la présentation de ce système de simplification formelle est organisée ainsi : nous présentons d'abord la simplification des expressions arithmétiques, puis celle des systèmes de contraintes. Enfin, nous verrons comment manipuler des QUAST, structure de donnée qui a été introduite en section 3.

6.2 Expressions arithmétiques

En ayant à l'esprit le souci d'une utilisation la plus aisée possible, nous ne restreignons pas la forme des expressions arithmétiques que l'utilisateur peut entrer. C'est le système qui simplifie ces expressions en essayant de les linéariser au maximum. Une autre raison d'autoriser des expressions quelconques est qu'une sous-expression non linéaire peut être linéarisée plus tard par instanciation d'une variable ou simplification symbolique.

L'utilisateur peut par exemple entrer les expressions suivantes, qui sont automatiquement simplifiées.

# <:e<2*((i*m)^2) % 3>>;;
- : SPPoC.Expr.t = (2*((i*m)**2)) mod 3
# <:e<(n mod 2)*(2i+3*(j-i))-((3/3*n+0) mod 2)*(3j-i)>>;;
- : SPPoC.Expr.t = 0

Les opérateurs arithmétiques reconnus par l'algorithme sont : l'addition, la soustraction, la multiplication, la division rationnelle, l'élévation à la puissance, la division entière et le modulo (reste de la division entière). Les calculs numériques faisant intervenir ces opérateurs sont effectués en arithmétique rationnelle de précision arbitraire⁵, les éléments neutres et absorbants sont traités, les formes affines sont développées et les expressions non linéaires factorisées. Comme pour tout algorithme de simplification où une forme canonique n'est pas définie (développée ou factorisée ?), le résultat n'est pas garanti mais il fonctionne plutôt bien sur les expressions quasi-linéaires que nous rencontrons dans nos applications.

L'heuristique de simplification parcourt l'arbre représentant l'expression arithmétique en partant des feuilles et en remontant vers la racine en appliquant les simplifications au fur et à mesure. Ce parcours de l'arbre garantit sa terminaison et une complexité linéaire dans la taille de l'expression (nombre de noeuds de l'arbre par exemple).

6.3 Systèmes de contraintes

Nous avons constaté expérimentalement, en particulier dans [2], que les deux outils, PIP et la PolyLib , sont très sensibles à la forme de leur entrée. En effet, deux représentations équivalentes d'un même polyèdre peuvent mener à des résultats plus ou moins compliqués (bien qu'équivalents) ou encore faire échouer le calcul. En particulier, l'enchaînement de calculs, comme dans l'exemple de la section 7.2, peut être très difficile si les résultats intermédiaires ne sont pas simplifiées au fur et à mesure du calcul.

Pour permettre une simplification la plus poussée possible, nous avons classé les variables symboliques, appelées symboles dans la suite, en trois catégories :

les << vraies >> variables, c'est-à-dire sur lesquelles porte le calcul ;
les variables intermédiaires qui ne servent qu'à exprimer le problème, elles sont en fait quantifiées existentiellement ;
les paramètres du calcul.

L'algorithme de simplification va essayer de supprimer les variables intermédiaires et d'exprimer les variables en fonction des paramètres.

6.3.1 Linéarisation

Les systèmes de contraintes doivent être affines pour définir des polyèdres. Il faut donc linéariser ces systèmes. Afin de ne pas s'interdire des simplifications possibles, cette linéarisation est faite le plus tard possible. Elle consiste principalement à utiliser la définition de la division euclidienne (équation 3 ci-dessous) pour faire disparaître les divisions entières et les modulos en introduisant une variable intermédiaire supplémentaire.

ì
í
î

r º a b

q = a ÷ b

ÜÞ

ì
ï
í
ï
î

si b>0 alors

ì
í
î

a = bq + r

0 £ r < b

si b<0 alors

ì
í
î

a = bq + r

b < r £ 0

(3)

Cette transformation n'est utile que si b est un entier non nul. En effet, dans le cas contraire, on obtient un système non linéaire.

6.3.2 Simplifications élémentaires

Nous décrivons ici les simplifications élémentaires faites par notre algorithme. L'enchaînement de ces transformations et la preuve de terminaison de l'algorithme sont expliqués dans la section suivante.

Toutes les transformations sont en fait des substitutions d'un symbole par une expression représentant sa valeur, ce qui va de la propagation des constantes à des substitutions plus complexes en passant par la suppression d'un symbole en cas de proportionnalité entre deux symboles. À chaque fois qu'une substitution est faite dans une expression, celle-ci est systématiquement simplifiée par l'algorithme présenté ci-dessus.

Ces remplacements de définitions de symboles conduisent à la simplification de l'exemple suivant, qui en est linéarisé :

# System.simplify <:v<i,j,k>> <:v<n,m>>
  <:s<n=10; k=n*i+j; j=m*n; i<=j>>;;
- : SPPoC.System.t = {j = 10*m, n = 10, i <= 10*m, 10*i+10*m = k}

La fonction System.simplify prend comme arguments la liste des variables, la liste des paramètres et le système à simplifier. Tous les symboles n'apparaissant dans aucune des listes arguments sont considérés comme des variables intermédiaires.

Toutes ces substitutions peuvent faire apparaître des inéquations inutiles, du genre définition d'une variable intermédiaire qui n'est jamais utilisée. Ces inéquations sont supprimées. En modifiant l'exemple précédent pour faire apparaître une variable intermédiaire, on en constate la disparition après simplification :

# System.simplify <:v<i,j,k>> <:v<n,m>>
  <:s<n=10; k=n*i+j; x=m*n; i<=x+j>>;;
- : SPPoC.System.t = {n = 10, i <= j+10*m, 10*i+j = k}

6.3.3 Enchaînement des simplifications

L'algorithme d'enchaînement des simplifications est assez simple : tant qu'une simplification est possible, on fait la transformation correspondante. Ce schéma est légèrement modifié par un ordre de priorité donné aux transformations. On essaye en priorité les substitutions qui simplifient le plus le système, à savoir la propagation des constantes, ensuite la proportionnalité puis les substitutions de définitions et enfin la suppression d'inéquations inutiles. Pour détecter un maximum de définitions, c'est à dire d'expressions pouvant se mettre sous la forme « symbole = expression », les inéquations affines sont systématiquement simplifiées par le plus grand diviseur commun des coefficients de la forme affine. Cette heuristique nous semble efficace. En effet le résultat obtenu est au moins aussi simple que ce que nous obtenons en simplifiant « à la main » sur tous les cas que nous avons rencontrés.

Comme chaque simplification consiste en le remplacement d'un symbole par une expression ne faisant pas intervenir ce symbole, nous marquons ce symbole comme inactif dans la suite de l'algorithme. En effet, une nouvelle substitution de ce symbole n'apporterait rien. Le nombre de symboles dans un système étant fini, nous pouvons déduire que l'algorithme de simplification s'arrête et fait au plus n substitutions où n est le nombre de symboles apparaissant dans le système de contraintes.

6.4 Calculs avec les QUAST

Un QUAST, ou arbre de sélection quasi-affine, représente un point paramétré. La valeur de ce point dépend de celles des paramètres qui permettent de sélectionner une des feuilles de cet arbre de sélection. Les prédicats de sélection sont des inégalités affines et les feuilles des listes de formes affines, une pour chaque dimension de l'espace.

Cette structure de données permet de représenter les résultats des appels à PIP . Suite à la présence possible de nouveaux paramètres définis comme des modulos de formes linéaires dans un tel résultat, nous avons définis des « QUAST étendus » autorisant ces paramètres modulaires. Toutes les fonctions décrites ci-dessous s'appliquent aussi bien aux QUAST qu'aux QUAST étendus.

Outre les fonctions de création et de destruction des types abstraits QUAST et QUAST étendu (implémentés par les modules Quast et EQuast), nous avons défini des fonctions permettant de calculer avec de telles structures de données :

la simplification d'un QUAST ;
le calcul du minimum ou du maximum de deux QUAST ;
la « mise à plat » un QUAST, c'est-à-dire la récupération une liste de couples (système de contraintes, valeur). Cette fonctionnalité est nécessaire pour l'application de la section 7.2.

La simplification se fait d'après la remarque suivante : suivre une branche de sélection dans un QUAST construit un système de contraintes. On peut donc éliminer les branches inutiles parce qu'inatteignables en testant l'existence d'un point dans le domaine défini par ces contraintes. Cela peut se faire en cherchant un point particulier dans ce domaine, par exemple le minimum lexicographique qui se calcule par un appel à PIP . On fusionne de même les branches qui, après élagage, sont identiques pour faire disparaître des noeuds inutiles dans l'arbre de sélection.

C'est lors des calculs d'extrema que la taille des QUAST manipulés peut augmenter dangereusement et que des simplifications sont particulièrement nécessaires. D'ailleurs, si lors d'un tel calcul des paramètres définissant des modulos interviennent avec des noms différents dans les deux QUAST, ils sont unifiés pour offrir plus de possibilités de simplification.