Previous research on the Adiar BDD package has been successful at designing algorithms capable of handling large Binary Decision Diagrams (BDDs) stored in external memory. To do so, it uses consecutive sweeps through the BDDs to resolve computations. Yet, this approach has kept algorithms for multi-variable quantification, the relational product, and variable reordering out of its scope. In this work, we address this by introducing the nested sweeping framework. Here, multiple concurrent sweeps pass information between eachother to compute the result. We have implemented the framework in Adiar and used it to create a new external memory multi-variable quantification algorithm. Compared to conventional depth-first implementations, Adiar with nested sweeping is able to solve more instances of our benchmarks and/or solve them faster.

翻译：先前对Adiar BDD软件包的研究已成功设计出能够处理存储在外部存储器中的大型二元决策图（BDD）的算法。为此，该软件包采用连续扫描BDD的方式来完成计算。然而，这种方法始终将多变量量化、关系积和变量重排序等算法排除在其适用范围之外。在本工作中，我们通过引入嵌套扫描框架来解决这一问题。该框架中，多个并发扫描相互传递信息以计算结果。我们已在Adiar中实现了该框架，并用于创建一种新的外部存储多变量量化算法。与传统的深度优先实现相比，采用嵌套扫描的Adiar能够解决更多基准测试实例，且/或求解速度更快。