Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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.

share|improve this question
2  
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
11  
I'd like to disagree. I think such questions are within scope, and should be ! –  Suresh Venkat Sep 15 '10 at 8:05
    
@Suresh: Thanks! ;-) –  Giorgio Camerani Sep 15 '10 at 9:06
    
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
add comment

7 Answers 7

up vote 13 down vote accepted

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.

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

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

share|improve this answer
1  
Thanks for your pointer, Holger. –  Giorgio Camerani Sep 21 '10 at 15:10
add comment

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.

share|improve this answer
add comment

Related topic: Best SAT Solver.

share|improve this answer
1  
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
2  
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. –  Sadeq Dousti Sep 15 '10 at 14:07
add comment

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.

share|improve this answer
add comment

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

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

share|improve this answer
    
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
add comment

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.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.