Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Can a SAT solver be used to find all solutions?

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?

like image 519
Vectornaut Avatar asked Sep 03 '12 18:09

Vectornaut


People also ask

What are SAT solvers used for?

A SAT solver is an algorithm for establishing satisfiability. It takes the Boolean logic formula as input and returns if it finds a combination of variables that can satisfy it or if it can demonstrate that no such combination exists.

Can SAT be solved in polynomial time?

Introduction. The Satisfiability problem (SAT) is to determine whether there exists a satisfying truth assignment for a given Boolean expression, usually in conjunctive normal form (CNF). This problem is NP-complete; thus, there is no known polynomial-time algorithm for solving it.

What is PySAT?

PySAT is a Python (2.7, 3.4+) toolkit, which aims at providing a simple and unified interface to a number of state-of-art Boolean satisfiability (SAT) solvers as well as to a variety of cardinality and pseudo-Boolean encodings.

What SAT programming?

SAT (in the context of algorithms) is the Boolean satisfiability problem which asks whether the variables in a given boolean formula can be set such that the formula evaluates to TRUE. For example, in p(x) = not x we can set x = FALSE , so p is satisfiable.


1 Answers

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.

like image 60
Vectornaut Avatar answered Sep 20 '22 18:09

Vectornaut