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

Question

我正在使用Z3 theorem prover (Z3Py) 的 Python 绑定。我有 N 个布尔变量，x1,..,xN。我想表达一个约束，即其中 N 个中的 K 个应该为真。在 Z3Py 中我该怎么做？是否有任何内置支持？我查看了在线文档，但 Z3Py docs 没有提及任何 API。

对于 N 中取一的约束，我知道我可以分别表示至少一个为真（断言 Or(x1,..,xN)）和至多一个为真（断言 Not(And( xi,xj)) 对于所有 i,j)。我也知道other ways 可以手动表达 1-out-of-N 和 K-out-of-N 约束。但是我的印象是，当求解器内置支持此约束时，它有时会比手动表达更有效。

Answer 1

是的，Z3Py 对此具有内置支持。有一个未记录的 API，在 Z3Py 文档中没有提到：使用PbEq。特别是表达式

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

如果将 N 个布尔变量中的 K 个设置为 true，则

将为 true。有some reports 表示这种编码会比手动表达约束的简单方式更快。

要表达 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()