Z3：寻找所有满足模型

Question

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

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

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

- marczoid

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]

- Taylor T. Johnson

---

此外，请参见此答案：https://dev59.com/f2ct5IYBdhLWcg3wufxb - Taylor T. Johnson

Z3在进行这样的搜索时是否是有状态的？它似乎不必每次都重新开始，因为直觉上来看，所有工作都完全相同，除了最后一步。 - GManNickG

根据我使用的示例，似乎确实是有状态的，因为在找到初始模型后，接下来找到几个模型会更快。以下是一个包含58个模型的特定案例的运行时间列表（以毫秒为单位）： 8942 801 1663 5 599 320 450 2 2 3 1 5 1377 36 5 738 162 105 1639 3 5 16 2041 27 475 953 562 746 45 151 18 4206 3416 9 850 120 3 4 12 615 593 1219 449 154 987 3 10 1365 16 438 792 1686 743 46 5 8 412 126。请注意，第一个模型肯定最耗时，但其他模型的时间更随机（可能取决于问题和求解器的运气）。 - Stanley Bak

是的，只要您使用相同的求解器对象，它就会保留其学习的所有子句。您可以使用push和pop选择性地将学习的子句遗忘到上次推送（唯一删除约束的方法是弹出到先前的推送）。 - Chris Connett

Answer 2

基于泰勒的回答，更普遍的解决方案是使用：

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)

这允许使用超过两个变量。

- Jaypthomer

---

这种解决方案可能非常低效，使用字符串/eval等方式回溯。而且，阻止解决方案的方式也不是最优的。请参见https://dev59.com/f2ct5IYBdhLWcg3wufxb#70656700，以获取更好的方法。 - alias