An answer to this question on Stack Overflow.

Question

I am using z3py to convert cardinality constraints into CNF. The tactic I used is t = Then('simplify', 'card2bv', 'simplify', 'bit-blast', 'tseitin-cnf'). My goal has 100 constraints over around 800 variables. The conversion takes around 48 minutes on an Intel Xeon CPU. Is the tactic that I used the most efficient one for this kind of constraints in terms of compactness or speed?

Does z3 implement something like sequential counters from Sinz, 2005 [1]?

[1] http://www.carstensinz.de/papers/CP-2005.pdf

Answer

Z3 is capable of using pseudo-boolean inequality constraints, which can be used to express cardinality.

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()