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.

$\endgroup$
  • 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 '10 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 '10 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 '10 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 '13 at 18:40

10 Answers 10

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.

$\endgroup$
  • $\begingroup$ Hi supercooldave, thanks for your pointer. I didn't know that SAT4J had this ability. $\endgroup$ – Giorgio Camerani Sep 15 '10 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.

$\endgroup$
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.

$\endgroup$
7
$\begingroup$

Related topic: Best SAT Solver.

$\endgroup$
  • 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 '10 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$ – M.S. Dousti Sep 15 '10 at 14:07
7
$\begingroup$

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

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

$\endgroup$
  • $\begingroup$ c2d solves much more CNFs than sharpsat. For toy purposes the "relsat" sat solver will do too. $\endgroup$ – Leon Leon Dec 31 '10 at 12:47
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.

$\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.

$\endgroup$
2
$\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.

$\endgroup$
1
$\begingroup$

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

$\endgroup$
0
$\begingroup$

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

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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