Ограничение K-вне-N в Z3Py

Да, Z3Py имеет встроенную поддержку для этого. Для этого существует недокументированный API, который не упоминается в документации Z3Py: используйте PbEq. В частности, выражение

PbEq(((x1,1),(x2,1),..,(xN,1)),K)

будет истинным, если ровно K из N логических переменных установлено в истинное значение. Есть некоторые отчеты о том, что эта кодировка будет быстрее, чем наивные способы выражения ограничения вручную.

Чтобы выразить ограничение 1 из N, просто установите K = 1 и используйте PbEq. Чтобы выразить ограничение не более K из N, используйте PbLe. Чтобы выразить ограничение как минимум K из N, используйте PbGe.

Вы можете выразить это в Python так:

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