I have a large logical expression, with roughly 100 boolean variables. I am interested in the solution with the smallest numbers of
True. It seems there is no such option, thus I use
SatisfiabilityInstances, searching for a large number of instances:
sf = SatisfiabilityInstances[FinalExpression, BooleanVariables[FinalExpression], 100000, Method -> "SAT"];
Afterwards, I search manually for the instance with the smallest number of True.
Question1: Is there a way to obtain the solution with smallest number of True in a more efficient way?
Question2: Is there a way to monitor the intermediate results of
SatisfiabilityInstances? For instance, that it periodically prints how many solutions its already found (and its truth values)