We follow up on the idea of Lars Arge to rephrase the Reduce and Apply procedures of Binary Decision Diagrams (BDDs) as iterative I/O-efficient algorithms. We identify multiple avenues to simplify and improve the performance of his proposed algorithms. Furthermore, we extend the technique to other common BDD operations, many of which are not derivable using Apply operations alone, and we provide asymptotic improvements for the procedures that can be derived using Apply. These algorithms are implemented in a new BDD package, named Adiar. We see very promising results when comparing the performance of Adiar with conventional BDD packages that use recursive depth-first algorithms. For instances larger than 8.2 GiB, our algorithms, in parts using the disk, are 1.47 to 3.69 times slower compared to CUDD and Sylvan, exclusively using main memory. Yet, our proposed techniques are able to obtain this performance at a fraction of the main memory needed by conventional BDD packages to function. Furthermore, with Adiar we are able to manipulate BDDs that outgrow main memory and so surpass the limits of other BDD packages.

翻译：我们基于Lars Arge的研究思路，将二进制决策图（BDDs）的Reduce与Apply过程重新表述为迭代式I/O高效算法。我们发现了多种途径来简化并提升其提出算法的性能。此外，我们将该技术扩展到其他常见BDD操作——其中许多无法仅通过Apply操作推导得出，并对可通过Apply推导的过程提供了渐进性改进。这些算法已在一个名为Adiar的新型BDD软件包中实现。通过将Adiar与采用递归深度优先算法的传统BDD软件包进行性能对比，我们获得了极具前景的结果：对于超过8.2 GiB的大型实例，我们部分采用磁盘存储的算法相较于完全使用主内存的CUDD和Sylvan，运行速度仅慢1.47至3.69倍。然而，我们提出的技术能以传统BDD软件包所需主内存的极小比例实现这一性能。更重要的是，Adiar能够操作超出主内存容量的BDD，从而突破了其他BDD软件包的限制。