Ordered Functional Decision Diagrams - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2020

Ordered Functional Decision Diagrams

Diagramme de Décision Fonctionnel Ordonné

(1) , (1)
1

Abstract

Several BDD variants were designed to exploit special features of Boolean functions to achieve better compression rates. Deciding a priori which variant to use is as hard as constructing the diagrams themselves and the conversion between variants comes in general with a prohibitive cost. This observation leads naturally to a growing interest into when and how one can combine existing variants to benefit from their respective sweet spots. In this paper, we introduce a novel framework, termed λDD (LDD), that revisits BDD from a purely functional point of view. The framework allows to classify the already existing variants, including the most recent ones like ChainDD and ESRBDD, as implementations of a special class of ordered models. We enumerate, in a principled way, all the models of this class and isolate its most expressive model. This new model, termed λDD-O-NUCX, is suitable for both dense and sparse Boolean functions, and, unlike ChainDD and ESRBDD, is invariant by negation. The canonicity of λDD-O-NUCX is formally verified using the Coq proof assistant. We furthermore provide experimental evidence corroborating our theoretical findings: more expressive λDD models achieve, indeed, better memory compression rates.
Les Diagrammes de Décision Binaires (BDD) sont une structure qui a été décliné en de nombreux variants, chacun conçu pour exploiter au mieux une propriété particulière des fonctions Booléennes et ainsi réduire leur taille mémoire. Cependant, décider quel variant est le plus adapté à priori est aussi difficile que construire chaque représentation. De plus la conversion entre les variants coûte également trop chère pour être utilisable en pratique. Ces observations ont conduit naturellement à un intérêt grandissant pour combiner des variants pour tirer parti de leurs avantages respectifs. Cet article introduit un cadre théorique à cette problématique en introduisant une méta-structure nommée \lambdaDD qui adopte un point de vue purement fonctionnel sur les BDD. Les diagrammes λDD permettent d'abstraire les variants classiques (par exemple ROBDD et ZDD) ainsi que des variants récents (en particulier ChainDD et ESRBDD) comme des modèles d'une classe de modèles ordonnés que nous appelons λDD-O Dans ces modèles ordonnés, les variables sont évaluées en suivant un ordre global strict. Nous énumérons les éléments de cette classe et isolons son modèle le plus expressif que nous nommons λDD-O-NUCX. Ce modèle permet non seulement de capturer les variables canalisantes (ce qui le rend plus expressif que ESRBDD par exemple) mais exploite aussi une propriété supplémentaire: les xor-variables. Le modèle est également invariant par négation, ce qui permet de calculer la négation d'une fonction Booléenne en temps constant. La canonicité de λDD-O-NUCX est formellement vérifiée en utilisant l'assistant de preuve Coq. De plus, nous fournissons des résultats expérimentaux confirmant l'intérêt de λDD-O-NUCX.
Fichier principal
Vignette du fichier
RR-9333.pdf (358.46 Ko) Télécharger le fichier

Dates and versions

hal-02512117 , version 1 (19-03-2020)

Licence

Copyright

Identifiers

Cite

Joan Thibault, Khalil Ghorbal. Ordered Functional Decision Diagrams: A Functional Semantic For Binary Decision Diagrams. [Research Report] RR-9333, Inria. 2020. ⟨hal-02512117⟩
150 View
244 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More