A compiler for deterministic, decomposable negation normal form
Adnan Y. Darwiche · 2002
We present a compiler for converting CNF formulas into de-terministic, 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 applica-tions. We present experimental results on compiling a variety of CNF formulas, some generated randomly and others cor-responding to digital circuits. A number of the formulas we were able to compile efficiently could not be similarly han-dled by some state-of-the-art model counters, nor by some state-of-the-art OBDD compilers.