New Compilation Languages Based on Structured Decomposability

We introduce in this paper two new, complete propositional languages and study their properties in terms of (1) their support for polytime operations and (2) their ability to represent boolean functions compactly. The new languages are based on a structured version of decomposability—a property that underlies a number of tractable languages. The key characteristic of structured decomposability is its support for a polytime conjoin operation, which is known to be intractable for unstructured decomposability. We show that any CNF can be compiled into formulas in the new languages, whose size is only exponential in the treewidth of the CNF. Our study also reveals that one of the languages we identify is as powerful as OBDDs in terms of answering key inference queries, yet is more succinct than OBDDs.

Authors

• Knot Pipatsrisawat Adnan Darwiche

Keywords

No keywords are indexed for this paper.