<p>You can also try the #SAT solver &quot;sharpSAT&quot; (<a href="https://sites.google.com/site/marcthurley/sharpsat" rel="noreferrer">website</a>, <a href="https://github.com/marcthurley/sharpSAT/" rel="noreferrer">github</a>) for counting the number of satisfying assignments of CNF formulas.</p>

CC BY-SA 3.0
2010-09-21T14:46:55.383Z
2013-08-19T06:30:55.880Z
2020-06-17T09:38:08.363Z
Holger
<p>One option is to use a BDD library, such as <a href="http://javabdd.sourceforge.net/">JavaBDD</a>. 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.</p>

<p>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.</p>

CC BY-SA 2.5
2010-09-15T10:35:07.213Z
2010-09-15T10:35:07.213Z
Radu GRIGore
<p>The best I found is "c2d compiler". <a href="http://reasoning.cs.ucla.edu/c2d/" rel="noreferrer">http://reasoning.cs.ucla.edu/c2d/</a></p>

<p>It uses d-DNNF and you need the <strong>-count</strong> option.</p>

CC BY-SA 2.5
2010-12-31T12:47:21.437Z
c2d solves much more CNFs than sharpsat. For _toy_ purposes the "relsat" sat solver will do too.
Leon Leon
CC BY-SA 2.5
2010-12-31T12:34:07.713Z
2010-12-31T12:34:07.713Z
Leon Leon
<p>Related topic: <a href="https://cstheory.stackexchange.com/q/1060/873">Best SAT Solver</a>.</p>

CC BY-SA 2.5
2010-09-15T07:56:46.477Z
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
CC BY-SA 2.5
2010-09-15T14:07:37.367Z
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
CC BY-SA 2.5
2010-09-15T07:27:23.340Z
2010-09-20T17:38:59.183Z
2017-04-13T12:32:28.077Z
Sadeq Dousti
<p>The MBound Solver given here <a href="http://www.cs.cornell.edu/~sabhar/">http://www.cs.cornell.edu/~sabhar/</a> can give model counts with probabilistic guarantees. It's much faster than enumerating all solutions.</p>

CC BY-SA 3.0
2011-06-19T07:37:39.293Z
2011-06-19T07:37:39.293Z
Opt
<p>I wrote a small <a href="http://sat.inesc-id.pt/~mikolas/sw/pienum/" rel="noreferrer" title="enumerator">model/prime implicant enumerator</a>. 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.</p>

CC BY-SA 3.0
2011-07-03T18:45:10.093Z
2011-07-03T18:45:10.093Z
Mikolas
<p>The website <a href="http://beyondnp.org/pages/solvers/model-counters-exact/" rel="nofollow noreferrer">BeyondNP</a> 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 <strong>approximate model counting</strong> and <strong>knowledge compilation</strong> (the task of transforming the CNF into a hopefully succinct data structure that often supports polynomial time model counting). </p>

<p>You may also find a list of tools for <strong>preprocessing</strong> CNF formulas which may be useful to improve the performances of model counters and various <strong>benchmarks</strong>.</p>

CC BY-SA 4.0
2019-09-19T17:22:19.100Z
2019-09-19T17:22:19.100Z
holf
<p><a href="https://gitlab.com/kourtis/tensorCSP" rel="nofollow noreferrer">Here is one</a> called tensorCSP and based on a tool called tensor networks. It is explained in <a href="https://arxiv.org/abs/1805.00475" rel="nofollow noreferrer">this paper</a>.</p>

CC BY-SA 4.0
2019-09-18T21:56:10.903Z
2019-09-18T21:56:10.903Z
delete000
<p>Glucose is a very efficient SAT solver developed at university of Bordeaux.</p>

<p><a href="https://www.labri.fr/perso/lsimon/glucose/" rel="nofollow noreferrer">https://www.labri.fr/perso/lsimon/glucose/</a></p>

CC BY-SA 4.0
2019-09-19T12:35:52.490Z
2019-09-19T12:35:52.490Z
Lamine
<p>You can do this with <a href="http://www.sat4j.org/">SAT4J</a>, simply by iterating over all models: <a href="http://www.sat4j.org/howto.php#models">http://www.sat4j.org/howto.php#models</a>. I imagine that most SAT solvers have this ability.</p>

CC BY-SA 2.5
2010-09-15T07:51:18.097Z
Hi supercooldave, thanks for your pointer. I didn't know that SAT4J had this ability.
Giorgio Camerani
CC BY-SA 2.5
2010-09-14T19:18:57.603Z
2010-09-14T19:18:57.603Z
Dave Clarke
<p>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.</p>

CC BY-SA 3.0
2013-03-03T18:40:07.083Z
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
CC BY-SA 2.5
2010-09-14T19:57:50.690Z
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
CC BY-SA 2.5
2010-09-15T07:48:30.067Z
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
CC BY-SA 2.5
2010-09-15T08:05:41.990Z
I'd like to disagree. I think such questions are within scope, and should be !
Suresh Venkat
<ds.algorithms><sat><software>
#SAT Solver download
Giorgio Camerani
# #SAT Solver download

(Asked by: username_0 on 2010-09-14)

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.

**Tags:** ds.algorithms, sat, software
> **Comments:**
> **username_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.  
> **username_0**: 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.  
> **username_3**: I'd like to disagree. I think such questions are within scope, and should be !  
> **username_1**: 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...  

---

## 10 answers

### Answer by username_13 on 2010-09-14. Score: 16 | Accepted answer

You can do this with [SAT4J](http://www.sat4j.org/), simply by iterating over all models: <http://www.sat4j.org/howto.php#models>. I imagine that most SAT solvers have this ability.

> **Comments:**
> **username_0**: Hi supercooldave, thanks for your pointer. I didn't know that SAT4J had this ability.  

---

### Answer by username_4 on 2010-09-21. Score: 16

You can also try the #SAT solver "sharpSAT" ([website](https://sites.google.com/site/marcthurley/sharpsat), [github](https://github.com/marcthurley/sharpSAT/)) for counting the number of satisfying assignments of CNF formulas.


---

### Answer by username_5 on 2010-09-15. Score: 11

One option is to use a BDD library, such as [JavaBDD](http://javabdd.sourceforge.net/). 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.


---

### Answer by username_6 on 2010-12-31. Score: 8

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

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

> **Comments:**
> **username_6**: c2d solves much more CNFs than sharpsat. For _toy_ purposes the "relsat" sat solver will do too.  

---

### Answer by username_7 on 2010-09-15. Score: 7

Related topic: [Best SAT Solver](https://cstheory.stackexchange.com/q/1060/873).

> **Comments:**
> **username_0**: 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.  
> **username_7**: 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.  

---

### Answer by username_8 on 2011-06-19. Score: 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.


---

### Answer by username_9 on 2011-07-03. Score: 5

I wrote a small [model/prime implicant enumerator](http://sat.inesc-id.pt/~mikolas/sw/pienum/ "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.


---

### Answer by username_10 on 2019-09-19. Score: 3

The website [BeyondNP](http://beyondnp.org/pages/solvers/model-counters-exact/) 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**.


---

### Answer by username_11 on 2019-09-18. Score: 1

[Here is one](https://gitlab.com/kourtis/tensorCSP) called tensorCSP and based on a tool called tensor networks. It is explained in [this paper](https://arxiv.org/abs/1805.00475).


---

### Answer by username_12 on 2019-09-19. Score: 0

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

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


---

