  For three decades binary decision diagrams, a data structure efficiently
representing Boolean functions, have been widely used in many distinct contexts
like model verification, machine learning, cryptography and 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 compaction
procedure on the full decision tree. A useful 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}, where the
ROBDD size is equal to the number of decision nodes of the underlying directed
acyclic graph (DAG for short) structure. 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 a ROBDD with $k$
variables is $M_k \approx 2^k / k$. Apart from the natural combinatorial
explosion observed, another difficulty for computing the distribution according
to size is to take into account dependencies within the DAG structure of
ROBDDs. 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$. The algorithm computes the (enumerative) generating function of
ROBDDs with $k$ variables up to size $n$. It performs $O(k n^4)$ arithmetical
operations on integers and necessitates storing $O((k+n) n^2)$ integers with
bit length $O(n\log n)$. Our new approach relies on a decomposition of ROBDDs
layer by layer and on an inclusion-exclusion argument.
