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

CNF to d-DNNF compiler.
link binary only 

CNF to EADT compiler.
link binary only 

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

CNF to Decision-DNNF compiler, exploiting hypergraph partitioning in a dynamic, yet parsimonious way.
link binary only


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

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

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

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