我正在尝试使用微软研究院开发的Z3来检索一些一阶理论的所有可能的模型。下面是一个最小的工作示例:
(declare-const f Bool)
(assert (or (= f true) (= f false)))
在这个命题例子中,有两个令人满意的赋值:f->true
和f->false
。因为Z3 (和一般的SMT求解器)只会尝试找到一个令人满意的模型,所以不可能直接找到所有的解决方案。Here我发现了一个名为(next-sat)
的有用命令,但最新版本的Z3似乎不再支持此命令。这对我来说有点不幸,总的来说,我认为这个命令非常有用。有没有其他方法可以做到这一点?
发布于 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]
发布于 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)
这允许两个以上的变量。
https://stackoverflow.com/questions/13395391
复制相似问题