Counting Reduced Ordered Binary Decision Diagrams With Respect to Size
Résumé
The set of binary decision diagrams, an efficient data structure representing Boolean functions, is extensively used in many distinct contexts like model verification, machine learning, cryptography or also resolution of combinatorial problems. The most famous variant, called reduced ordered binary decision diagram (robdd for short), can be viewed as the result of a specific compaction of a complete decision tree. A great property is that, once an order over the Boolean variables is fixed, each Boolean function is represented by exactly one robdd. In this paper we aim at computing the exact distribution of the Boolean functions in k variables according to the robdd size. Recall the number of Boolean functions with k variables is equal to 2 2 k , which is of double exponential growth with respect to the number of variables. The maximal size of an robdd with k variables is M k ≈ 2 k /k. In this paper, we develop the first polynomial algorithm to derive the distribution of Boolean functions over k variables with respect to robdd size denoted by n. It performs O(k n 3 log n) arithmetical operations on integers and necessitates to store O(n 2 ) integers in memory storage. Our new approach relies on a decomposition of robdds layer by layer and on an enumerative inclusion-exclusion argument.
| Origine | Fichiers produits par l'(les) auteur(s) |
|---|---|
| Licence |