Counting Reduced Ordered Binary Decision Diagrams With Respect to Size

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}\approx 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)\) arithmetic operations on integers and necessitates to store \(O(n^{2})\) integers in memory storage; note that the maximal size of integers involved in the computations is \(O(k\;2^{k})\) bits. Our new approach relies on a decomposition of robdd s layer by layer and on an enumerative inclusion-exclusion argument.