21
$\begingroup$

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.

Improve this question
$\endgroup$
4
  • 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 Williams
    Sep 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 Camerani
    Sep 15, 2010 at 7:48
  • 12
    $\begingroup$ I'd like to disagree. I think such questions are within scope, and should be ! $\endgroup$
    – Suresh Venkat
    Sep 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$
    – vzn
    Mar 3, 2013 at 18:40

10 Answers 10

Reset to default
16
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Hi supercooldave, thanks for your pointer. I didn't know that SAT4J had this ability. $\endgroup$
    – Giorgio Camerani
    Sep 15, 2010 at 7:51
16
$\begingroup$

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

Improve this answer
$\endgroup$
0
11
$\begingroup$

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.

Improve this answer
$\endgroup$
8
$\begingroup$

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

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

Improve this answer
$\endgroup$
1
  • $\begingroup$ c2d solves much more CNFs than sharpsat. For toy purposes the "relsat" sat solver will do too. $\endgroup$
    – Leon Leon
    Dec 31, 2010 at 12:47
7
$\begingroup$

Related topic: Best SAT Solver.

Improve this answer
$\endgroup$
2
  • 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$
    – Giorgio Camerani
    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$
    – Sadeq Dousti
    Sep 15, 2010 at 14:07
7
$\begingroup$

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.

Improve this answer
$\endgroup$
5
$\begingroup$

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.

Improve this answer
$\endgroup$
3
$\begingroup$

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.

Improve this answer
$\endgroup$
1
$\begingroup$

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

Improve this answer
$\endgroup$
0
$\begingroup$

Glucose is a very efficient SAT solver developed at university of Bordeaux.

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

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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