论文标题
一种迭代方法，用于计数减少有序的二进制决策图
An iterative approach for counting reduced ordered binary decision diagrams
论文作者
论文摘要
在三十年中，二进制决策图（有效地代表布尔功能的数据结构）已在许多不同的上下文中广泛使用，例如模型验证，机器学习，加密以及组合问题的解决。最著名的变体，称为减少有序的二进制决策图（简称ROBDD），可以看作是完整决策树上压实过程的结果。一个有用的属性是，一旦固定了布尔变量上的订单，每个布尔函数就会完全由一个robdd表示。在本文中，我们旨在根据ROBDD尺寸计算$ k $变量中布尔函数的确切分布}，其中ROBDD大小等于基础定向的无循环图（短）结构的DAG的决策节点数量。回想一下带有$ K $变量的布尔函数的数量等于$ 2^{2^k} $，相对于变量的数量，这是双重指数增长的。 $ k $变量的Robdd的最大尺寸为$ m_k \ of 2^k / k $。除了观察到的自然组合爆炸外，根据大小计算分布的另一个困难是考虑ROBDDS的DAG结构内的依赖性。在本文中，我们开发了第一种多项式算法，以根据$ n $表示的ROBDD大小来得出$ k $变量以上的布尔函数的分布。该算法计算$ k $变量的ROBDD的（枚举）生成功能，最高为$ n $。它在整数上执行$ o（k n^4）$算术操作，因此需要存储$ o（（（k+n）n^2）$ benge $ o（n \ log n）$的整数。我们的新方法依赖于按一层和包含 - 排斥参数的RobDDS分解。
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.
