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