Julien Clément (GREYC, Caen )

Les diagrammes de décision binaires sont une famille de structures de données permettant de représenter efficacement une fonction booléenne. Ils ont été notamment popularisés par Randal Bryant en 1986 et ont suscité de nombreuses applications.

Nous aborderons dans cet exposé quelques questions de comptage sur ces structures en nous concentrant sur la variante la plus connue, dite réduite et ordonnée (Reduced ordered decision diagram ou ROBDD). Le principal résultat est de fournir un algorithme polynomial pour calculer le nombre de ROBDD à \(k\) variables de taille \(n\) (la taille étant le nombre de nœuds de décision de la structure). Après moult efforts, nous avons pu appliquer la méthode pour \(k=16\) variables (il faut savoir rester modeste). La gageure est de faire cela sans examiner naïvement une par une les \(2^{2^{16}}= 2^{65536}\) fonctions booléennes pour vérifier leur taille en tant que diagramme de décision binaire. (Pour mémoire le nombre d’atomes dans l’univers est estimé être de l’ordre de \(2^{266}\).)

Comme application de ces résultats, nous proposons la première méthode polynomiale de génération aléatoire uniforme (pour la taille) des ROBDD.