Augmenting Ordered Binary Decision Diagrams with Conjunctive Decomposition

Original · EN

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.