Abstract
We identify two families of canonical representations called ROBDD[/\i^]_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[/\i^]_C, and then to ROBDD[/\i+1^]_C. We also demonstrate that ROBDD[/\i^]_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.
Keywords
- Knowledge Representation, Reasoning, and Logic: Computational Complexity of Reasoning
- Knowledge Representation, Reasoning, and Logic: Knowledge Representation Languages
- Knowledge Representation, Reasoning, and Logic: Tractable languages and knowledge compilation
