Z3Py中的K-out-of-N约束

Question

我正在使用Python绑定Z3定理证明器(Z3Py).我有N个布尔变量,x1,..,xN.我想表达一个约束条件,即N中的N个应该是真的.我怎么能在Z3Py中做到这一点？有没有内置的支持？我检查了在线文档,但Z3Py文档没有提及任何API.

对于N个中的一个约束,我知道我可以单独表达至少一个是真的(断言Or(x1,..,xN))并且最多只有一个为真(断言Not(And(xi,xj) ))所有i,j).我也知道其他方法来手动表达N-out和N-K-out-of-N约束.但是我的印象是,当解算器内置支持此约束时,它有时比手动表达它更有效.

Answer 1

是的,Z3Py内置了对此的支持.有一个未记录的API,在Z3Py文档中没有提到:使用PbEq.特别是表达

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

如果N个布尔变量中的K个被设置为true,则为真.有一些报道称这种编码比手动表达约束的天真方式更快.

要表示1-out-of-N约束,只需设置K = 1并使用PbEq.要表达最多K-out-of-N约束,请使用PbLe.要表达至少K-out-of-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()