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

Question

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

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

Answer 1

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

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

如果 N 个布尔变量中的 K 个恰好设置为 true，则为 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()