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

Question

我对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

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

Answer 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