Augmenting Ordered Binary Decision Diagrams with Conjunctive Decomposition
Yong Lai, Dayou Liu, Minghao Yin

TL;DR
This paper introduces a generalized form of OBDD with conjunctive decomposition, demonstrating increased succinctness and efficiency through theoretical analysis and empirical evaluation of various decomposition levels.
Contribution
It proposes a new canonical language family ROBDD[$ abla$], analyzing its properties, efficiency, and practical advantages over existing representations.
Findings
Succinctness increases with higher decomposition levels.
Conjoining ROBDD[$ abla$]s is more efficient at certain levels.
Space-efficiency comparable to d-DNNF and SDD.
Abstract
This paper augments OBDD with conjunctive decomposition to propose a generalization called OBDD[]. By imposing reducedness and the finest -decomposition bounded by integer (-decomposition) on OBDD[], we identify a family of canonical languages called ROBDD[], where ROBDD[] is equivalent to ROBDD. We show that the succinctness of ROBDD[] is strictly increasing when increases. We introduce a new time-efficiency criterion called rapidity which reflects that exponential operations may be preferable if the language can be exponentially more succinct, and show that: the rapidity of each operation on ROBDD[] is increasing when increases; particularly, the rapidity of some operations (e.g., conjoining) is strictly increasing. Finally, our empirical…
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 · Logic, Reasoning, and Knowledge · Constraint Satisfaction and Optimization
