4 papers
Multi-variable Quantification of BDDs in External Memory using Nested Sweeping (Extended Paper)
Steffan Christ Sølvsten, Jaco van de Pol
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…
Efficient Binary Decision Diagram Manipulation in External Memory
Steffan Christ Sølvsten, Jaco van de Pol, Anna Blume Jakobsen +1
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 ave…
Predicting Memory Demands of BDD Operations using Maximum Graph Cuts (Extended Paper)
Steffan Christ Sølvsten, Jaco van de Pol
The BDD package Adiar manipulates Binary Decision Diagrams (BDDs) in external memory. This enables handling big BDDs, but the performance suffers when dealing with moderate-sized B…
Symbolic Model Checking in External Memory
Steffan Christ Sølvsten, Jaco van de Pol
We extend the external memory BDD package Adiar with support for monotone variable substitution. Doing so, it now supports the relational product operation at the heart of symbolic…