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.