.png){kind=icon}
.png){kind=icon}
Return
Counting Reduced Ordered Binary Decision Diagrams with Respect to Size
.png){kind=icon}
PRE
AI
DOI：10.1145/3799237.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
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, and resolution of combinatorial problems. The most famous variant, called reduced ordered binary decision diagram (ROBDD), 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 article, we aim at computing the exact distribution of the Boolean functions ink variables according to the ROBDD size. Recall the number of Boolean functions with k variables is equal to 22k, which is of double exponential growth with respect to the number of variables. The maximal size of an ROBDD with k variables is Mk approximate to 2k/k. In this article, 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 n3 log n) arithmetic operations on integers and necessitates to store O(n2) integers in memory storage; note that the maximal size of integers involved in the computations is O(k 2k) bits. Our new approach relies on a decomposition of ROBDDs layer by layer and on an enumerative inclusion-exclusion argument.
Keywords:
Boolean Function
Reduced Ordered Binary Decision Diagram (ROBDD)
Enumerative Combinatorics
Directed Acyclic Graph
Journal
A
IF:
0
Papers:
18
Citations:
0