| 1 | {{{ |
| 2 | #!html |
| 3 | <h1>TME 6 : Représentation des fonctions Boolèennes : ROBDD</h1> |
| 4 | }}} |
| 5 | [[PageOutline]] |
| 6 | |
| 7 | = Objectif = |
| 8 | |
| 9 | L'objectif principal de ce TME est de vous familiariser avec la représentation des |
| 10 | fonctions Booléennes sous forme de ROBDD. Les ROBDD (Reduced Ordered Binary Decision |
| 11 | Diagram) sont utilisés pour représenter de façon compacte une ou plusieurs fonctions |
| 12 | Booléennes, partageant le même support (c’est à dire dépendant d’un même ensemble de |
| 13 | variables Booléennes). Pour un ordre donné des variables constituant le support, cette |
| 14 | représentation est canonique : a chaque fonction Booléenne est associé un unique graphe |
| 15 | orienté acyclique (DAG). Le graphe étant acyclique, chaque noeud BDD définit un |
| 16 | sous-graphe dont il est la racine. Par conséquent, chaque noeud BDD correspond à une |
| 17 | fonction Booléenne particulière. On utilise le fait que les variables Booléennes |
| 18 | constituant le support sont ordonnées pour identifier ces variables par leur index. |
| 19 | |
| 20 | Des squelettes de démarrage vous sont fournis pour un certain nombre de fichiers, ainsi |
| 21 | qu'une librairie {{{ebm}}} ({{{libebm.a}}} précompilée. |
| 22 | |
| 23 | [[Image(BDD-1.png)]] |
| 24 | |
| 25 | |
| 26 | = A) Structures de données et fonctions de base = |
| 27 | |
| 28 | La structure C++ permettant de représenter un noeud du graphe ROBDD est définie de la |
| 29 | façon suivante : |
| 30 | |
| 31 | {{{ |
| 32 | #!cpp |
| 33 | class Bdd { |
| 34 | public: |
| 35 | class Key { |
| 36 | private: |
| 37 | unsigned int _index; |
| 38 | unsigned int _highIdent; |
| 39 | unsigned int _lowIdent; |
| 40 | public: |
| 41 | inline Key ( unsigned int index, unsigned int high, unsigned int low ); |
| 42 | friend bool operator< ( const Key& lhs, const Key& rhs ); |
| 43 | }; |
| 44 | private: |
| 45 | static unsigned int _maxIdent; |
| 46 | static unsigned int _maxStamp; |
| 47 | static std::map<Key,Bdd*> _bdds; |
| 48 | private: |
| 49 | unsigned int _ident; // Unicity identifier. |
| 50 | unsigned int _index; // Decomposition variable index. |
| 51 | Bdd* _high; // Low cofactor pointer. |
| 52 | Bdd* _low; // High cofactor pointer. |
| 53 | unsigned _stamp; // Used to flag already reached nodes in the DAG |
| 54 | // recursive walktrhough. |
| 55 | public: |
| 56 | static Bdd* ConstHigh; |
| 57 | static Bdd* ConstLow; |
| 58 | private: |
| 59 | Bdd ( unsigned index, Bdd* high, Bdd* low ); |
| 60 | ~Bdd (); |
| 61 | public : |
| 62 | static Bdd* create ( unsigned index, Bdd* high, Bdd* low ); |
| 63 | static Bdd* apply ( OperatorType, Bdd*, Bdd* ); |
| 64 | static Bdd* Not ( Bdd* ); |
| 65 | static Bdd* And ( Bdd*, Bdd* ); |
| 66 | static Bdd* And ( Bdd*, Bdd*, Bdd* ); |
| 67 | static Bdd* And ( Bdd*, Bdd*, Bdd*, Bdd* ); |
| 68 | static Bdd* Xor ( Bdd*, Bdd* ); |
| 69 | static Bdd* Xor ( Bdd*, Bdd*, Bdd* ); |
| 70 | static Bdd* Xor ( Bdd*, Bdd*, Bdd*, Bdd* ); |
| 71 | static Bdd* Or ( Bdd*, Bdd* ); |
| 72 | static Bdd* Or ( Bdd*, Bdd*, Bdd* ); |
| 73 | static Bdd* Or ( Bdd*, Bdd*, Bdd*, Bdd* ); |
| 74 | public: |
| 75 | inline unsigned getIdent (); |
| 76 | inline unsigned getIndex (); |
| 77 | inline Bdd* getHigh (); |
| 78 | inline Bdd* getLow (); |
| 79 | Bdd* neg (); |
| 80 | unsigned int depth (); |
| 81 | Bdd* satisfy (); |
| 82 | void display ( std::ostream& ); |
| 83 | ValueType eval (); |
| 84 | Ebm* toEbm (); |
| 85 | static Bdd* fromEbm ( Ebm* ); |
| 86 | private: |
| 87 | inline Key _getKey (); |
| 88 | void _display ( std::ostream& ); |
| 89 | friend std::ostream& operator<< ( std::ostream&, const Bdd* ); |
| 90 | }; |
| 91 | }}} |
| 92 | |
| 93 | * Le constructeur {{{Bdd::Bdd()}}}, alloue un nouveau noeud BDD et l'ajoute dans le |
| 94 | dictionnaire des noeuds BDD. |
| 95 | |
| 96 | * La méthode '''Bdd::create()''' gère un dictionnaire de tous les noeuds BDD déjà créés |
| 97 | et fournit la garantie qu’il n’existera jamais deux noeuds BDD possédant les mêmes |
| 98 | valeurs pour les attributs {{{_index}}}, {{{_high}}} et {{{_low}}}. La méthode |
| 99 | Bdd::create() recherche le noeud BDD possédant les valeurs définies par les arguments, |
| 100 | et renvoie un pointeur sur le noeud BDD correspondant. Si ce noeud n’existe pas, elle |
| 101 | le crée en appelant le constructeur de BDD. |
| 102 | |
| 103 | * La méthode '''Bdd::apply()''' prend pour arguments un entier définissant un opérateur |
| 104 | Booléen (les valeurs possibles sont OR, AND, et XOR), deux pointeurs {{{bdd1}}} et |
| 105 | {{{bdd2}}} sur deux noeuds BDD représentant deux fonctions Booléennes F1 et F2 (notons |
| 106 | que les deux fonctions F1 et F2 ne dépendent pas forcément de toutes les variables |
| 107 | Booléennes définies dans le support global). La méthode {{{Bdd::apply()}}} construit le |
| 108 | graphe ROBDD représentant la fonction {{{F = F1 oper F2}}}, et renvoie un pointeur sur |
| 109 | le noeud ROBDD racine de ce graphe. |
| 110 | |
| 111 | * La méthode '''Bdd::neg()''' renvoie un pointeur sur un noeud BDD représentant la |
| 112 | négation du noeud courant {{{NOT(bdd)}}}. |
| 113 | |
| 114 | * La fonction '''Bdd::display()''' affichera sur la sortie standard le graphe de noeuds |
| 115 | BDD ayant le noeud courant pour racine. L'affichage sera récursif et indenté: |
| 116 | {{{ |
| 117 | Bdd( [10] idx:4 high:8 low:7 ) - x1 |
| 118 | High of [10] x1 |
| 119 | [...] |
| 120 | Low of [10] x1 |
| 121 | [...] |
| 122 | }}} |
| 123 | Ou {{{[X]}}}, {{{high:Y}}} et {{{low:Z}}} sont respectivement les identificateurs du |
| 124 | neud courant (X), du BDD high cofacteur (Y) et du BDD low cofacteur (Z). {{{idx:I}}} |
| 125 | est l'index de la variable suivant laquelle on décompose et {{{x1}}} son nom. Un |
| 126 | exemple complet donnera: |
| 127 | {{{ |
| 128 | Bdd( [10] idx:4 high:8 low:7 ) - x1 |
| 129 | High of [10] x1 |
| 130 | Bdd( [8] idx:3 high:1 low:2 ) - x2 |
| 131 | High of [8] x2 |
| 132 | Bdd( One ) |
| 133 | Low of [8] x2 |
| 134 | Bdd( [2] idx:2 high:1 low:0 ) - x3 |
| 135 | High of [2] x3 |
| 136 | Bdd( One ) |
| 137 | Low of [2] x3 |
| 138 | Bdd( Zero ) |
| 139 | Low of [10] x1 |
| 140 | Bdd( [7] idx:3 high:2 low:0 ) - x2 |
| 141 | High of [7] x2 |
| 142 | Bdd( [2] idx:2 high:1 low:0 ), already displayed. |
| 143 | Low of [7] x2 |
| 144 | Bdd( Zero ) |
| 145 | |
| 146 | }}} |
| 147 | |
| 148 | Pour la modélisation des variables, vous réutiliserez l'objet {{{EbmVar}}} vu au TME |
| 149 | précédent. Pour ne pas bloquer sur des erreurs que contiendrais éventuellement votre |
| 150 | implantation, des ''headers'' {{{Ebm.h}}}, {{{EbmVar.h}}}, {{{EbmExpr.h}}} ainsi qu'une |
| 151 | librairie compilée {{{libebm.a}}} vous sont fournis |
| 152 | |
| 153 | |
| 154 | = B) Techniques de Programmation = |
| 155 | |
| 156 | == B.1) Constructeur pré-conditionné == |
| 157 | |
| 158 | Avant de créer un nouveau BDD, il est nécessaire de vérifier s'il n'existe pas déja. Cela |
| 159 | ne peut pas être fait ''dans'' le constructeur puisque si nous sommes dans cette fonction, |
| 160 | c'est que l'objet est ''déjà'' en cours de construction. |
| 161 | |
| 162 | Pour résoudre ce problème on adopte l'architecture suivante: |
| 163 | |
| 164 | * Le constructeur est rendu ''privé''. Ce qui inderdit son utilisation, sauf par des |
| 165 | fonctions membre de la classe. |
| 166 | |
| 167 | * On ajoute une fonction membre statique {{{Bdd::create()}}} qui va jouer le rôle du |
| 168 | constructeur. Comme elle est membre de la classe, elle a le droit d'appeler le |
| 169 | constructeur. Et comme elle est {{{static}}} elle n'est pas attachée à un objet de la |
| 170 | classe. Dans cette fonction on peut donc effectuer les vérifications (est-ce que le BDD |
| 171 | existe déjà?) puis créer ou non un nouvel objet. |
| 172 | |
| 173 | |
| 174 | == B.2) Dictionnaire de BDD == |
| 175 | |
| 176 | |
| 177 | Comme il a été montré en cours, une expression booléenne sous la forme canonique de |
| 178 | Shannon est associée à un et un seul ROBDD. Celui-çi étant entièrement caractérisé par son |
| 179 | triplet {{{(_index,_high,_low)}}}. Lorsque la méthode {{{Bdd::create()}}} est appelée il |
| 180 | faut qu'elle puisse déterminer rapidement si un ROBDD existe ou non. |
| 181 | |
| 182 | Le conteneur approprié pour ce type d'opération est la {{{stl::map<>}}}. La {{{map<>}}} |
| 183 | associe une valeur (le pointeur sur le ROBDD) à une clé (le triplet). Elle à les |
| 184 | propriétés suivantes: |
| 185 | |
| 186 | * Une clé d'une valeur donnée sera présente en un unique exemplaire dans la {{{map<>}}}, |
| 187 | et sera associée à une unique valeur. |
| 188 | |
| 189 | * On peut retrouver très rapidement une valeur en fonction d'une clé. |
| 190 | |
| 191 | * N'importe quel objet (classe) peut servir de clé ''sous réserve'' de disposer d'une |
| 192 | fonction d'ordre. C'est à dire de disposer d'une surcharge de l'operateur |
| 193 | ''strictement inférieur''. |
| 194 | |
| 195 | La définition de la classe {{{Bdd}}} comporte donc une classe imbriquée {{{Key}}} |
| 196 | représentant le triplet et proposant une fonction d'ordre. La relation d'ordre sera |
| 197 | simplement l'ordre lexicographique du triplet. Soit: |
| 198 | |
| 199 | {{{ |
| 200 | #!cpp |
| 201 | if ( lhs->_index != rhs->_index ) return lhs->_index < rhs->_index; |
| 202 | |
| 203 | if ( lhs->_highIndex != rhs->_highIndex ) |
| 204 | return lhs->_highIndex < rhs->_highIndex; |
| 205 | |
| 206 | return lhs->_lowIndex < rhs->_lowIndex; |
| 207 | }}} |
| 208 | |
| 209 | |
| 210 | = C) Représentation Graphique = |
| 211 | |
| 212 | Soit la fonction Booléenne F(a,b,c,d,e), définie par l’expression suivante |
| 213 | |
| 214 | E0 = (a’ . (b + c + d’) . e) + c |
| 215 | |
| 216 | La notation a’ signifie NOT(a). |
| 217 | |
| 218 | E0 peut se re-écrire sous forme préfixée de la façon suivante : |
| 219 | |
| 220 | E0 = OR( AND (NOT (a) OR (b c NOT (d) e)) c) |
| 221 | |
| 222 | '''C.1''' En utilisant la décomposition de Shannon, représentez graphiquement le graphe |
| 223 | ROBDD associé à la fonction F(a,b,c,d,e) pour l’ordre a > b > c > d > e , puis pour |
| 224 | l’ordre e > d > c > b > a. |
| 225 | |
| 226 | '''C.2''' Précisez, pour chaque noeud du ROBDD ainsi construit, quelle est la fonction |
| 227 | Booléenne représentée par ce noeud. |
| 228 | |
| 229 | |
| 230 | = D) Méthodes Bdd::neg() et Bdd::apply() = |
| 231 | |
| 232 | Les méthodes {{{Bdd::apply()}}} et {{{bdd::neg()}}} ont été présentées en cours. Vous |
| 233 | trouverez le code de ces fonctions dans le fichier {{{Bdd.cpp}}}. |
| 234 | |
| 235 | '''D.1''' Soient F1 et F2 deux fonctions Booléennes, et les fonctions F1H, F1L, F2H, F2L |
| 236 | définies par la décomposition de Shannon suivant la variable x : |
| 237 | |
| 238 | * F1 = x . F1H + x’ . F1L |
| 239 | * F2 = x . F2H + x’ . F2L |
| 240 | |
| 241 | La relation de recurrence (F1 op F2) = x . (F1H op F2H) + x’. (F1L op F2L) a été démontrée |
| 242 | en cours dans le cas des opérateurs OR et AND. Démontrez que cette relation est vraie dans |
| 243 | le cas d’un opérateur XOR. Analysez le cas général, ainsi que les cas particuliers où |
| 244 | l’une des deux fonctions F1 ou F2 est égale à une des deux fonctions constantes 0 ou 1. |
| 245 | |
| 246 | '''D.2''' Soit la fonction F, définie par l’expression E1 = a . (b + c) Représentez |
| 247 | graphiquement le ROBDD représentant la fonction F, pour l’ordre des variables a > b > |
| 248 | c. On appelle p0, p1, p2, p3, p4 les pointeurs sur les 5 noeuds BDD contenus dans ce |
| 249 | graphe : |
| 250 | |
| 251 | * p0 représente la fonction F0 = 0 |
| 252 | * p1 représente la fonction F1 = 1 |
| 253 | * p2 représente la fonction F2 = c |
| 254 | * p3 représente la fonction F3 = b + c |
| 255 | * p4 représente la fonction F4 = a . (b + c) |
| 256 | |
| 257 | Représentez graphiquement l’arbre d’appels des fonctions lorsqu’on appelle la méthode |
| 258 | bdd::neg() sur l'objet pointé par p4. Quel est le nombre maximum d’appels de fonctions |
| 259 | empilés sur la pile d’exécution? Combien de noeuds BDD vont être créés par la fonction |
| 260 | create_bdd(), si on suppose que la structure de données ne contient initialement que les 5 |
| 261 | noeuds pointés par p0, p1, p2, p3, et p4 au moment de l’appel de la méthode bdd::neg()? |
| 262 | |
| 263 | |
| 264 | = E) Méthode Bdd::fromEbm() = |
| 265 | |
| 266 | On cherche à écrire la méthode {{{Bdd::fromEbm()}}}, qui construit automatiquement le |
| 267 | graphe ROBDD représentant une fonction Booléenne F, à partir d'une Expression Booléenne |
| 268 | multiniveaux particulière de cette fonction F. Cette méthode prend comme unique argument |
| 269 | un pointeur sur la racine d’une {{{Ebm}}}, et renvoie un pointeur sur le noeud BDD |
| 270 | représentant la fonction. Puisque {{{Ebm}}} ne contiennent que des opérateurs OR, AND, |
| 271 | XOR et NOT, et qu’on dispose des fonctions {{{Bdd::apply()}}} et {{{bdd::neg()}}, il est |
| 272 | possible de construire le graphe ROBDD en utilisant uniquement ces deux fonctions. |
| 273 | |
| 274 | '''E.1''' Décrire en français, l’algorithme de cette méthode {{{Bdd::fromEbm()}}} dans le |
| 275 | cas particulier où tous les opérandes AND, OR ou XOR présents dans l’arbre ABL n’ont que |
| 276 | deux opérandes. On traite successivement les trois cas suivants: |
| 277 | |
| 278 | * Le pointeur p désigne une variable. |
| 279 | |
| 280 | * Le pointeur p désigne une expression Booléenne multi-niveaux, dont l'opérateur racine |
| 281 | est l'opérateur NOT. |
| 282 | |
| 283 | * Le pointeur p désigne une expression Booléenne multi-niveaux, dont l'opérateur racine |
| 284 | est l'un des trois opérateurs OR, AND ou XOR. |
| 285 | |
| 286 | '''E.2''' Ecrire en langage C++ la méthode {{{Bdd::fromEbm()}}} dans le cas particulier de |
| 287 | la question précédente. Pour valider cette fonction, on écrira un programme main(), qui |
| 288 | effectue successivement les opérations suivantes : |
| 289 | |
| 290 | * Construction de l'{{{Ebm}}} représentant l’expression E1, avec la fonction |
| 291 | {{{Ebm::parse()}}}. |
| 292 | |
| 293 | * Affichage de cette expression Booléenne, avec la fonction {{{Ebm::display()}}}, pour |
| 294 | vérifier que l’{{{Ebm}}} est correctement construite. |
| 295 | |
| 296 | * Construction du graphe ROBDD représentant la fonction F, avec la fonction |
| 297 | Bdd::fromEbm(). |
| 298 | |
| 299 | * Affichage du graphe ROBDD ainsi construit, en utilisant la fonction Bdd::display(). |
| 300 | |
| 301 | '''E.3''' Comment faut-il modifier la fonction {{{Bdd::fromEbm()}}}, pour traiter le cas |
| 302 | général, où les opérateurs OR, AND et XOR peuvent avoir une arité quelconque? Modifier le |
| 303 | code de la fonction, et validez ces modifications sur l’exemple de l’expression Booléenne |
| 304 | E0, ou sur des expressions encore plus complexes. |
| 305 | |
| 306 | |
| 307 | = F) Méthode Bdd::satisfy() = |
| 308 | |
| 309 | Soit une fonction Booléenne quelconque F(x1, x2, x3, ... xn), dépendant de n |
| 310 | variables. Soit la fonction Booléenne G, définie comme un produit (opérateur AND) d’un |
| 311 | nombre queconque de variables xi (directes ou complémentées). On dit que G “satisfait” F |
| 312 | si on a la relation G => F. (Autrement dit, si G = 1, alors F = 1). Remarquez que la |
| 313 | condition G = 1 impose la valeur de toutes les variables appartenant au support de G (les |
| 314 | variables directes doivent prendre la valeur 1, et les variables complémentées doivent |
| 315 | prendre la valeur 0). Notez que, pour une fonction F donnée, il existe plusieurs fonction |
| 316 | G qui satisfont F... |
| 317 | |
| 318 | Exemple : F = (a . b) + c |
| 319 | |
| 320 | On peut avoir {{{G = c}}} ou {{{G = a . b}}} ou encore {{{G = a . b . c’}}}. |
| 321 | |
| 322 | Dans la suite de cet exercice, on cherche à construire automatiquement le ROBDD |
| 323 | représentant une fonction G satisfaisant une fronction F quelconque. Comme il existe |
| 324 | plusieurs solutions, on choisira la systématiquement la solution qui minimise le nombre de |
| 325 | variable {{{xi}}} dans le support de G. La méthode Bdd::satisfy() appliqué au noeud |
| 326 | représentant F retourne un pointeur sur le noeud représentant G. |
| 327 | |
| 328 | '''F.1''' La décomposition de Shannon de la fonction F suivant la variable x d’index le |
| 329 | plus élévé définit les cofacteurs FH et FL : F = x . FH + x’ . FL Pour alléger les |
| 330 | notations, on note sat(F) la fonction Booléenne construite par la méthode |
| 331 | {{{Bdd::satisfy()}}} pour la fonction F. Donner la relation de récurrence entre les |
| 332 | fonctions sat(F), sat (FH), et sat(FL). On étudiera successivement le cas général où ni |
| 333 | FH et FL ne sont constantes, et les quatre cas particuliers où l’une des deux fonctions FH |
| 334 | ou FL sont égales à 0 ou 1. |
| 335 | |
| 336 | '''F.2''' Ecrire, en langage C++, le code de la méthode {{{Bdd::satisfy()}}}, et |
| 337 | appliquez-la sur la fonction Booléenne F définie dans la partie, en modifiant le programme |
| 338 | main de la fonction précédente. |
| 339 | |
| 340 | |
| 341 | = G) Méthode Bdd::toEbm() = |
| 342 | |
| 343 | On souhaite pour finir écrire la méthode Bdd::toEbm(), qui construit automatiquement une |
| 344 | expression Booléenne multi-niveaux, à partir d'un ROBDD représentant une fonction |
| 345 | Booléenne. |
| 346 | |
| 347 | Il existe évidemment un grand nombre d’expressions Booléennes équivalentes pour une même |
| 348 | fonction Booléenne. Dans un premier temps, nous nous contenterons d’utiliser des |
| 349 | opérateurs OR, et AND à deux opérandes, ainsi que l’opérateur NOT. Soit un noeud BDD |
| 350 | représentant une fonction Booléenne F. Soient x la variable associée à ce noeud BDD, FH et |
| 351 | FL les fonctions Booléennes associées aux noeuds BDD pointés par les pointeurs HIGH et LOW |
| 352 | (cofacteurs de Shannon). |
| 353 | |
| 354 | '''G.1''' Quelle expression Booléenne dépendant de x, FH et FL peut-on associer à la |
| 355 | fonction F dans le cas général ou FH et FL sont quelconques ? (aucune des deux fonctions |
| 356 | FH ou FL n’est égale à 0 ou à 1) |
| 357 | |
| 358 | '''G.2''' Comment cette expression Booléenne se simplifie-t-elle lorsque l’une des deux |
| 359 | fonctions FH ou FL est égale à 0 ou à 1. Etudier un par un les 4 cas particuliers. |
| 360 | |
| 361 | '''G.3''' En utilisant les résultats des questions précédentes, proposez un algorithme. |