Ordered {AND, OR}-Decomposition and Binary-Decision Diagram

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 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.