Suppose I have a collection of logical assertions in Z3 and I want to check the satisfiability. Is there a way to bound the total number of Trues/Falses in the satisfying model(s)?
For example, I might have a collection of assertions involving 100 Boolean variables, but I am only interested in solutions with at least 90 Trues.
Yes. There are two relatively easy ways to achieve this:
For a generic SMT solver, simply assert:
(assert (<= 90 (+ (ite v1 1 0) (ite v2 1 0) ...)))
where v1, v2 etc. are your booleans. This makes sure at least
90 of them will be true.
If you're using z3, then you can employ pseudo-boolean constraints. In your case you want PbGe. See this answer for details: K-out-of-N constraint in Z3Py
Note that you can even get z3 to "maximize" the number of true booleans. This will use the optimization engine, and works by maximizing the sum expression in the first option above. You can find many references in SO on how to use the optimizer.