Multi-variable Quantification of BDDs in External Memory using Nested Sweeping
summary
Implements nested sweeping inside Adiar to do multi-variable BDD quantification in external memory, replacing recursion with coordinated concurrent sweeps and IO‑efficient priority queues. Claims a practical 1.7× speedup over prior Adiar quantification, processes BDDs up to 700–900 GB on a 300 GB machine using SSDs, and outperforms disk-based CAL by orders of magnitude while matching in‑RAM packages on small cases and avoiding RAM blowups on large instances.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:23Binary Decision Diagrams background
- 4:55IO efficiency in BDDs
- 11:25Arger tool implementation
- 13:10Single-variable quantification limits
- 18:05Nested sweeping for multi-variable
- 19:51Benchmarking method
- 20:35Performance gains with nested sweeping
- 21:59Cal BDD comparison
- 23:24Depth-first BDD comparison
- 26:13Applications beyond quantification
- 27:17Q&A
related talks
21mWeighted Context-Free-Language Ordered Binary Decision Diagrams
14mDependency-Aware Compilation for Surface Code Quantum Architectures
15mPolynomial Bounds of CFLOBDDs against BDDs
19mPanel: Compilation Frameworks
19mDecoupling Data Layouts from Bounding Volume Hierarchies
01h 05mThe Power of Extended Resolution: A Practitioner's Perspective
32mBit-Stealing Made Legal: Compilation for Custom Memory Representations of Algebr...
21mNavigating the Frontier of EDDO-Based Accelerators: Programming and Code(…)