Ordered {AND, OR}-Decomposition and Binary-Decision Diagram
This work addresses the problem of improving knowledge compilation efficiency for AI and logic reasoning, but it appears incremental as it builds on existing languages like OBDD and AOBDD.
The paper introduces Ordered {AND, OR}-Decomposition and Binary-Decision Diagram (OAODD), a knowledge compilation language that extends OBDDs with AND and OR decomposition nodes, and characterizes its space efficiency and tractability through theoretical analysis and polynomial-time algorithms.
In the context of knowledge compilation (KC), we study the effect of augmenting Ordered Binary Decision Diagrams (OBDD) with two kinds of decomposition nodes, i.e., AND-vertices and OR-vertices which denote conjunctive and disjunctive decomposition of propositional knowledge bases, respectively. The resulting knowledge compilation language is called Ordered {AND, OR}-decomposition and binary-Decision Diagram (OAODD). Roughly speaking, several previous languages can be seen as special types of OAODD, including OBDD, AND/OR Binary Decision Diagram (AOBDD), OBDD with implied Literals (OBDD-L), Multi-Level Decomposition Diagrams (MLDD). On the one hand, we propose some families of algorithms which can convert some fragments of OAODD into others; on the other hand, we present a rich set of polynomial-time algorithms that perform logical operations. According to these algorithms, as well as theoretical analysis, we characterize the space efficiency and tractability of OAODD and its some fragments with respect to the evaluating criteria in the KC map. Finally, we present a compilation algorithm which can convert formulas in negative normal form into OAODD.