JEUDI 18 AVRIL 2024
08h00-12h00
FILIERE MPI - Epreuve
INFORMATIQUE C (XULSR)
Égalités et différences
Le sujet comporte 17 pages, numérotées de 1 à 17 et une annexe.
Vue d'ensemble du sujet.
Ce sujet traite du problème de satisfiabilité de formules construites par la conjonction de contraintes d'égalité et de différence (dis-égalité) entre expressions. Ce problème se présente, par exemple, dans la compilation de programmes, quand on cherche à réduire des expressions complexes (nécessitant beaucoup de calculs) vers des expressions plus simples, en utilisant les propriétés des opérateurs apparaissant dans ces expressions. Par exemple, si x est une variable entière, est une contrainte d'égalité entre deux expressions écrites en C. De même, si et sont des variables booléennes, l'égalité permet de simplifier l'expression C écrite à gauche de l'égalité.
Il est important de savoir si un ensemble donné de contraintes d'égalité ou de différence est satisfiable. Dans la suite, est le problème suivant : «Étant donnée une formule , conjonction de contraintes de la classe , décider si F est satisfiable ».
Ce sujet propose d'étudier la complexité du problème et les algorithmes pour le résoudre dans le cas de quatre classes de contraintes :
La partie I considère la classe où les contraintes ont la forme ou avec , et des variables propositionnelles (c'est-à-dire, ayant des valeurs booléennes).
La partie II concerne la classe incluant les contraintes de la classe et celles de la forme (entre autres) avec et des variables propositionnelles. Les algorithmes des deux premières parties seront codés en OCaml.
La partie III s'intéresse à la classe des contraintes de la forme ou avec et des variables entières.
Enfin, la partie IV concerne les contraintes d'égalité et de différence entre les expressions construites à partir de variables entières et de fonctions à deux arguments. Les algorithmes des deux dernières parties seront codés en C .
Les parties III et IV peuvent être traitées indépendamment de parties I et II. Il est recommandé de traiter les parties I et II de manière séquentielle. De même pour les parties III et IV.
Notations
Les contraintes seront construites en utilisant un ensemble de variables notées avec . Une valeur de vérité est un élément de où 1 représente le vrai et 0 le faux. Une valeur entière est un élément de et sa valeur absolue est notée . Étant donnés avec , l'intervalle [ ] est l'ensemble des tels que .
Logique propositionnelle. On utilisera les formules de la logique propositionnelle construites à partir de l'ensemble de variables propositionnelles , les constantes propositionnelles (faux) et (vrai), les connecteurs logiques classiques (négation), (conjonction), (disjonction). On définit (implication) par , et (équivalence) . Pour les connecteurs et , on utilise leur forme -aire avec . Par exemple, est une formule utilisant une conjonction -aire. Par convention, une conjonction 0 -aire est T , et une disjonction 0 -aire est ; une conjonction (resp. disjonction) unaire est identique à son opérande.
Un littéral est soit une variable soit sa négation . Une formule est en forme normale conjonctive (CNF) si c'est une conjonction de disjonctions de littéraux. Une formule est en forme -CNF avec , si elle est en forme CNF et le nombre de littéraux différents dans chaque disjonction est au plus . Par exemple, la formule est en forme 3-CNF.
On rappelle qu'une formule propositionnelle peut être satisfaite ou non par une valuation , qui assigne une valeur de vérité à chaque variable. On note la relation de satisfaction. Une formule est conséquence logique de , noté , quand, pour toute valuation telle que , on a aussi . Deux formules sont logiquement équivalentes lorsque chacune est conséquence logique de l'autre (ou, de façon équivalente, quand elles sont satisfaites par les mêmes valuations). Une formule est une tautologie si elle est satisfaite par toutes les valuations. Une formule est une contradiction (antilogie) ou contradictoire si elle n'est satisfaite par aucune valuation. Une formule est satisfiable s'il existe une valuation telle que .
L'annexe rappelle certaines règles de la déduction naturelle.
Complexité. Par la complexité d'un algorithme on entend le nombre d'opérations élémentaires (comparaison, addition, soustraction, multiplication, division, affectation, test, etc.) nécessaires à l'exécution de A dans le pire cas. Lorsque la complexité dépend d'un ou plusieurs paramètres , on dit que a une complexité en s'il existe une constante telle que, pour toutes les valeurs de suffisamment grandes (c'est-à-dire plus grandes qu'un certain seuil), pour toute instance du problème de paramètres la complexité est au plus . De même, on dit que a une complexité en s'il existe deux constantes et telles que, pour toutes les valeurs de suffisamment grandes, la complexité de est au moins et au plus . Dans tout ce sujet, on note «log» le logarithme à base 2 , et on utilisera exclusivement ce logarithme.
Programmation. Dans les questions de programmation en C et OCaml, on n'utilise que les fonctions qui sont incluses dans la bibliothèque standard du langage.
Pour le code écrit en C, on suppose que les en-têtes stdbool.h, stdio.h, stdlib.h et assert.h ont été inclus.
On rappelle quelques opérations sur les listes en OCaml.
List.iter f lst applique la fonction f : ' unit à chaque élément de la liste lst de type 'a list. Si la complexité de f est en , alors la complexité de List.iter est en , où est la longueur de lst.
List.map f lst renvoie la liste de type 'b list obtenue en appliquant la fonction f : ' ' b à chaque élément de la liste lst de type ' a list. Si la complexité de f est en , alors la complexité de List.map est en , où est la longueur de lst.
List.mem e lst renvoie true si et seulement si e est un élément de lst. Si la complexité du test d'égalité est en , la complexité de List.mem est en , où est la longueur de lst.
List.exists f lst renvoie true si et seulement s'il existe au moins un élément e de lst (liste de type 'a list) tel que e renvoie true avec 'a bool. Si la complexité de f est en , alors la complexité de List. exists est en , où est la longueur de lst.
List.for_all f lst renvoie true si et seulement si tous les éléments de lst (de type 'a list) satisfont le prédicat f : ' bool. Si la complexité de f est en , alors la complexité de List.for_all est en , où est la longueur de lst.
List.filter f lst renvoie la liste de tous les éléments de lst (de type 'a list) qui satisfont le prédicat f : ' bool. Si la complexité de f est en , alors la complexité de List.filter est en , où est la longueur de lst.
On rappelle quelques opérations sur les tableaux en OCaml.
Array. length tab renvoie la longueur du tableau tab en temps .
Array.make k v crée un tableau de k éléments, tous initialisés à v , en temps .
La valeur à la case numéro i du tableau tab est tab. (i). Les cases sont numérotées à partir de zéro et l'accès est fait en temps .
L'affectation de la case i du tableau tab avec la valeur v s'écrit tab. (i) <- v; sa complexité est en .
Array.copy tab crée une copie du tableau tab en temps avec la longueur du tableau en argument.
Partie I. Équivalences de littéraux
Dans cette partie, on se place dans le cadre de la logique propositionnelle. On définit comme la classe des contraintes de la forme avec et des littéraux. Une formule est dite construite sur , notation , si elle est une conjonction de contraintes de . Dans cette partie, on considère que la variable est toujours interprétée à 1 , donc qu'elle représente la valeur de vérité vrai. La formule définie ci-dessous est dans :
Question 1. Donner une formule logiquement équivalente à en forme 2-CNF.
Question 2. Donner une réduction en temps linéaire du problème au problème de satisfiabilité des formules en 2-CNF.
Mise en œuvre en OCaml. Une contrainte de est représentée par un couple d'entiers avec . Pour tout , le littéral représenté par , noté lit , est si et si . Par la convention sur l'interprétation de , l'entier (resp. ) représente la valeur de vérité 1 (resp. 0). Enfin, une formule dans est représentée par la liste des couples correspondant aux contraintes dont la formule est conjonction. Par convention, la liste vide représente . Le nombre de variables, , est une variable globale entière. Ce codage est donné par les déclarations OCaml ci-dessous :
type contr1 = int * int (* contraintes L1 *)
type eform1 = contr1 list (* formules L1 *)
exception Bad_literal of int
exception Exn_unsat
Les exceptions déclarées ci-dessus seront utilisées dans les fonctions de cette partie et de la partie suivante.
Question 3. Écrire les fonctions suivantes:
var_of_lit: int -> int renvoie l'index de la variable apparaissant dans le littéral représenté par l'argument . Par exemple, pour , la fonction renvoie 3 si l'argument est 3 , et 2 si l'argument est 7 . Si alors la fonction exécute raise (Bad_literal i).
neg_lit: int -> int renvoie, pour un argument , l'entier tel que lit est logiquement équivalent à ; si alors la fonction exécute raise (Bad_literal i).
eform1_is_wf: eform1 -> bool renvoie true si et seulement si l'argument est «bien formé », c'est-à-dire qu'il contient uniquement des entiers qui représentent des littéraux sur l'ensemble de variables .
Dans la suite de ce sujet, on suppose que tous les entiers utilisés par les valeurs de type contr1 et eform1 représentent des littéraux sur l'ensemble de variables . Par conséquent, l'exception Bad_literal ne doit pas être levée.
Graphe d'une formule. Le graphe associé à , noté , est un graphe non orienté dont les sommets sont les entiers dans l'intervalle . Les arêtes sont les ensembles tels que et contient soit la contrainte , soit la contrainte avec et égaux respectivement à neg_lit et neg_lit . Par exemple, pour , la contrainte ( ) est représentée par les arêtes et . On note que les contraintes de de la forme ne sont pas représentées par .
Question 4. On suppose . Pour chacune des formules suivantes, donner le graphe associé :
On suppose disposer d'une bibliothèque munie d'un type graph et qui code des graphes non orientés. Les sommets sont représentés par des entiers. Les opérations suivantes sont disponibles pour la construction et l'exploration des graphes :
g_create : int -> graph renvoie une valeur représentant un graphe sans arêtes et ayant sommets, où est donné en argument, supposé strictement positif. Les sommets sont numérotés de 1 à . La complexité de cette opération est en .
g_add_edge : graph -> int -> int -> unit ajoute au graphe donné comme premier argument l'arête entre les sommets donnés en 2ème et 3ème arguments. Si les sommets en argument ne sont pas déclarés dans le graphe ou si l'arête existe déjà, alors cette fonction ne change pas le graphe. Sinon, le graphe est modifié en place. La complexité de cette opération est en , avec le nombre de sommets du graphe.
g_nb_vertex : graph -> int renvoie le nombre de sommets du graphe en argument. La complexité de cette opération est en .
g_succ : graph -> int -> int list renvoie la liste des sommets adjacents du sommet en second argument dans le graphe donné en premier argument. Si le sommet en argument n'existe pas, la liste renvoyée est vide. La complexité de cette opération est en .
Question 5. Écrire une fonction eform1_to_graph: eform1 -> graph qui renvoie le graphe associé à la formule représentée par l'argument. Si contient une contrainte de la forme , alors la fonction lève l'exception Exn_unsat.
Lorsqu'un appel à eform1_to_graph lst lève l'exception Exn_unsat, la formule représentée par lst contient toujours une contrainte contradictoire. Cependant, une formule peut être une contradiction sans que l'exception soit levée, comme c'est le cas de la formule ( .
Question 6. Donner et justifier soigneusement la complexité de eform1_to_graph en fonction de et de la longueur de la liste en argument.
Soient une formule et g la représentation de , le graphe associé à . On note par l'ensemble des ensembles de sommets des composantes connexes de . Soit la taille de , c'est-à-dire, le nombre de composantes connexes de . On représente par un tableau c de entiers, qui associe à chaque , sommet de g , un entier dans l'intervalle . Ainsi, c. (i) identifie de manière unique la composante connexe du sommet i. La case de c à la position 0 ne sera pas utilisée, mais elle permet d'utiliser directement les indices des variables comme positions de c. Par convention, c. (0) est 0.
Question 7. Écrire une fonction g_cc_array: graph -> (int array * int) qui renvoie le couple ( ), où c est le tableau des composantes connexes du graphe en argument et où est le nombre de composantes connexes.
Question 8. Démontrer que si et sont des sommets distincts appartenant à la même composante connexe de , alors .
Question 9. Soit l'ensemble des sommets d'une composante connexe de . Soit l'ensemble de sommets avec pour tout . Démontrer que est élément de .
Question 10. Démontrer que est une contradiction si et seulement s'il existe une composante connexe de et un sommet de tels que neg_lit est un sommet de .
Question 11. Écrire une fonction cc_is_sat: int array bool qui a comme argument c, le tableau représentant les composantes connexes de et qui renvoie true si et seulement si est satisfiable.
Représentation d'une valuation. Une valuation de est représentée par un tableau v de valeurs 0 ou 1 tel que v . (i) est 1 si et seulement si . En particulier, v. (1)=1 par convention sur . La case à la position 0 n'est pas utilisée, mais elle permet d'utiliser les indices des variables comme positions du tableau; par convention, v. (0) est 0 .
Question 12. Écrire une fonction eform1_sat: eform1 (int array) option qui a comme argument une liste lst représentant une formule . L'appel eform1_sat lst renvoie None si est une contradiction. Si est satisfiable, l'appel renvoie Some(v) avec v un tableau qui représente une valuation qui satisfait . La complexité en temps de l'algorithme doit être en où est la longueur de la liste lst en argument. Justifier que votre algorithme a cette complexité en temps.
Partie II. Équivalences avec une conjonction de deux littéraux
On reste dans le cadre de la logique propositionnelle, mais on considère une nouvelle classe de contraintes. La classe contient les contraintes de la forme où sont des littéraux. Pour identifier les contraintes des classes et , on appelle -contrainte une contrainte de la classe avec . Une formule est dite construite sur , notation , si elle est une conjonction de 2 -contraintes. On garde l'hypothèse que est toujours interprétée . Un exemple de formule de est :
Question 13. Donner une réduction en temps polynomial du problème au problème de satisfiabilité des formules en 3-CNF.
Question 14. Donner une dérivation formelle (preuve en déduction naturelle) du séquent suivant :
Les règles de la déduction naturelle à utiliser dans cette preuve sont rappelées dans l'annexe.
En utilisant la convention sur l'interprétation de , toute 1 -contrainte est logiquement équivalente à la 2 -contrainte . À l'inverse, certaines 2 -contraintes sont logiquement équivalentes à des formules de . Par exemple, les équivalences logiques suivantes sont vraies pour tout couple de littéraux et (les preuves ne sont pas demandées) :
Dans la suite de cette partie, on dénote par toutes les équivalences définies sur l'ensemble des littéraux par les équivalences de (1) à (6) et par leur variantes obtenues en utilisant la symétrie de la conjonction. Par exemple, « équivalent à » est également une équivalence de , grâce à la symétrie de la conjonction appliquée à (1).
Mise en œuvre en OCaml. Une 2-contrainte est représentée par un enregistrement avec trois champs entiers. Les entiers de ces enregistrements prennent des valeurs dans et représentent des littéraux avec la même convention de codage qu'en première partie. Une formule dans est représentée par une liste d'enregistrements; la liste vide représente T. Ce codage est donné par les types OCaml suivants :
type contr2 = { ll: int; lr1: int; lr2: int } (* contraintes L2 *)
type eform2 = contr2 list (* formules L2 *)
Une valeur e de type contr2 représente la 2 -contrainte e. e. e. .
Dans la suite de cette partie, on suppose que toutes les valeurs des types contri et eform avec sont bien formées, c'est-à-dire que les entiers qu'elles contiennent représentent des littéraux sur .
Question 15. Écrire la fonction contr2_simplify_eq5: contr2 -> eform1 option qui applique l'équivalence (5) pour simplifier la 2-contrainte en argument. L'appel contr2_simplify_eq5 e2:
renvoie None si la simplification ne peut pas être faite avec (5);
lève l'exception Exn_unsat (déclarée en partie I) si la simplification peut être faite mais la 2 -contrainte représentée par e2 est une contradiction;
enfin, renvoie Some [(1,e2.lr1); (1,e2.lr2)] si la simplification peut être effectuée sans détecter de contradiction.
Valuation partielle. Une valuation partielle est une fonction telle que . Pour tout , si alors on dit que assigne à . Si alors on dit que n'est pas assignée par . On étend la notion de valuation partielle aux littéraux et aux formules comme suit : si avec , et si .
Soit la 1 -contrainte . Si alors si et 0 sinon. Si au moins une des valeurs ou est -1 , alors .
Pour la conjonction de deux littéraux si au moins une des valeurs ou est -1 ; sinon la valeur de est 1 si et seulement si et .
Soit la 2-contrainte . Si alors si et 0 sinon. Si au moins une des valeurs ou est -1 , alors .
La valeur d'une formule où pour une valuation partielle , notation , est -1 s'il existe une contrainte de telle que ; sinon, si pour toute contrainte de on a , et sinon.
Une valuation partielle est compatible avec une valuation si pour tout tel que on a .
Une valuation partielle est représentée en OCaml par un tableau v de taille dont les éléments appartiennent à . Comme pour les valuations, la case de position 0 n'est pas utilisée et, par convention, v. (0)=0.
Question 16. Écrire la fonction eform1_of_valp: int array -> eform1 qui renvoie une formule de telle que encode les assignations de la valuation partielle v en argument. Ainsi, un appel à eform1_of_valp v renvoie la liste de couples tels que et si alors et si alors .
Soit la formule représentée par le résultat de l'appel à eform1_of_valp v. Démontrez que, pour toute valuation on a si et seulement si v est compatible avec .
Une 2-contrainte peut être simplifiée en présence d'une valuation partielle en une formule de . Par exemple, si alors la 2-contrainte a la même valeur que la 1-contrainte pour la valuation partielle . On suppose donnée une fonction contr2_simplify_valp: contr2 -> int array -> eform1 option qui applique les équivalences de pour simplifier la 2 -contrainte e2 en premier argument en tenant compte de
la valuation partielle vp donnée comme second argument. Plus précisement, si vp(e2)=0, alors la fonction lève l'exception Exn_unsat. Si aucune simplification ne s'applique, alors le résultat est None. Si e2 est simplifiable, le résultat est Some(lst) avec lst une liste représentant une formule de obtenue par simplification de e2 telle que . La complexité de contr2_simplify_valp est en .
Algorithme. Les questions suivantes vous guident pour prouver la correction et la terminaison de l'algorithme de décision pour qui est mis en œuvre dans la fonction eform2_sat de la figure 1.
On cherche à démontrer que la fonction eform2_sat est correcte, c'est-à-dire qu'un appel à eform2_sat 1st0 doit renvoyer None si la formule représentée par 1st0 est une contradiction. Sinon, l'appel doit renvoyer Some(v) où v est un tableau qui représente une valuation qui satisfait . L'algorithme mis en œuvre pour eform2_sat est un algorithme de type retour sur trace (backtracking) dont le principe est de réduire la formule en une formule de afin d'appliquer eform1_sat, l'algorithme polynomial de la partie I. Pour effectuer cette réduction, eform2_sat appelle à la ligne 5 la fonction récursive eform2_sat_aux dont les arguments sont une liste 12 représentant une formule , une liste 11 représentant une formule et une valuation partielle vp.
La correction de eform2_sat_aux est un lemme important de la preuve de correction de eform2_sat. Un appel à eform2_sat_aux 1211 vp est correct s'il renvoie un tableau qui représente une valuation telle que et vp est compatible avec , si une telle valuation existe; sinon, l'appel doit lever l'exception Exn_unsat.
La mise en œuvre de eform2_sat_aux cherche à compléter la valuation partielle vp en assignant des valeurs à certaines variables (non assignées) qui apparaissent dans les littéraux de et qui permettent de simplifier en une formule de . Pour savoir si une 2-contrainte e2 de 12 peut être simplifiée en présence de vp, on appelle contr2_simplify_valp e2 vp (ligne 15). Si e2 se simplifie, l'argument 11 accumule les formules de obtenues par la simplification et eform2_sat_aux continue la simplification du reste des contraintes de 12 (ligne 17). Si la contrainte e2 est une contradiction en présence de vp, l'exception Exn_unsat est levée par contr2_simplify_valp e2 vp. Si e2 ne peut pas être simplifiée (ligne 19), alors eform2_sat_aux explore les simplifications de la contrainte e2 obtenues en assignant la variable du littéral e2.lr1 à chaque valeur de . L'exploration d'une assignation est faite grâce à un appel récursif à eform2_sat_aux avec le paramètre représentant la valuation partielle mis à jour avec l'assignation choisie.
Quand toutes les 2-contraintes de ont été simplifiées, c'est-à-dire quand la liste 12 est vide (ligne 10), eform2_sat_aux appelle eform1_sat avec l'argument (l1'@l1) où la liste l1' est obtenue par l'appel à eform1_of_valp vp. Si l'appel à eform1_sat (l1'@l1) renvoie Some(v), alors le résultat de eform2_sat_aux est v. Sinon, eform2_sat_aux lève l'exception Exn_unsat. Ceci a comme effet de revenir dans un appel précédent (sur la pile d'appels) de eform2_sat_aux pour explorer une autre assignation (lignes 25-28) ou, si toutes les assignations ont été explorées, de terminer l'appel à eform2_sat_aux 1211 vp par l'exception Exn_unsat.
Question 17. Démontrer que tout appel eform2_sat lst0 termine.
Question 18. Démontrer que la fonction eform2_sat est correcte en supposant que la fonction eform2_sat_aux est correcte.
Dans les trois questions suivantes, on cherche à démontrer les principaux cas de la correction de eform2_sat_aux.
let rec eform2_sat (lst:eform2) : (int array) option =
try
let vinit = Array.make (n+1) (-1) in (
vinit.(0) <- 0; vinit.(1) <- 1;
Some (eform2_sat_aux lst [] vinit) )
with Exn_unsat -> None
and eform2_sat_aux (12:eform2) (l1:eform1) (vp:int array) : int array =
match l2 with
| [] -> let l1' = eform1_of_valp vp in
let r = eform1_sat (l1'@l1) in
(match r with None -> raise Exn_unsat | Some v -> v)
| e2::12' ->
match contr2_simplify_valp e2 vp with
Some l1' -> (* simplification *)
eform2_sat_aux l2' (l1'@l1) vp
| None -> (* branchement sur valeur de e2.lr1 *)
let xlr1 = var_of_lit e2.lr1 in
try
let vp1 = Array.copy vp in (
vp1.(xlr1) <- 1;
eform2_sat_aux l2 l1 vp1 )
with Exn_unsat ->
let vp0 = Array.copy vp in (
vp0.(xlr1) <- 0;
eform2_sat_aux l2 l1 vp0 )
Figure 1 - Mise en œuvre OCaml de l'algorithme de décision pour
Question 19. Démontrez la correction de eform2_sat_aux quand son premier argument est la liste vide, on supposant que les fonctions eform1_of_valp et eform1_sat sont correctes.
Question 20. Soit un appel eform2_sat_aux 1211 vp tel que 12 est e2::12' et contr2_simplify_vp e2 vp renvoie Some l1'. Démontrez la correction d'un tel appel en supposant que l'appel récursif à eform2_sat_aux de la ligne 17 est correct.
Question 21. Soit un appel eform2_sat_aux 1211 vp tel que 12 est e2::12' et contr2_simplify_vp e2 vp renvoie None. Démontrez la correction d'un tel appel en supposant que les appels récursifs aux lignes 24 et 28 sont corrects.
Question 22. Donner la complexité de eform2_sat en fonction de la longueur de la liste en argument et du nombre de variables .
Partie III. Égalités et différences entre entiers
Dans cette partie, le domaine d'interprétation des variables est . La classe est constituée de contraintes de la forme et , avec . Une formule est dite construite sur , notation , si elle est une conjonction de contraintes de . Une valuation est une fonction qui assigne une valeur dans à chaque variable. Une valuation satisfait une contrainte (resp. ) si et seulement si (resp. ). Une valuation satisfait une formule si et seulement si satisfait chaque contrainte de . Les notions de conséquence logique, équivalence logique, tautologie et antilogie sont définies de manière similaire à la logique propositionnelle.
Le problème peut être réduit (en temps polynomial en et en la taille de la formule) au problème de satisfiabilité d'une formule propositionnelle. Dans cette partie, on étudie un algorithme polynomial en et en la taille de la formule pour .
Mise en œuvre en langage . On propose de représenter les formules de par des listes simplement chaînées acycliques de type eform3_t*. Chaque cellule c (de type eform3_t) d'une telle liste représente une contrainte grâce à trois données : un booléen c.is_eq qui est vrai si et seulement si est une égalité, et deux entiers positifs c.xi et c.xj qui représentent les indices des variables utilisées par . La formule est représentée par la liste vide de valeur NULL. On suppose que le nombre de variables dans est déclaré comme une variable globale entière. Enfin, on suppose que toute structure eform3_t est bien formée, c'est-à-dire que tous les entiers qu'elle contient appartiennent à l'intervalle .
Question 23. Donner la déclaration du type eform3_t.
Question 24. Écrire la fonction void eform3_print(eform3_t *lst) qui affiche sur la sortie standard chaque contrainte (par exemple, sous la forme ) de la formule représentée par lst, une contrainte par ligne; si lst est NULL, la fonction affiche true sur une ligne.
Classes d'équivalence avec «unir et trouver». On utilise une structure unir et trouver (union-find) pour résoudre le problème . On suppose disposer d'une bibliothèque C qui fournit une implémentation d'une structure unir et trouver sur des ensembles d'entiers. Cette bibliothèque exporte les déclarations de types et de fonctions suivantes :
/* Rappel: definition dans stdlib.h
typedef unsigned int size_t; */
struct uf_s { /* type unir et trouver (union-find) */
size_t nelem; /* nombre d'elements de l'ensemble */
int *parent; /* tableau de taille nelem = relation parent */
... /* champs utiles pour operations en O(log n) */
};
typedef struct uf_s uf_t;
uf_t *uf_create(size_t sz);
int uf_find(uf_t *cs, int i);
void uf_union(uf_t *cs, int i1, int i2);
Dans ce qui suit, on supposera les propriétés suivantes de cette implémentation :
uf_create(s) renvoie un pointeur cs vers une structure unir et trouver allouée dans le tas et qui représente une partition de l'ensemble où chaque élément de l'ensemble est seul dans sa classe d'équivalence; donne la valeur du champ cs->nelem.
uf_find(cs,i) renvoie la classe de i, c'est-à-dire un entier entre 0 et cs->nelem-1 qui est le représentant de cette classe.
uf_union(cs,i1,i2) fusionne les classes de i1 et i2 en modifiant la structure *cs.
Si cs est un pointeur valide vers une structure uf_t avec cs->nelem==s, le champ cs->parent pointe vers un tableau de entiers ayant des valeurs dans l'intervalle ; ce tableau encode la relation représentant d'une classe d'équivalence. Si cs->parent [i]==j alors i est dans la classe de j. Le tableau cs->parent est initialisé par uf_create de sorte que cs->parent[i]==i. Les opérations ci-dessus sur la structure unir et trouver ont une complexité en pour uf_create et en pour uf_find et uf_union.
Pour notre problème, l'ensemble de valeurs à partitionner sera , c'est-à-dire l'ensemble d'indices de variables dans auquel on ajoute la valeur 0 . La valeur 0 ne sera pas utilisée, mais elle permet d'utiliser directement les indices des variables comme positions du tableau cs->parent.
Question 25. Écrire la fonction uf_t *eform3_to_uf (eform3_t lst) qui renvoie une valeur de type uf_t représentant les classes d'équivalence sur définies par les contraintes d'égalité de la formule représentée par lst. On suppose que lst n'est pas vide. Les contraintes de différence de lst seront ignorées dans cette fonction.
Algorithme de décision. D'après la question précédente, la structure unir et trouver permet donc de représenter les contraintes d'égalité d'une formule de , mais pas les contraintes de différence.
Question 26. Écrire une fonction bool eform3_sat_int(eform3_t *lst) qui renvoie true si et seulement si toutes les contraintes de différence de la formule représentée par lst peuvent être satisfaites en respectant les contraintes d'égalité de lst. Si lst est NULL, la fonction renvoie true. Justifier la correction de la fonction eform3_sat_int, c'est-à-dire, que tout appel à cette fonction renvoie true si et seulement si la formule représentée par son argument est satisfiable.
Question 27. On suppose que 1st (de type eform3_t*) représente une formule avec un nombre de contraintes d'égalité égal à et un nombre de contraintes de différence égal à . Donner la complexité de l'appel à eform3_sat_int(lst) en fonction de et .
Calculer une valuation. Dans la suite de cette partie, on se propose de calculer, si elle existe, une valuation qui satisfait une formule de .
Question 28. Écrire une fonction int uf_classes(uf_t *cs) qui renvoie le nombre de classes d'équivalence de la structure unir et trouver pointée par cs ; si cs est NULL alors la fonction renvoie 0 . Cette fonction doit avoir une complexité en .
Question 29. Écrire une fonction int *uf_valuation (uf_t *cs) qui renvoie un pointeur v vers un tableau de entiers, alloué dans le tas. Soit le résultat de l'appel de uf_classes(cs). On suppose . Pour tout , est une valeur entière dans l'intervalle qui
est associée de façon unique à (chaque élément de) la classe d'équivalence de . La case à la position 0 de v n'est pas utilisée, mais elle permet d'utiliser les indices des variables comme positions de v ; par convention, . La fonction uf_valuation doit avoir une complexité en .
Soit une formule représentée par une liste lst différente de NULL telle que eform3_sat_int(lst) renvoie true. Soient cs le résultat de l'appel à eform3_to_uf(lst) et v le résultat de l'appel à uf_valuation(cs).
Question 30. Démontrer que v pointe vers un tableau qui représente une valuation qui satisfait la formule représentée par 1st.
Question 31. Si ne contient pas de contraintes de différence, alors quel est le nombre minimal de valeurs que peut avoir l'image d'une valuation qui satisfait ? Donner un exemple d'une telle valuation.
La même question si contient une seule contrainte de différence.
Question 32. Lorsque cela est possible, on souhaite construire une valuation telle que satisfait la formule et l'image de est un ensemble de taille 2 . Quel algorithme sur les graphes peut être utilisé pour obtenir ce résultat et sur quel graphe? Vous devez définir formellement le graphe en entrée de l'algorithme et donner la complexité de l'algorithme.
Partie IV. Égalités et différences d'expressions
Soit un ensemble de symboles de fonction notés . Chaque symbole représente une fonction de dans . Comme dans la partie III, on interprète les variables de dans l'ensemble . Les symboles de fonctions de ne sont pas interprétés, c'est-à-dire qu'ils n'ont pas de définition. Les seules propriétés connues de ces fonctions sont données sous la forme de contraintes d'égalité ou de différence. Ces contraintes sont celles de la classe définie ci-dessous.
Les contraintes de la classe utilisent des termes. Un terme est défini de manière inductive : est
soit , une variable de ,
soit , l'application d'une fonction sur deux termes et , appelés aussi sous-termes directs de .
Le symbole racine du terme (resp. ) est (resp. ). On note l'ensemble des termes construits avec les variables de et les symboles de fonctions .
Ces termes peuvent être représentés par des arbres binaires. La figure 2 représente les arbres binaires correspondants aux termes:
Chaque noeud de ces arbres est étiqueté en partie haute par un nom unique appelé identifiant, et en partie basse par le symbole racine du terme. L'arc à gauche (resp. droite) d'un noeud correspond au premier (resp. second) sous-terme direct et est dessiné avec un trait en pointillé (resp. plein).
Figure 2 - Arbres des termes (à gauche) et (à droite)
L'ensemble des sous-termes d'un terme , noté , est défini de manière inductive par
Question 33. Donner et pour les termes et définis ci-dessus.
La classe contient les contraintes de la forme ou avec et des termes. Une formule de est une conjonction de contraintes . L'ensemble des sous-termes d'une contrainte de la forme ou est . L'ensemble des sous-termes d'une formule de , noté , est défini comme l'union des ensembles des sous-termes de toutes les contraintes de .
Mise en œuvre en langage . Afin de concevoir un algorithme de décision pour , nous représentons les contraintes d'égalité d'une formule de par une structure de données appelée e-graphe. Cette structure combine un graphe orienté acyclique avec une structure unir et trouver. Les définitions de types C suivantes codent une structure de e-graphe :
struct tnode_s { /* type des noeuds des arbres representant les termes */
char *label; /* symbole racine */
int li; /* position dans tset du premier sous-terme direct ou 0 */
int ri; /* position dans tset du second sous-terme direct ou 0 */
};
typedef struct tnode_s tnode_t;
struct egraph_s { /* type e-graphe representant une formule L4 */
size_t tset_sz; /* longueur de tset */
tnode_t *tset; /* debut tableau des termes de la formule */
int *pre; /* relation sous-terme -- terme */
uf_t *uf; /* unir et trouver pour les classes des termes */
};
typedef struct egraph_s egraph_t;
Dans ce qui suit, on supposera les propriétés suivantes de la mise en œuvre de la structure egraph_t. Si g est une variable de type egraph_t représentant les contraintes d'égalité d'une formule , g.tset code l'ensemble des sous-termes comme suit :
g.tset est un pointeur vers le debut d'un tableau de taille g.tset_sz;
g.tset [0] est initialisée à la valeur {.label=NULL, . , . } (premier champ à NULL et les suivants à 0 ) de tnode_t, valeur qu'on appelle aussi terme vide;
un terme est représenté par une valeur t de type tnode_t tel que t.label est une chaîne de caractères qui décrit le symbole racine du terme, et t.li (resp. t.ri) est la position du premier (resp. second) sous-terme direct dans le tableau g.tset.
Un invariant du tableau g.tset est le suivant :
tout terme de est représenté par une unique position du tableau g.tset.
Cet invariant correspond à une factorisation des termes communs et donc à la transformation de l'ensemble des arbres correspondant aux termes en un graphe orienté acyclique.
Par exemple, considérons la formule utilisant les termes représentés dans la figure 2 . La partie droite de la figure 3 représente le tableau g.tset de l'ensemble des sous-termes de la formule (une valeur tnode_t par ligne) et le terme vide. La partie gauche de la figure 3 représente le tableau g.tset sous la forme d'un graphe orienté acyclique : les noeuds contiennent en partie haute la position du terme dans le tableau g.tset et, pour la lisibilité de la transformation, l'ensemble des identifiants des nœuds correspondants dans les arbres de la figure 2. La partie basse d'un noeud donne le symbole racine.
La composante g.pre de l'e-graphe contient la relation prédécesseur dans le graphe dirigé acyclique représenté par g.tset. Cette relation est donnée sous la forme d'une matrice linéarisée en un tableau de g.tset_sz valeurs dans l'ensemble . Si g.pre[i*g.tset_sz + j] vaut 1 alors le terme g.tset [i] a comme sous-terme direct le terme g.tset [j]. La valeur 0 dénote que g.tset [j] n'est pas sous-terme direct de g.tset [i].
Figure 3 - Codage de sous forme de graphe (à gauche) et de tableau (à droite)
NULL
0
0
"X2"
0
0
"X1"
0
0
"f2"
2
1
"f1"
3
1
"f3"
2
3
La composante de l'e-graphe code les classes d'équivalence définies par les contraintes d'égalités entre les termes. La définition du type uf_t est la même que celle donnée dans la partie III. Chaque terme est représenté dans l'ensemble des éléments de g.uf par la position du noeud racine du terme dans le tableau g.tset. Par conséquent, un autre invariant de la structure d'e-graphe est le suivant :
g.uf->nelem est égal à g.tset_sz.
Question 34. Écrire la fonction bool term_is_diff(egraph_t *g, int tid1, int tid2) qui teste si la contrainte peut être satisfaite simultanément aux contraintes d'égalité représentées par g. Les paramètres tid1 et tid2 sont les positions dans g.tset des noeuds racine représentant respectivement et .
Congruence. Soient et g un e-graphe tel que g. tset représente , l'ensemble des sous-termes de . On définit la relation d'équivalence sur par si et seulement si et sont représentés par des positions de g.tset qui sont dans la même classe d'équivalence de g.uf. On définit la relation sur comme suit :
pour tout et pour tout quadruplet de termes , si et , alors .
Question 35. Écrire la fonction bool term_is_congruent(egraph_t *g, int tid1, int tid2) qui renvoie true si et seulement si les termes représentés aux positions tid1 et tid2 dans g.tset sont dans la relation . Donner et justifier soigneusement la complexité de term_is_congruent en fonction de g.tset_sz, si on suppose que le test d'égalité d'étiquettes (symboles de ou ) se fait en temps constant.
Algorithme de décision. Soient et un e-graphe tel que g représente les termes et les contraintes d'égalité de ainsi que deux termes et , pas nécessairement dans . On cherche à modifier g pour qu'il représente . On appelle cette opération merge( , t1, t2) pour faire la différence avec uf_union. En effet, cette opération ne peut pas se limiter à appeler uf_union pour unir les classes d'équivalence des positions représentant les termes et . Elle doit en plus tester si pour tous termes et qui incluent respectivement et comme sous-termes directs mais ne sont pas déjà dans la même
classe d'équivalence. Si , alors et doivent être mis dans la même classe d'équivalence. Cette dernière relation est propagée aux termes qui contiennent et et ainsi de suite, tant qu'on trouve des couples de termes dans la relation mais pas dans .
Question 36. Écrire une fonction récursive void merge(egraph_t *g, int tid1, int tid2) qui ajoute la contrainte d'égalité entre les termes aux positions tid1 et tid2 dans g.tset, selon le processus décrit ci-dessus. Si tid1 et tid2 sont déjà dans la même classe d'équivalence, merge termine immédiatement.
Question 37. Donner le nombre maximum d'appels récursifs qu'un appel à merge peut engendrer en fonction de g.tset_sz.
Question 38. On suppose que le graphe orienté acyclique représenté par g.tset contient arêtes. Donner la complexité en temps de l'opération merge en fonction de g.tset_sz et .
Fin du sujet.
Annexe : Preuves en déduction naturelle
Un séquent est composé d'un ensemble de formules et d'une formule .
Le sous-ensemble suivant de règles de la déduction naturelle peut être utilisé dans la preuve demandée à la question 14 .
Introduction
Elimination
X ENS Informatique C MPI 2024 - Version Web LaTeX | WikiPrépa | WikiPrépa
