A Compiler for Deterministic, Decomposable Negation Normal Form

Abstract

We present a compiler for converting CNF formulas into deterministic, decomposable negation normal form (d-DNNF). This is a logical form that has been identified recently and shown to support a number of operations in polynomial time, including clausal entailment; model counting, minimization and enumeration; and probabilistic equivalence testing, d-DNNFs are also known to be a superset of, and more succinct than, OBDDs. The polytime logical operations supported by d-DNNFs are a subset of those supported by OBDDs, yet are sufficient for model-based diagnosis and planning applications. We present experimental results on compiling a variety of CNF formulas, some generated randomly and others corresponding to digital circuits. A number of the formulas we were able to compile efficiently could not be similarly handled by some state-of-the-art model counters, nor by some state-of-the-art OBDD compilers.