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

Posted 2023-02-25

【中文标题】Z3Py 中的 K-out-of-N 约束

【英文标题】：K-out-of-N constraint in Z3Py

【发布时间】：2017-08-22 06:10:46

【问题描述】：

我正在使用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 约束。但是我的印象是，当求解器内置支持此约束时，它有时会比手动表达更有效。

【参考方案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()

【讨论】：

有趣。有什么方法可以通过 smt-lib 接口访问PbEq 吗？ （也许是通过战术，或者其他 z3 魔法？）

@LeventErkok，我不知道。好问题！内部 C/C++ API 是 Z3_mk_pbeq()。

在这里提交了一张票，看看 z3 人是否能想出办法：github.com/Z3Prover/z3/issues/960

SMT-LIB 语法是 ((_ at-most k) xyzuv), ((_ at-least k) xyzuv), ((_ pbge c1 c2 c3 c4 c5 k) xyzuv), ((_pble c1 c2 c3 c4 c5 k) xyzuv), ((_pbeq c1 c2 c3 c4 c5 k) xyzuv)，如果只使用位向量和PB约束，则设置逻辑为QF_FD（无量词有限域）。然后它使用 SAT 求解器。