Efficient way of iterating over satisfiability instances

Question

I am working on a problem that involves searching through solutions to a boolean equation, to see if any have a specific property. As the computations are not particularly fast, I would like to minimize the number I run. For this, the SelectFirst function is helpful, but not fast enough.

The only way I found to get all the solutions to a boolean equation is:

SatisfiabilityInstances[expression, vars, SatisfiabilityCount[expression]]

This works, but will often generate more than is needed. sometimes, the first expression works, but other times, it takes thousands. While SelectFirst can speed up some of the computation, there are still way more solutions generated than are needed most of the time. Is there a way to get the SatisfiabilityInstances one at a time, so that I only generate as many as I need? Or at least something better than what I have now?

---

The code ends up looking something like:

SatisfiabilityInstances[expression, vars, SatisfiabilityCount[expression]]
  // SelectFirst[functionX]

The specific functionX involves creating matrices based on the boolean expressions, getting their eigenvalues, and measuring the distribution, which is not really part of this question.

Answer 1

Note you can use SatisfiabilityInstances[expression, vars, All] to obtain all solutions, but if your specific property is common enough this is indeed inefficient. In this case, a better approach would be to use a randomized algorithm, e.g. try running a few times

FindInstance[expression, vars, Booleans, RandomSeeding -> Automatic]

However, this may or may not give different solutions according to your specific problem, so you may need to additionally randomize your expression somehow (e.g. rename variables, reorder terms, etc)... and even this is not guaranteed to work.

If on the other hand your property is not very common, you'd probably be better off trying to include it (or some of its necessary conditions) as extra terms in your expression, which either solves your problem immediately or eventually brings you back to the case outlined above.