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.
-
2$\begingroup$ 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. $\endgroup$– Ryan WilliamsSep 14, 2010 at 19:57
-
$\begingroup$ 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. $\endgroup$– Giorgio CameraniSep 15, 2010 at 7:48
-
12$\begingroup$ I'd like to disagree. I think such questions are within scope, and should be ! $\endgroup$– Suresh VenkatSep 15, 2010 at 8:05
-
$\begingroup$ 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... $\endgroup$– vznMar 3, 2013 at 18:40
10 Answers
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.
-
$\begingroup$ Hi supercooldave, thanks for your pointer. I didn't know that SAT4J had this ability. $\endgroup$ Sep 15, 2010 at 7:51
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.
-
$\begingroup$ c2d solves much more CNFs than sharpsat. For toy purposes the "relsat" sat solver will do too. $\endgroup$ Dec 31, 2010 at 12:47
-
1$\begingroup$ 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. $\endgroup$ Sep 15, 2010 at 7:56
-
2$\begingroup$ 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. $\endgroup$ Sep 15, 2010 at 14:07
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.
Here is one called tensorCSP and based on a tool called tensor networks. It is explained in this paper.
Glucose is a very efficient SAT solver developed at university of Bordeaux.