Efficient Binary Decision Diagram Manipulation in External Memory
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2021
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910066692587520 |
|---|---|
| author | Sølvsten, Steffan Christ van de Pol, Jaco Jakobsen, Anna Blume Thomasen, Mathias Weller Berg |
| author_facet | Sølvsten, Steffan Christ van de Pol, Jaco Jakobsen, Anna Blume Thomasen, Mathias Weller Berg |
| contents | 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 obtain this performance at a fraction of the main memory needed by conventional BDD packages to function. Furthermore, with Adiar we are able to manipulate BDDs that outgrow main memory and so surpass the limits of other BDD packages. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2104_12101 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Efficient Binary Decision Diagram Manipulation in External Memory Sølvsten, Steffan Christ van de Pol, Jaco Jakobsen, Anna Blume Thomasen, Mathias Weller Berg Data Structures and Algorithms 68W30 (primary) 68R05, 68Q60, 68R07 (secondary) E.1; F.2.2; F.2.1; I.1.2 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 obtain this performance at a fraction of the main memory needed by conventional BDD packages to function. Furthermore, with Adiar we are able to manipulate BDDs that outgrow main memory and so surpass the limits of other BDD packages. |
| title | Efficient Binary Decision Diagram Manipulation in External Memory |
| topic | Data Structures and Algorithms 68W30 (primary) 68R05, 68Q60, 68R07 (secondary) E.1; F.2.2; F.2.1; I.1.2 |
| url | https://arxiv.org/abs/2104.12101 |