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.

翻译：三十年来，二叉决策图作为一种高效表示布尔函数的数据结构，已被广泛应用于模型验证、机器学习、密码学以及组合问题求解等多个领域。其中最著名的变体称为约化有序二叉决策图（简称ROBDD），可视为对完整决策树进行压缩处理的结果。一个有用的性质是：一旦固定布尔变量的顺序，每个布尔函数恰好对应唯一的ROBDD。本文旨在计算$k$个变量的布尔函数根据ROBDD大小的精确分布，其中ROBDD大小等于底层有向无环图（简称DAG）结构中决策节点的数量。回顾可知，$k$个变量的布尔函数总数为$2^{2^k}$，随变量数量呈双指数增长。具有$k$个变量的ROBDD最大规模为$M_k \approx 2^k / k$。除了观察到的自然组合爆炸现象外，根据大小计算分布的另一个难点在于需考虑ROBDD的DAG结构内部的依赖关系。本文提出了首个多项式算法，用于推导$k$个变量布尔函数关于ROBDD大小（记为$n$）的分布。该算法计算了规模不超过$n$的$k$变量ROBDD的（枚举）生成函数。算法需执行$O(k n^4)$次整数算术运算，并存储$O((k+n) n^2)$个位长为$O(n\log n)$的整数。我们的新方法基于逐层分解ROBDD以及容斥原理。