Model Counters

Model counting is the problem of determining the number of assignments satisfying a given propositional formula (typically represented as a CNF). Model counting, and weighted model counting, are central to many AI problems including probabilistic inference. Model counting is #P-complete, and hard to approximate. It is also often supported by knowledge compilers.


Exact Model Counters

Cachet
Based on ZChaff SAT solver, with component caching and clause learning.
link open source

miniC2D
Model counter based on exhaustive DPLL, whose trace is an SDD.
link open source 

sharpSAT
Based on DPLL SAT solving.
link open source

Model Counting via Knowledge Compilation
Some knowledge compilers support model counting, such as c2d, cnf2eadt, CNF2OBDD, DSHARP, and SDD.
see Knowledge Compilers


Approximate Model Counters

ApproxMC
Based on randomly generated parity constraints, using a SAT solver as a black box.
link open source

FocusedFlatSAT
Based on adaptive Markov Chain Monte Carlo.
link open source

MBound
Based on employing randomly generated parity constraints to streamline an input formula.
link open source

SampleCount
Based on solution sampling, and guarantees lower bounds.
link open source

Search Tree Sampler
Based on sampling search trees in a breadth-first manner.
link open source