Encoding "at-most-k / at-least-k booleans are true" constraints in Z3

Question

What's a good way to encode "at least k / at most k of these boolean variables must be true" constraints in Z3, for arbitrary k and number of boolean variables?

I'm thinking of casting "at least k" as a pseudo-boolean problem by introducing new PB variables (using this encoding), relating them to my boolean variables through a biconditional (e.g. x == true iff y == 1), and asserting that their sum is greater than or equal to k. Is this a reasonable approach, or is there a simpler / more efficient encoding that I should use instead?

Answer 1

The easiest is to encode cardinality constraints using arithmetic. So if you want to say a + b + c <= 2, where a, b, c are Bool, then you can formulate it as (if a 1 0) + (if b 1 0) + (if c 1 0) >= 2. The underlying solver, Simplex, often does a very reasonable job with this encoding.

There are many other way to deal with cardinality constraints. One is to compile cardinality constraints into "sorting circuits", and there is quite developed methods in this end. A future version of Z3 will have direct support for cardinality constraints, and more generally pseudo-Boolean inequalities. If you have many cardinality constraints and feel very adventurous you are welcome to try out the "opt" branch where this is being developed. It uses dedicated format for pseudo-Boolean inequalities and it also include a mode where it detects "(if a 1 0) + (if b 1 0) + (if c 1 0) >= 2" inequalities as PB inequalities. That said, I would first try the very simple encoding and see how the simplex-based engine works for your domain.