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.

  • $\begingroup$ Welcome to Mathematica.SE! I suggest the following: 1) As you receive help, try to give it too, by answering questions in your area of expertise. 2) Take the tour and check the faqs! 3) When you see good questions and answers, vote them up by clicking the gray triangles, because the credibility of the system is based on the reputation gained by users sharing their knowledge. Also, please remember to accept the answer, if any, that solves your problem, by clicking the checkmark sign $\endgroup$
    – Dunlop
    Jun 3, 2021 at 5:10
  • $\begingroup$ Can you give an example code of an expression that you are looking at? this may help others give you a solution $\endgroup$
    – Dunlop
    Jun 3, 2021 at 5:12
  • 2
    $\begingroup$ I do not think there is a way to get them one by one. This comment I wrote is relevant: community.wolfram.com/groups/-/m/t/1781821 $\endgroup$
    – Szabolcs
    Jun 3, 2021 at 9:38
  • $\begingroup$ @Szabolcs That is helpful. It would be so nice to have iterators in the language. $\endgroup$
    – MegaTom
    Jun 4, 2021 at 0:53

1 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.

  • $\begingroup$ Using All is much cleaner. Thank you for that suggestion! $\endgroup$
    – MegaTom
    Jun 3, 2021 at 14:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.