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

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

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

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

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

Based on adaptive Markov Chain Monte Carlo.
link open source

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

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