Knowledge Compilers

Knowledge compilation is concerned with converting general types of knowledge into tractable forms, which allows certain hard tasks to be performed efficiently on the compiled forms. For example, one may compile a CNF into an OBDD, allowing one to count the models of the CNF efficiently and under different variable settings. Many of the compiled forms are based on subsets of Negation Normal Form (NNF) including, for example, Ordered Binary Decision Diagrams (OBDD), Sentential Decsion Diagrams (SDD), and Decomposable Negation Normal Form (DNNF).


Knowledge Compilers

c2d
CNF to d-DNNF compiler.
link binary only 

cnf2eadt
CNF to EADT compiler.
link binary only 

CNF2OBDD
CNF to OBDD compiler, based on MiniSat.
link open source

DSHARP
CNF to d-DNNF compiler, based on sharpSAT.
link open source

miniC2D
CNF to SDD compiler (and model counter), based on exhaustive DPLL.
link open source 

SDD
CNF/DNF to SDD compiler, and SDD manipulation package.
link open source (compiler only), binary library

Tree-of-BDDs
CNF to Trees-of-BDDs compiler.
link open source