Ordered {AND, OR}-Decomposition and Binary-Decision Diagram
Yong Lai, Dayou Liu

TL;DR
This paper introduces OAODD, an extension of OBDDs with AND and OR decomposition nodes, providing new algorithms for conversion, logical operations, and analysis of space efficiency in knowledge compilation.
Contribution
It defines OAODD, explores its properties, and develops algorithms for conversion and logical operations, advancing knowledge compilation techniques.
Findings
OAODD generalizes several existing decision diagram languages.
Polynomial-time algorithms for logical operations on OAODD are developed.
Theoretical analysis characterizes OAODD's space efficiency and tractability.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, Reasoning, and Knowledge · Advanced Algebra and Logic
