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?
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.
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.
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.
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.
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With