Augmenting Ordered Binary Decision Diagrams with Conjunctive Decomposition
share
This paper augments OBDD with conjunctive decomposition to propose a generalization called OBDD[∧]. By imposing reducedness and the finest ∧-decomposition bounded by integer i (∧_i-decomposition) on OBDD[∧], we identify a family of canonical languages called ROBDD[∧_i], where ROBDD[∧_0] is equivalent to ROBDD. We show that the succinctness of ROBDD[∧_i] is strictly increasing when i 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[∧_i] is increasing when i increases; particularly, the rapidity of some operations (e.g., conjoining) is strictly increasing. Finally, our empirical results show that: a) the size of ROBDD[∧_i] is normally not larger than that of the equivalent i+1; b) conjoining two ROBDD[∧_1]s is more efficient than conjoining two ROBDD[∧_0]s in most cases, where the former is NP-hard but the latter is in P; and c) the space-efficiency of ROBDD[∧_∞] is comparable with that of d-DNNF and that of another canonical generalization of called SDD.
READ FULL TEXT