Efficient Binary Decision Diagram Manipulation in External Memory

We follow up on the idea of Lars Arge to rephrase the Reduce and Apply algorithms of Binary Decision Diagrams (BDDs) as iterative I/O-efficient algorithms. We identify multiple avenues to improve the performance of his proposed algorithms and extend the technique to other basic BDD algorithms. These algorithms are implemented in a new BDD library, named Adiar. We see very promising results when comparing the performance of Adiar with conventional BDD libraries that use recursive depth-first algorithms. For instances of about 50 GiB, our algorithms, using external memory, are only up to 3.9 times slower compared to Sylvan, exclusively using internal memory. Yet, our proposed techniques are able to obtain this performance at a fraction of the internal memory needed by Sylvan to function. Furthermore, with Adiar we are able to manipulate BDDs that outgrow main memory and so surpass the limits of the other BDD libraries.