Multi-variable Quantification of BDDs in External Memory using Nested Sweeping (Extended Paper)

TL;DR

This paper introduces a nested sweeping framework for external memory BDD algorithms, enabling efficient multi-variable quantification and outperforming traditional methods in handling large BDDs.

Contribution

The paper presents a novel nested sweeping framework for external memory BDD algorithms, extending capabilities to multi-variable quantification and variable reordering.

Findings

More instances solved faster with nested sweeping

Outperforms conventional depth-first implementations

Effective handling of large BDDs in external memory

Abstract

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.