Skip to Main content Skip to Navigation
Reports

Functional Decision Diagrams: A Unifying Data Structure For Binary Decision Diagrams

Joan Thibault 1 Khalil Ghorbal 1
1 HYCOMES - Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Résumé : Zero-suppressed binary Decision Diagram (ZDD) est le variant le plus connu des Reduced Ordered Binary Decision Diagram (ROBDD) permettant d'atteindre une représentation plus compacte en mémoire des fonctions booléennes creuses, i.e., les fonctions valant zéro presque partout. Décider \'a priori quel variant est plus adapté pour représenter une fonction donnée est aussi dur que construire les diagrammes eux-mêmes. De plus, convertir un ZDD en ROBDD (ou vice versa) a usuellement un cout trop élevé. Cette même observation peut être faite pour presque tous les variants de BDD dans la mesure où les règles de réductions pour calculer les diagrammes sont pour l'essentiel incompatibles. En particulier, elles ne peuvent ni commuter ni composer. Dans cet article, nous introduisons une interprétation fonctionnelle des BDD, dénommée Lambda Decision Diagram (LDD), qui a pour ambition de classifier les variants existants comme des implémentations particulières de modèles de LDD tout en suggérant, de manière systématique, de nouveaux modèles exploitants des propriétés spécifiques aux applications souhaitées. De manière à d'avantage réduire la taille des diagrammes, nous montrons comment les règles de réduction capturent, dans une certaine mesure, l'impacte global de chaque variable sur le résultat des fonctions considérées. Cette connaissance suggère un ordre local des variables: ceci différencie fortement notre approche de l'ordre statique global des variants déjà existants ou des techniques de réordonnancement dynamique. Nous appelons ces variants uniformes dans la mesure où les règles de réduction sont appliquées de manière identique à chaque variable et non spécifiquement à la première dans l'ordre choisi.
Document type :
Reports
Complete list of metadatas

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-02369112
Contributor : Joan Thibault <>
Submitted on : Friday, November 29, 2019 - 12:09:41 PM
Last modification on : Friday, July 10, 2020 - 4:01:36 PM

File

RR-9306.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02369112, version 3

Citation

Joan Thibault, Khalil Ghorbal. Functional Decision Diagrams: A Unifying Data Structure For Binary Decision Diagrams. [Research Report] RR-9306, INRIA Rennes - Bretagne Atlantique and University of Rennes 1, France. 2019. ⟨hal-02369112v3⟩

Share

Metrics

Record views

52

Files downloads

285