New Canonical Representations by Augmenting OBDDs with Conjunctive
Decomposition (Extended Abstract)?
Abstract
We identify two families of canonical representations called ROBDD[?bi]C and ROBDD[?Tb,i]T by
augmenting ROBDD with two types of conjunctive decompositions. These representations cover the three existing languages ROBDD, ROBDD
with as many implied literals as possible (ROBDDL?), and AND/OR BDD. We introduce a new time
efficiency criterion called rapidity which reflects
the idea that exponential operations may be preferable if the language can be exponentially more succinct. Then we demonstrate that the expressivity, succinctness and operation rapidity do not decrease from ROBDD[?Tb,i]T to ROBDD[?bi]C, and
then to ROBDD[?[i+1]C. We also demonstrate that
ROBDD[?bi]C (i > 1) and ROBDD[?Tb,i]T are
not less tractable than ROBDD-L? and ROBDD,
respectively. Finally, we develop a compiler for
ROBDD[?c?]C which significantly advances the
compiling efficiency of canonical representations