A Compiler for Deterministic, Decomposable Negation Normal Form

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 18

Satisfiability

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 oncompiling 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 somestate-of-the-art OBDD compilers.