New canonical representations by augmenting OBDDS with conjunctive decomposition

Abstract

We identify two families of canonical representations called ROBDD [∧î]C and ROBDD [∧T,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 (ROBDD-L∞), 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 [∧T,i]T to ROBDD [∧î]C, and then to ROBDD [∧i+1]C. We also demonstrate that ROBDD [∧î]C (i > 1) and ROBDD [∧T,i]T are not less tractable than ROBDD-L∞ and ROBDD, respectively. Finally, we develop a compiler for ROBDD [∧∞]C which significantly advances the compiling efficiency of canonical representations.