Could anyone please point to one or more websites where is possible to download a working implementation of a #SAT solver? I'm interested in those returning the exact solution count, not an approximation.
One option is to use a BDD library, such as JavaBDD. All such libraries either have a function that counts solutions fast or, at least, they make it easy to write such a function. The disadvantage, however, is that constructing the BDD will be slow in many cases and may require much memory.
In case your input is in CNF, a simple heuristic that speeds up the construction of the BDD is the following. First, build a small BDD for each clause and put them into a priority queue whose root is the smallest BDD. Second, pop two BDDs, compute AND between them and push the result to the priority queue. Here's the idea: Since computing AND between BDDs of size $m$ and $n$ takes $O(mn)$ in theory but $\sim m+n$ in practice, minimizing the runtime is the same as finding a Huffman code.
The best I found is "c2d compiler". http://reasoning.cs.ucla.edu/c2d/
It uses d-DNNF and you need the -count option.
Related topic: Best SAT Solver.
The MBound Solver given here http://www.cs.cornell.edu/~sabhar/ can give model counts with probabilistic guarantees. It's much faster than enumerating all solutions.
I wrote a small model/prime implicant enumerator. This can already be used for model counting with the model enumeration but that's not very practical. If anybody's interested, I can extend it so it counts models from prime implicants.
The website BeyondNP contains a good inventory of the existing tools to solve #SAT (and other related hard problems on CNF formulas). You may also find a list of tools for approximate model counting and knowledge compilation (the task of transforming the CNF into a hopefully succinct data structure that often supports polynomial time model counting).
You may also find a list of tools for preprocessing CNF formulas which may be useful to improve the performances of model counters and various benchmarks.
Glucose is a very efficient SAT solver developed at university of Bordeaux.