1

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.

Rocket Man
  • 113
  • 3

1 Answers1

2

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.

alias
  • 28,120
  • 2
  • 23
  • 40
  • Being able to assert conditions on subsets of the variables is exactly what I was looking for. Thanks! – Rocket Man Jun 16 '21 at 23:51
  • For folks trying the first cardinality constraint encoding, just know it can be kinda inefficient (absent arbitrary preprocessing). If solving happens to be slow, you may want to look at solver statistics for the # of theory lemmas. After ite purification, the `<=` constraint only becomes inconsistent after 11/100 vK variables are set to false. If all of these combination are otherwise valid, this can take a while. A good place to start on cardinality constraint encodings is: https://heron.model.in.tum.de/files/paper.pdf . – Tim Jun 17 '21 at 03:26
  • @Tim Thanks for the pointer. This is why I pointed out the pseudo-boolean encoding as supported by z3, which use a more efficient encoding. See Section 6.2.3 of https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-boolean-theories – alias Jun 17 '21 at 03:59
  • @alias For clarity I think the first encoding is reasonable and IMO is what folks without more specialized solvers should try first. I just want to give them a heads up that things can go wrong, and what some next steps to take are. – Tim Jun 17 '21 at 19:26