The c2d Compiler
Description
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 results of
using c2d on some benchmarks.
Download
Download c2d and instructions for using it.
Related Software
miniC2D:
A software package for knowledge compilation and model counting based on exhaustive DPLL.
Ace:
A system for compiling Bayesian networks which is based on c2d.
The SDD Package:
A system for constructing, manipulating, and optimizing Sentential Decision Diagrams (SDDs).
B+E:
A CNF preprocessor. See results on c2d in:
J.-M. Lagniez, E. Lonca, P. Marquis. "Improving Model Counting by Leveraging Definability". Proceedings of IJCAI'16, pages 751-757.
paper
Contact
Send questions and comments to darwiche at cs.ucla.edu.