z3 cardinality constraint to CNF

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

It might be easier and faster to use [bc2cnf](https://users.ics.aalto.fi/tjunttil/circuits/). It has built-in `cardinality` gates. — Axel Kemper, Jul 05 '18 at 19:11
See [K-out-of-N constraint in Z3Py](https://stackoverflow.com/questions/43081929/k-out-of-n-constraint-in-z3py). — Jeffrey Bosboom, Jun 03 '19 at 06:23

score 3 · Answer 1 · answered Jan 24 '19 at 13:54

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

z3 cardinality constraint to CNF

1 Answers1