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]
functionX involves creating matrices based on the boolean expressions, getting their eigenvalues, and measuring the distribution, which is not really part of this question.