Z3:找到所有令人满意的模型
Z3:找到所有令人满意的模型
提问于 2012-11-15 18:18:07
我正在尝试使用微软研究院开发的Z3来检索一些一阶理论的所有可能的模型。下面是一个最小的工作示例：
(declare-const f Bool)
(assert (or (= f true) (= f false)))在这个命题例子中，有两个令人满意的赋值：f->true和f->false。因为Z3 (和一般的SMT求解器)只会尝试找到一个令人满意的模型，所以不可能直接找到所有的解决方案。Here我发现了一个名为(next-sat)的有用命令，但最新版本的Z3似乎不再支持此命令。这对我来说有点不幸，总的来说，我认为这个命令非常有用。有没有其他方法可以做到这一点？
回答 2
Stack Overflow用户
回答已采纳
发布于 2012-11-15 21:51:10
实现这一点的一种方法是使用其中一种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]Stack Overflow用户
发布于 2022-01-13 09:33:27
基于Taylor的更一般的解决方案是使用
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)这允许两个以上的变量。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/13395391
复制相关文章
相似问题