New compilation languages based on structured decomposability

Abstract

We introduce in this paper two new, complete propositional languages and study their properties in terms of (1) their sup-port 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 charac-teristic of structured decomposability is its support for a poly-time 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.