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.
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this communityAll 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.
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.
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):
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: