CODEWITHSUNDEEP
z3
Josh Rosen
Josh Rosen

Reputation: 13841

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

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?

Upvotes: 5

Views: 2389

Answers (2)

Aster
Aster

Reputation: 61

For at least k boolean variables must be true, you can write in Python:

from z3 import *

booleans = [Bool('var{}'.format(n)) for n in range(10)] # 10 variables

s = Solver()

# To change k by an integer of your choice
s.add(PbEq([(b,1) for b in booleans], k))

Upvotes: 0

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

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.

Upvotes: 5

Related Questions