Multi-variable Quantification of BDDs in External Memory Using Nested Sweeping.

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 each other to compute the result. We have implemented the framework in Adiar and used it to create a new external memory multi-variable quantification algorithm. In practice, this improves Adiar’s running time by a factor of 1.7. In turn, this work extends the previous research results on Adiar to also apply to its quantification operation: compared to conventional depth-first implementations, Adiar with nested sweeping is able to solve more problems and/or solve them faster.