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.

• Hi Walter, your question is close to the border of what would be officially "on-topic" for this site. However, if you have nowhere else to ask this question and we can answer it, perhaps it's not that bad... (Since the site is still under development, I think we are being more open than other sites may be.) Rest assured that the point of this comment is not to "scold" or "warn", it is just a friendly notice. – Ryan Williams Sep 14 '10 at 19:57
• Hi Ryan, thanks for your notice. I'm sorry if this question is close to the border. I've searched on the web and I didn't find anything: only some SAT solvers, but no #SAT solvers. That's why I've asked here. Of course I know that I can write my own code which uses a SAT solver as an engine to count solutions, but I was looking for something already made and ready to use. – Giorgio Camerani Sep 15 '10 at 7:48
• I'd like to disagree. I think such questions are within scope, and should be ! – Suresh Venkat Sep 15 '10 at 8:05
• agree its in scope. fyi/imho its not too practical to build a #SAT solver from a SAT solver unless one has the source code and even in that case, not so practical, except for very small formulas, because of a very bad exponential blowup. usually special techniques unique to #SAT and not SAT would be required... – vzn Mar 3 '13 at 18:40

You can do this with SAT4J, simply by iterating over all models: http://www.sat4j.org/howto.php#models. I imagine that most SAT solvers have this ability.

• Hi supercooldave, thanks for your pointer. I didn't know that SAT4J had this ability. – Giorgio Camerani Sep 15 '10 at 7:51

You can also try the #SAT solver "sharpSAT" (website, github) for counting the number of satisfying assignments of CNF formulas.

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.

Related topic: Best SAT Solver.

• Thanks Sadeq. The topic you indicated seems to be theoretical-oriented. It lists several papers on decreasing the upper bound. It's very interesting, but I was looking for a ready-to-use working implementation. – Giorgio Camerani Sep 15 '10 at 7:56
• You are most welcome. Among the links cited there, there was one which was purely practical: satcompetition.org. I think you can find very good implementations there. – M.S. Dousti Sep 15 '10 at 14:07

The best I found is "c2d compiler". http://reasoning.cs.ucla.edu/c2d/

It uses d-DNNF and you need the -count option.

• c2d solves much more CNFs than sharpsat. For toy purposes the "relsat" sat solver will do too. – Leon Leon Dec 31 '10 at 12:47

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.

Here is one called tensorCSP and based on a tool called tensor networks. It is explained in this paper.

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.

https://www.labri.fr/perso/lsimon/glucose/