Tools

Solvers may also benefit from the use of independent tools, which can (for example) convert problems from other domains to CNF formats, to pre-process inputs or to post-process outputs.


File Format Converters


Pre-Processors

B+E
A CNF pre-processfor for model counters and knowledge compilers. B+E tracks definability relations between variables (aka gates) and use them to reduce the instance by eliminating variables which have been identified as outputs of some gates.
link binary only 

PMC
A CNF pre-processfor for model counters and knowledge compilers. Preprocessings include occurrence reduction, vivification, backbone identification, as well as equivalence, AND and XOR gate identification and replacement.
link binary only


Libraries

CUDD
A library for constructing and manipulating OBDDs.
link open-source

The SDD Package
A library for constructing and manipulating SDDs.
link binary only