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的研究思路，将二叉决策图（BDD）的Reduce与Apply过程重构为迭代式I/O高效算法。我们提出了多种途径以简化其算法设计并提升性能。进一步地，我们将该技术扩展至其他常见BDD操作——其中许多无法仅通过Apply运算推导实现，并对可通过Apply推导的流程提供了渐进性改进。这些算法已集成于新型BDD工具包Adiar中。通过与采用递归深度优先算法的传统BDD工具包进行性能对比，我们获得了极具前景的结果：对于超过8.2 GiB的大型实例，我们部分采用磁盘存储的算法相较于完全依赖主存的CUDD与Sylvan工具包，运行速度仅降低1.47至3.69倍。值得注意的是，本研究所提技术仅需传统BDD工具包正常运行所需主存的一小部分即可实现此性能。此外，Adiar能够处理超出主存容量的BDD，从而突破了其他BDD工具包的操作限制。