Efficient Binary Decision Diagram Manipulation in External Memory
Steffan Christ S{\o}lvsten, Jaco van de Pol, Anna Blume Jakobsen, Mathias Weller Berg Thomasen

TL;DR
This paper introduces I/O-efficient algorithms for Binary Decision Diagram (BDD) operations, enabling manipulation of large BDDs beyond main memory with improved performance and reduced memory requirements.
Contribution
It extends and simplifies Arge's algorithms for BDD manipulation, providing asymptotic improvements and implementing them in a new package called Adiar.
Findings
Adiar outperforms traditional BDD packages on large instances
Algorithms are significantly faster when disk I/O is optimized
Allows manipulation of BDDs larger than main memory
Abstract
We follow up on the idea of Lars Arge to rephrase the Reduce and Apply procedures of Binary Decision Diagrams (BDDs) as iterative I/O-efficient algorithms. We identify multiple avenues to simplify and improve the performance of his proposed algorithms. Furthermore, we extend the technique to other common BDD operations, many of which are not derivable using Apply operations alone, and we provide asymptotic improvements for the procedures that can be derived using Apply. These algorithms are implemented in a new BDD package, named Adiar. We see very promising results when comparing the performance of Adiar with conventional BDD packages that use recursive depth-first algorithms. For instances larger than 8.2 GiB, our algorithms, in parts using the disk, are 1.47 to 3.69 times slower compared to CUDD and Sylvan, exclusively using main memory. Yet, our proposed techniques are able to…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Advanced Database Systems and Queries
