TD 2 : Diagrammes de décision binaire --- BDD

Exercice 1 :

Dans la figure ci-dessous est représenté l'arbre de décision binaire pour la fonction f(x₁, x₂, x₃). Ecrire le BDD correspondant.

Exercice 2 :

Soit f(a,b,c) = c  .  (¬ a  +  ¬ b) et g(a,b,c) = (¬ a)  .  b  .  c.

• Dessinez le BDD pour f(a,b,c) et l'ordre c < a < b. Répétez pour l'ordre b < c < a.
• Expliquez quel est le meilleur ordre pour f(a,b,c).
• Dessinez le DAG à plusieurs racines (multi-rooted DAG) qui représente les deux fonctions f(a,b,c) et g(a,b,c) pour l'ordre c < a < b. Répétez pour l'ordre b < c < a.
• Est-il vrai que le meilleur ordre pour f(a,b,c) est encore le meilleur ordre pour le DAG représentant f(a,b,c) et g(a,b,c) ?

Exercice 3 :

Un automate fini peut être codé en utilisant les BDD. Par exemple, dans la figure ci-dessous, les quatre états sont codés en utilisant deux variables booléennes x₁ et x₂.

• Calculez les fonctions de transition x₁'= f₁(x₁, x₂) et x₂'=f₂(x₁, x₂) pour cet automate. (x₁' et x₂' sont les bits codant l'état cible de la transition.)
• Calculez la relation de transition TR(x₁', x₂', x₁, x₂) et dessinez le BDD la représentant. (Indication : TR(x₁', x₂', x₁, x₂)  .  x₁(¬ x₂) = x₁(¬ x₂)x'₁(¬ x'₂).)
  
  
• Supposons que A est l'état initial de l'automate. Ecrivez la formule qui permet d'obtenir les états successeurs directs de l'état A (donc une formule en x'₁ et x'₂).
  
  
• (En TP :) Ecrivez un petit programme qui calcule la formule ci-dessus en utilisant la bibliothèque de BDD CUDD.

Ce document a été traduit de L^AT_EX par H^EV^EA.