如何使用 z3py 设置“最多 n 次”等要求？答案

【问题标题】：How to set requirements like "at most n times" by using z3py?如何使用 z3py 设置“最多 n 次”等要求？
【发布时间】：2020-09-12 20:33:43
【问题描述】：

我是 python 新手，也是 z3 新手。我正在尝试通过 z3py 解决一些 SMT 问题。现在我需要设置一个限制：array1(1,8) 至少有 5 个零。但是我遇到了一些错误。

al1,al2,al3,al4,al5,al6,al7,al8=Ints('al1 al2 al3 al4 al5 al6 al7 al8')

这是我声明的，当我想使用al1=If(be1*wi1,1,0)时，会出现一个错误，说Z3Exception: Value cannot be converted into a Z3 Boolean value 或Z3Exception: Symbolic expressions cannot be cast to concrete Boolean values

我想知道如何计算这些元素中有多少个零？我不确定这个声明是否可以更改...我只是从示例中复制了这部分.. p>

【问题讨论】：

请发布一个最小但完整的示例，以便重现您的问题。关于您的目标（最多 n 次）：您可以使用存在（不存在数组具有特定值的五个不同索引）；如果数组的长度是静态已知的，那么存在可以被析取替换；根据数组中的值，可以选择使用总和/乘积的解决方案。

标签： python z3 z3py

【解决方案1】：

最好发布您的完整代码，以便人们可以看到并评论您的具体尝试。

在任何一种情况下，要表达这种至少/最多种类的约束，您应该使用所谓的“伪布尔”约束。例如，要说这些元素中至少有 5 个为 0，您可以说：

from z3 import *

al1,al2,al3,al4,al5,al6,al7,al8 = Ints('al1 al2 al3 al4 al5 al6 al7 al8')

s = Solver()

s.add(AtLeast(al1 == 0, al2 == 0, al3 == 0, al4 == 0, al5 == 0, al6 == 0, al7 == 0, al8 == 0, 5))

print(s.check())
print(s.model())

当我运行它时，我得到：

sat
[al8 = 1,
 al7 = 1,
 al6 = 1,
 al5 = 0,
 al4 = 0,
 al3 = 0,
 al2 = 0,
 al1 = 0]

如您所见，其中 5 个变量为 0。（显然这不是唯一可能的模型，而是 z3 为您找到的模型。您显然可以添加其他约束。）

有关伪布尔约束的详细信息，请参见此处：https://z3prover.github.io/api/html/namespacez3py.html#a8575bdeb9d1b8feac119aa162b5acfa6

您要查看的函数称为：AtMost、AtLeast、PbLe、PbGe 和 PbEq。

【讨论】：