21

I wrote an answer to what I thought was a quite interesting question, but unfortunately the question was deleted by its author before I could post. I'm reposting a summary of the question and my answer here in case it might be of use to anyone else.

Suppose I have a SAT solver that, given a Boolean formula in conjunctive normal form, returns either a solution (a variable assignment that satisfies the formula) or the information that the problem is unsatisfiable.

Can I use this solver to find all the solutions?

Community
  • 1
  • 1
Vectornaut
  • 473
  • 5
  • 11
  • Can the person who downvoted please explain why? After reading this blog entry (http://blog.stackoverflow.com/2011/07/its-ok-to-ask-and-answer-your-own-questions/), I thought what I did here was "not merely OK," but "explicitly encouraged." – Vectornaut Sep 03 '12 at 19:10
  • 1
    It's perfectly ok. Good answer, btw. – Michael Petrotta Sep 03 '12 at 19:15

2 Answers2

13

There is definitely a way to use the SAT solver you described to find all the solutions of a SAT problem, although it may not be the most efficient way.

Just use the solver to find a solution to your original problem, add a clause that does nothing except rule out the solution you just found, use the solver to find a solution to the new problem, and so forth. Keep going until you get a problem that's unsatisfiable.

For example, suppose you want to satisfy (X or Y) and (X or Z). There are five solutions:

  • Four with X true, Y and Z arbitrary.

  • One with X false, Y and Z true.

So you run your solver, and let's say it gives you the solution (X, Y, Z) = (T, F, F). You can rule out this solution---and only this solution---with the constraint

not (X and (not Y) and (not Z))

This constraint can be rewritten as the clause

(not X) or Y or Z

So now you can run your solver on the new problem

(X or Y) and (X or Z) and ((not X) or Y or Z)

and so forth.

Like I said, this is a way to do what you want, but it probably isn't the most efficient way. When your SAT solver is looking for a solution, it learns a lot about the problem, but it doesn't return all that information to you---it just gives you the solution it found. When you run the solver again, it has to re-learn all the information that was thrown away.

Vectornaut
  • 473
  • 5
  • 11
  • What are more efficient ways to achieve it? Z3 or painless are what I use at the moment. – outmind Mar 02 '21 at 01:09
  • @outmind, Takahisa Toda and Takehide Soh have [implemented](http://www.disc.lab.uec.ac.jp/toda/code/allsat.html) some all-solutions SAT solvers in C, and written a [paper](https://dx.doi.org/10.1145/2975585) explaining how they work under the hood. – Vectornaut Mar 02 '21 at 22:13
11

Sure it can. When MiniSat[1] finds a solution

s SATISFIABLE
v 1 2 -3 0

(solution 1=True, 2=True, 3=False) then you have to put into the original CNF[2] a clause that bans this solution:

-1 -2 3 0

(which means, either 1 or 2 must be False or 3 must be True). Then you solve again. You do this until the solver returns UNSAT i.e. that there are no more solutions to the problem. You will insert one clause for each iteration, and each clause will have the same format as the solution except that it's all inverted and has a 0 at the end

It's much faster to do this using the C++ interface of MiniSat, as it can then save intermediate data and the iterations will be faster.

[1] http://minisat.se/

[2] http://fairmut3x.wordpress.com/2011/07/29/cnf-conjunctive-normal-form-dimacs-format-explained/

Mate Soos
  • 191
  • 1
  • 8