Compiling Binary Decision Diagrams with Interrupt-Based Downsizing

Binary decision diagrams (BDDs) constitute a versatile data structure for Boolean functions, applied in many areas of computer-aided design, formal verification, and fault-tree analysis. Given a suitable variable order, BDDs usually admit a compact representation once constructed. However, while constructing BDDs, their intermediate sizes can by far exceed memory constraints, also known as the peak-size explosion problem. We introduce the generic concept of interrupt-based downsizing where BDD construction can be interrupted by size-reducing transformations. We exemplify our concept on BDD compilations from propositional logic formulas in conjunctive normal form where threshold-triggered interrupts invoke variable reordering, over-approximations, or care-set reductions. Our implementation and evaluation on standard benchmarks shows that interrupt-based downsizing can successfully mitigate the peak-size explosion problem, improve compilation performance, or even enable a BDD compilation.