StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>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.</p> <p>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.</p> <hr> <p>For example, suppose you want to satisfy <code>(X or Y) and (X or Z)</code>. There are five solutions:</p> <ul> <li><p>Four with <code>X</code> true, <code>Y</code> and <code>Z</code> arbitrary.</p></li> <li><p>One with <code>X</code> false, <code>Y</code> and <code>Z</code> true.</p></li> </ul> <p>So you run your solver, and let's say it gives you the solution <code>(X, Y, Z) = (T, F, F)</code>. You can rule out this solution---and only this solution---with the constraint</p> <pre><code>not (X and (not Y) and (not Z)) </code></pre> <p>This constraint can be rewritten as the clause</p> <pre><code>(not X) or Y or Z </code></pre> <p>So now you can run your solver on the new problem</p> <pre><code>(X or Y) and (X or Z) and ((not X) or Y or Z) </code></pre> <p>and so forth.</p> <hr> <p>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.</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload