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.
$\begingroup$
$\endgroup$
-
7$\begingroup$ 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. $\endgroup$ – András Salamon Jul 3 '13 at 11:25
-
$\begingroup$ one approach is a CNF→DNF conversion for which there is a lot of literature $\endgroup$ – vzn Dec 26 '13 at 16:28
$\begingroup$
$\endgroup$
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, 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, Said Jabbour, Lakhdar Sais, Yakoub Salhi, 2013
You could try contacting these authors for their implementation.
-
$\begingroup$ For the second paper you just need to click the first version v1 to see it. $\endgroup$ – Tayfun Pay Jul 5 '13 at 22:23
-
$\begingroup$ This recent paper seems related: homes.cs.washington.edu/~sudeepa/UAI2013-ModelCounting.pdf $\endgroup$ – Kaveh Jul 27 '13 at 14:09
-
1$\begingroup$ @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. $\endgroup$ – Vijay D Aug 10 '13 at 2:46
$\begingroup$
$\endgroup$
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.
For those without an IEEE subscription, there's a free copy on Subramanyan's Princeton web page. (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 Vijay D is also of this kind.
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:
- “Applying SAT Methods in Unbounded Symbolic Model Checking” by K. L. McMillan, CAV’02.
