Compressing Binary Decision Diagrams
Esben Rune Hansen, S. Srinivasa Rao, Peter Tiedemann

TL;DR
The paper presents a new linear-time compression technique for Binary Decision Diagrams that significantly reduces their size when random access isn't needed, outperforming previous methods.
Contribution
A novel compression method for BDDs that achieves near-optimal size reduction with linear time complexity, surpassing existing techniques.
Findings
Compression reduces BDD size to 1-2 bits per node
Technique dominates previous methods on tested instances
Compression and decompression are linear in BDD size
Abstract
The paper introduces a new technique for compressing Binary Decision Diagrams in those cases where random access is not required. Using this technique, compression and decompression can be done in linear time in the size of the BDD and compression will in many cases reduce the size of the BDD to 1-2 bits per node. Empirical results for our compression technique are presented, including comparisons with previously introduced techniques, showing that the new technique dominate on all tested instances.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Embedded Systems Design Techniques · Petri Nets in System Modeling
