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能够解决更多基准测试实例，且/或解决速度更快。