<p>I found a more recent (2014) paper on All-SAT at a VLSI conference, so it is definitely geared toward the practical side (which seems in tune with the OP's question here, albeit less so with cstheory.SE in general):</p>

<ul>
<li>"All-SAT using Minimal Blocking Clauses" by Yinlei Yu, Pramod Subramanyan, Nestan Tsiskaridze, Sharad Malik, VLSI Design 2014. <a href="http://dx.doi.org/10.1109/VLSID.2014.22" rel="nofollow">doi:10.1109/VLSID.2014.22</a>.</li>
</ul>

<p>For those without an IEEE subscription, there's a free copy on <a href="http://www.princeton.edu/~psubrama/" rel="nofollow">Subramanyan's Princeton web page</a>. (He uses a file-sharing service to store/distribute copies of his papers and I'm not sure how stable those URLs are, hence this roundabout link.)</p>

<p>The gist of this paper seems to be:</p>

<blockquote>
  <p>Our contribution, the Non-Disjoint-Dec algorithm, generates extremely short blocking clauses that do not contain any of the implied variables in the solver. Note that typically the majority of the variables in a satisfying minterm are implied. Short blocking clauses are very beneficial for solver performance as demonstrated by the evaluation.</p>
</blockquote>

<p>Their implementation builds on MiniSat. Source code for their extension doesn't seem to be publicly available though. Alas this seems to be a habit in the field of All-SAT, so papers in this area which contain experimental results just setup some more-or-less straw-man simpler algorithm to beat and can seldom be directly compared (in terms of experimental results) with any other published algorithm for All-SAT. The paper by Jabbour et al. mentioned by Vijay D is also of this kind.</p>

<p>As I don't see it mentioned in the other answer (but only in the comment of András Salamon), the [rather popular] blocking-clauses techinique was introduced in:</p>

<ul>
<li><a href="http://www.kenmcmil.com/pubs/CAV02.pdf" rel="nofollow">“Applying SAT Methods in Unbounded Symbolic Model Checking”</a> by K. L. McMillan, CAV’02.</li>
</ul>

CC BY-SA 3.0
2015-02-24T11:21:59.460Z
2015-02-24T12:37:09.153Z
2015-02-24T12:37:09.153Z
got trolled too much this week
<p>You are looking for an ALL-SAT or all solutions SAT solver. This is a different problem from #SAT. You do not have to enumerate all solutions to count them. </p>

<p>I do not know of a tool that solves your problem because people add these algorithms on top of existing SAT solvers but rarely seem to release these extensions. Two papers that should help you in modifying a CDCL solver to implement ALL-SAT are below.</p>

<p><a href="http://www.cs.technion.ac.il/users/orna/All_SAT_reachability_FMCAD04.ps.gz">Memory Efficient All-Solutions SAT solver and its Application to Reachability</a>, O. Grumberg, A. Schuster, A. Yadgar, FMCAD 2004</p>

<p>Here is a recent article posted on the arXiv.</p>

<p><a href="http://arxiv.org/abs/1305.0574v1">Extending Modern SAT Solvers for Enumerating All Models</a>, Said Jabbour, Lakhdar Sais, Yakoub Salhi, 2013</p>

<p>You could try contacting these authors for their implementation.</p>

CC BY-SA 3.0
2013-07-05T22:23:39.103Z
For the second paper you just need to click the first version v1 to see it.
Tayfun Pay
CC BY-SA 3.0
2013-07-27T14:09:50.977Z
This recent paper seems related: http://homes.cs.washington.edu/~sudeepa/UAI2013-ModelCounting.pdf
Kaveh
CC BY-SA 3.0
2013-08-10T02:46:42.503Z
@Kaveh, I believe the OP is asking for an ALLSAT solver or a way to turn a #SAT solver into an ALLSAT solver. This is a paper on lower bounds for #SAT. I'm not sure it helps the OP.
Vijay D
CC BY-SA 3.0
2013-07-03T17:46:10.220Z
2013-07-06T07:31:00.123Z
2013-07-06T07:31:00.123Z
Vijay D
<p>All the #SAT solvers I know, e.g RelSat, C2D, only return the number of satisfiable instances. But I want to know each of those instances?</p>

<p>Is there such a #SAT solver or how I should modify an available #SAT solver to do this?</p>

<p>Thank you.</p>

CC BY-SA 3.0
2013-07-03T11:25:23.157Z
This is often called an "all-solutions SAT solver", but doesn't seem to be available off the shelf.  The references I can find talk about modifications to MiniSAT and other solvers, usually by adding blocking clauses to exclude a solution when it is found.  On the other hand, most constraint solvers support generating all solutions as standard.
András Salamon
CC BY-SA 3.0
2013-12-26T16:28:30.530Z
one approach is a CNF→DNF conversion for which there is a lot of literature
vzn
CC BY-SA 4.0
2021-02-19T16:28:46.940Z
The literature on d-DNNF says that they should allow polytime-delay enumeration of all the possible solutions. Why is it not possible in practice?
SagarM
<lo.logic><sat><software>
Enumerate all solutions of a SAT problem
sean
# Enumerate all solutions of a SAT problem

(Asked by: username_0 on 2013-07-03)

All the #SAT solvers I know, e.g RelSat, C2D, only return the number of satisfiable instances. But I want to know each of those instances?

Is there such a #SAT solver or how I should modify an available #SAT solver to do this?

Thank you.

**Tags:** lo.logic, sat, software

> **Comments:**
> **username_1**: This is often called an "all-solutions SAT solver", but doesn't seem to be available off the shelf.  The references I can find talk about modifications to MiniSAT and other solvers, usually by adding blocking clauses to exclude a solution when it is found.  On the other hand, most constraint solvers support generating all solutions as standard.  
> **username_2**: one approach is a CNF→DNF conversion for which there is a lot of literature  
> **username_3**: The literature on d-DNNF says that they should allow polytime-delay enumeration of all the possible solutions. Why is it not possible in practice?  

---

## 2 answers

### Answer by username_5 on 2013-07-03. Score: 14 | Accepted answer

You are looking for an ALL-SAT or all solutions SAT solver. This is a different problem from #SAT. You do not have to enumerate all solutions to count them.

I do not know of a tool that solves your problem because people add these algorithms on top of existing SAT solvers but rarely seem to release these extensions. Two papers that should help you in modifying a CDCL solver to implement ALL-SAT are below.

[Memory Efficient All-Solutions SAT solver and its Application to Reachability](http://www.cs.technion.ac.il/users/orna/All_SAT_reachability_FMCAD04.ps.gz), O. Grumberg, A. Schuster, A. Yadgar, FMCAD 2004

Here is a recent article posted on the arXiv.

[Extending Modern SAT Solvers for Enumerating All Models](http://arxiv.org/abs/1305.0574v1), Said Jabbour, Lakhdar Sais, Yakoub Salhi, 2013

You could try contacting these authors for their implementation.

> **Comments:**
> **username_6**: For the second paper you just need to click the first version v1 to see it.  
> **username_7**: This recent paper seems related: http://homes.cs.washington.edu/~sudeepa/UAI2013-ModelCounting.pdf  
> **username_5**: @username_7, I believe the OP is asking for an ALLSAT solver or a way to turn a #SAT solver into an ALLSAT solver. This is a paper on lower bounds for #SAT. I'm not sure it helps the OP.  

---

### Answer by username_4 on 2015-02-24. Score: 2

I found a more recent (2014) paper on All-SAT at a VLSI conference, so it is definitely geared toward the practical side (which seems in tune with the OP's question here, albeit less so with cstheory.SE in general):

* "All-SAT using Minimal Blocking Clauses" by Yinlei Yu, Pramod Subramanyan, Nestan Tsiskaridze, Sharad Malik, VLSI Design 2014. [doi:10.1109/VLSID.2014.22](http://dx.doi.org/10.1109/VLSID.2014.22).

For those without an IEEE subscription, there's a free copy on [Subramanyan's Princeton web page](http://www.princeton.edu/~psubrama/). (He uses a file-sharing service to store/distribute copies of his papers and I'm not sure how stable those URLs are, hence this roundabout link.)

The gist of this paper seems to be:

> Our contribution, the Non-Disjoint-Dec algorithm, generates extremely short blocking clauses that do not contain any of the implied variables in the solver. Note that typically the majority of the variables in a satisfying minterm are implied. Short blocking clauses are very beneficial for solver performance as demonstrated by the evaluation.

Their implementation builds on MiniSat. Source code for their extension doesn't seem to be publicly available though. Alas this seems to be a habit in the field of All-SAT, so papers in this area which contain experimental results just setup some more-or-less straw-man simpler algorithm to beat and can seldom be directly compared (in terms of experimental results) with any other published algorithm for All-SAT. The paper by Jabbour et al. mentioned by username_5 is also of this kind.

As I don't see it mentioned in the other answer (but only in the comment of username_1), the [rather popular] blocking-clauses techinique was introduced in:

* [“Applying SAT Methods in Unbounded Symbolic Model Checking”](http://www.kenmcmil.com/pubs/CAV02.pdf) by K. L. McMillan, CAV’02.


---

