#SAT Solver download

Question

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 07:48
I'd like to disagree. I think such questions are within scope, and should be ! — Suresh Venkat, Sep 15 '10 at 08: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 03 '13 at 18:40

score 16 · Accepted Answer · answered Sep 14 '10 at 19:18

16

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.

answered Sep 14 '10 at 19:18

Dave Clarke

16,666
3
60
106

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

score 16 · Answer 2 · edited Jun 17 '20 at 09:38

16

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

edited Jun 17 '20 at 09:38

Community

1

answered Sep 21 '10 at 14:46

Holger

975
9
17

score 11 · Answer 3 · answered Sep 15 '10 at 10:35

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.

score 8 · Answer 4 · answered Dec 31 '10 at 12:34

8

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

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

answered Dec 31 '10 at 12:34

Leon Leon

343
2
7

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

score 7 · Answer 5 · edited Apr 13 '17 at 12:32

7

Related topic: Best SAT Solver.

edited Apr 13 '17 at 12:32

Community

1

answered Sep 15 '10 at 07:27

Sadeq Dousti

16,479
9
69
152

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 07:56
2

You are most welcome. Among the links cited there, there was one which was purely practical: http://www.satcompetition.org/. I think you can find very good implementations there. – Sadeq Dousti Sep 15 '10 at 14:07

score 7 · Answer 6 · answered Jun 19 '11 at 07:37

7

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.

answered Jun 19 '11 at 07:37

Opt

1,311
14
20

score 5 · Answer 7 · answered Jul 03 '11 at 18:45

5

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.

answered Jul 03 '11 at 18:45

Mikolas

1,322
9
13

score 3 · Answer 8 · answered Sep 19 '19 at 17:22

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.

score 1 · Answer 9 · answered Sep 18 '19 at 21:56

1

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

answered Sep 18 '19 at 21:56

delete000

818
8
16

score 0 · Answer 10 · answered Sep 19 '19 at 12:35

0

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

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

answered Sep 19 '19 at 12:35

Lamine

1,138
1
12
21

#SAT Solver download

10 Answers10

Linked