Z3：找到所有满意的模型

Question

我正在尝试使用 Z3（Microsoft Research 开发的 SMT 求解器）检索某些一阶理论的所有可能模型。这是一个最小的工作示例：

(declare-const f Bool)
(assert (or (= f true) (= f false)))

在这个命题案例中，有两个令人满意的分配：f->true 和 f->false。因为 Z3（以及一般的 SMT 求解器）只会尝试找到一个令人满意的模型，所以不可能直接找到所有解决方案。 Here 找到了一个好用的命令，叫(next-sat)，不过好像最新版的Z3已经不支持了。这对我来说有点不幸，总的来说我认为该命令非常有用。还有其他方法吗？

Answer 1

实现此目的的一种方法是使用其中一个 API 以及模型生成功能。然后，您可以使用从一个可满足性检查生成的模型来添加约束，以防止以前的模型值被用于后续可满足性检查，直到没有更多令人满意的分配。当然，您必须使用有限排序（或有一些约束来确保这一点），但如果您不想找到所有可能的模型（即，在生成一堆后停止），您也可以将其与无限排序一起使用.

这是一个使用 z3py 的示例（链接到 z3py 脚本：http://rise4fun.com/Z3Py/a6MC）：

a = Int('a')
b = Int('b')

s = Solver()
s.add(1 <= a)
s.add(a <= 20)
s.add(1 <= b)
s.add(b <= 20)
s.add(a >= 2*b)

while s.check() == sat:
  print s.model()
  s.add(Or(a != s.model()[a], b != s.model()[b])) # prevent next model from using the same assignment as a previous model

一般来说，使用所有涉及的常量的析取应该可以工作（例如，a 和 b 这里）。这将枚举满足a >= 2b 的a 和b（在1 和20 之间）的所有整数赋值。例如，如果我们将a 和b 限制在1 和5 之间，则输出为：

[b = 1, a = 2]
[b = 2, a = 4]
[b = 1, a = 3]
[b = 2, a = 5]
[b = 1, a = 4]
[b = 1, a = 5]

Answer 2

基于 Taylors 答案的更通用的解决方案是使用

while s.check() == z3.sat:  
    solution = "False"
    m = s.model()
    for i in m:
        solution = f"Or(({i} != {m[i]}), {solution})"
    f2 = eval(solution)
    s.add(f2)

这允许两个以上的变量。