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
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 cs.ucla.edu.