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 :
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 : Wednesday, December 4, 2019 - 4:15:26 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

36

Files downloads

169