I am using the Python bindings for the Z3 theorem prover (Z3Py). I have N boolean variables, x1,..,xN. I want to express the constraint that exactly K out of N of them should be true. How can I do that, in Z3Py? Is there any built-in support for that? I checked the online documentation, but the Z3Py docs don't have any mention of any API for that.
For one-out-of-N constraints, I know I can separately express that at least one is true (assert Or(x1,..,xN)) and that at most one is true (assert Not(And(xi,xj)) for all i,j). I also know of other ways to manually express the 1-out-of-N and K-out-of-N constraints. However I have the impression that when the solver has built-in support for this constraint, it can sometimes be more efficient than expressing it manually.
Yes, Z3Py has built-in support for this. There is an undocumented API for this, that isn't mentioned in the Z3Py docs: use PbEq. In particular, the expression
PbEq(((x1,1),(x2,1),..,(xN,1)),K)
will be true if exactly K out of the N boolean variables are set to true. There are some reports that this encoding will be faster than naive ways of manually expressing the constraint.
To express a 1-out-of-N constraint, just set K=1 and use PbEq. To express an at-most-K-out-of-N constraint, use PbLe. To express an at-least-K-out-of-N constraint, use PbGe.
You can express this in Python like this:
import z3
s = z3.Solver()
bvars = [z3.Bool("Var {0}".format(x)) for x in range(10)]
#Exactly 3 of the variables should be true
s.add( z3.PbEq([(x,1) for x in bvars], 3) )
s.check()
m = s.model()
s = z3.Solver()
bvars = [z3.Bool("Var {0}".format(x)) for x in range(10)]
#<=3 of the variables should be true
s.add( z3.PbLe([(x,1) for x in bvars], 3) )
s.check()
m = s.model()
s = z3.Solver()
bvars = [z3.Bool("Var {0}".format(x)) for x in range(10)]
#>=3 of the variables should be true
s.add( z3.PbGe([(x,1) for x in bvars], 3) )
s.check()
m = s.model()
