我正在尝试使用 Z3(Microsoft Research 开发的 SMT 求解器)检索某些一阶理论的所有可能模型。这是一个最小的工作示例:
(declare-const f Bool)
(assert (or (= f true) (= f false)))
在这个命题案例中，有两个令人满意的赋值:f->true 和 f->false。由于 Z3(以及一般的 SMT 求解器)只会尝试找到一种令人满意的模型，因此不可能直接找到所有解。 Here我发现了一个有用的命令，叫做(next-sat)，但是最新版本的Z3似乎不再支持这个。这对我来说有点不幸，总的来说我认为这个命令非常有用。还有其他方法可以做到这一点吗？
最佳答案
实现此目的的一种方法是使用其中一个 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 。例如，如果我们限制 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]
关于Z3:找到所有满意的模型，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/13395391/