Compiling Knowledge into Decomposable Negation Normal Form

Abstract

We propose a method for compiling propositional theories into a new tractable form that we refer to as decomposable negation normal form (DNNF). We show a number of results about our compilation approach. First, we show that every propositional theory can be compiled into DNNF and present an algorithm to this effect. Second, we show that if a clausal form has a bounded treewidth, then its DNNF compilation has a linear size and can be computed in linear time - treewidth is a graphtheoretic parameter which measur es the connectivity of the clausal form. Third , we show that once a propositional theory is compiled into DNNF, a number of reasoning tasks, such as satisfiability and forgetting, can be performed in linear time. Finally, we propose two techniques for approximating th e DNNF compilation of a theory when the size of such compilation is too large to be practical. One of the techniques generates a sound but incomplete compilation, while the other generates a complete but unsound compilation. Together, these approximations bound the exact compilation from below and above in terms for their ability to answer queries.