The c2d Compiler


c2d is a system that compiles CNF into d-DNNF (deterministic, decomposable negation normal form). d-DNNF is a tractable logical form that allows operations such as model counting, clausal entailment, and model enumeration and minimization to be performed in linear time. d-DNNF is also a strict superset of OBDD and is strictly more succinct than OBDD.

Read the paper that describes the c2d compiler.
Read the paper that describes d-DNNF and related languages.
See also Ace: a system for compiling Bayesian networks which is based on c2d.
See results of using c2d on some benchmarks.


Download c2d and instructions for using it.

Also check out the new SDD package here!


Send questions and comments to darwiche at