New Canonical Representations by Augmenting OBDDs with Conjunctive Decomposition

Abstract

We identify two families of canonical knowledge compilation languages. Both families augment ROBDD with conjunctive decomposition bounded by an integer i ranging from 0 to ∞. In the former, the decomposition is finest and the decision respects a chain C of variables, while both the decomposition and decision of the latter respect a tree T of variables. In particular, these two families cover the three existing languages ROBDD, ROBDD with as many implied literals as possible, and AND/OR BDD. We demonstrate that each language in the first family is complete, while each one in the second family is incomplete with expressivity that does not decrease with incremental i. We also demonstrate that the succinctness does not decrease from the i-th language in the second family to the i-th language in the first family, and then to the (i+1)-th language in the first family. For the operating efficiency, on the one hand, we show that the two families of languages support a rich class of tractable logical operations, and particularly the tractability of each language in the second family is not less than that of ROBDD; and on the other hand, 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, and we demonstrate that the rapidity of each operation does not decrease from the i-th language in the second family to the i-th language in the first family, and then to the (i+1)-th language in the first family. Furthermore, we develop a compiler for the last language in the first family (i = ∞). Empirical results show that the compiler significantly advances the compiling efficiency of canonical representations. In fact, its compiling efficiency is comparable with that of the state-of-the-art compilers of non-canonical representations. We also provide a compiler for the i-th language in the first family by translating the last language in the first family into the i-th language (i < ∞). Empirical results show that we can sometimes use the i-th language instead of the last language without any obvious loss of space efficiency.