Skip to Main content Skip to Navigation

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
Abstract : Zero-suppressed binary Decision Diagram (ZDD) is a notable alternative data structure of Reduced Ordered Binary Decision Diagram (ROBDD) that achieves a better size compression rate for Boolean functions that evaluate to zero almost everywhere. Deciding \textit{a priori} which variant is more suitable to represent a given Boolean function is as hard as constructing the diagrams themselves. Moreover, converting a ZDD to a ROBDD (or vice versa) often has a prohibitive cost. This observation could be in fact stated about almost all existing BDD variants as it essentially stems from the non-compatibility of the reduction rules used to build such diagrams. Indeed, they are neither interchangeable nor composable. In this work, we investigate a novel functional framework, termed Lambda Decision Diagram (LDD), that ambitions to classify the already existing variants as implementations of special LDD models while suggesting, in a principled way, new models that exploit application-dependant properties to further reduce the diagram's size. We show how the reduction rules we use locally capture the global impact of each variable on the output of the entire function. Such knowledge suggests a variable ordering that sharply contrasts with the static fixed global ordering in the already existing variants as well as the dynamic reordering techniques commonly used.
Document type :
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Joan Thibault Connect in order to contact the contributor
Submitted on : Friday, November 29, 2019 - 12:09:41 PM
Last modification on : Wednesday, November 3, 2021 - 8:17:57 AM


Files produced by the author(s)


  • HAL Id : hal-02369112, version 3


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⟩



Les métriques sont temporairement indisponibles