# Efficient way of iterating over satisfiability instances

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.

• 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 Jun 3, 2021 at 5:10
• Can you give an example code of an expression that you are looking at? this may help others give you a solution Jun 3, 2021 at 5:12
• 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 Jun 3, 2021 at 9:38
• @Szabolcs That is helpful. It would be so nice to have iterators in the language. Jun 4, 2021 at 0:53

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]

• Using All is much cleaner. Thank you for that suggestion! Jun 3, 2021 at 14:00