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