Multi-variable Quantification of BDDs in External Memory using Nested Sweeping (Extended Paper)
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915884389367808 |
|---|---|
| author | Sølvsten, Steffan Christ van de Pol, Jaco |
| author_facet | Sølvsten, Steffan Christ van de Pol, Jaco |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_14216 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Multi-variable Quantification of BDDs in External Memory using Nested Sweeping (Extended Paper) Sølvsten, Steffan Christ van de Pol, Jaco Data Structures and Algorithms Databases 68W30 (primary) 68Q60, 68R07 (secondary) E.1; F.2.2; I.1.2 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. |
| title | Multi-variable Quantification of BDDs in External Memory using Nested Sweeping (Extended Paper) |
| topic | Data Structures and Algorithms Databases 68W30 (primary) 68Q60, 68R07 (secondary) E.1; F.2.2; I.1.2 |
| url | https://arxiv.org/abs/2408.14216 |