2012/08/14 by Yong Lai, Lai, Yong, Dayou Liu +1
Computer Science · #Advanced Algebra and Logic #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #cs.AI #cs.LO
paper · pdf · doi:10.48550/arxiv.1208.2852
The authors have resubmitted a new version with a different tittle, arXiv:1410.6671
openalex publication_date 2012/08/14 · arxiv created 2014/10/27 · arxiv updated 2014/10/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.