38

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

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

在这个命题情况下，有两个令人满意的分配：f->true和f->false。因为 Z3（以及一般的 SMT 求解器）只会尝试找到一个令人满意的模型，所以不可能直接找到所有解决方案。在这里我找到了一个有用的命令叫做(next-sat)，但是Z3的最新版本似乎不再支持这个。这对我来说有点不幸，总的来说我认为该命令非常有用。还有另一种方法吗？

4

2 回答 2

39

实现此目的的一种方法是使用其中一个 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和b（在1和之间20）的整数赋值a >= 2b。例如，如果我们限制aandb位于 and 之间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]
于 2012-11-15T13:51:10.107 回答
0

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

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)

这允许两个以上的变量。

于 2022-01-13T09:33:27.470 回答