Z3:寻找所有令人满意的模型

内容来源于 Stack Overflow,并遵循CC BY-SA 3.0许可协议进行翻译与使用

  • 回答 (1)
  • 关注 (0)
  • 查看 (23)

我试图检索所有可能的模型,一些一阶理论使用Z3,一个SMT的解决方案开发的微软研究。下面是一个最小的工作示例:

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

在这个命题中,有两个令人满意的任务:f->truef->false...。由于Z3(和SMT求解器一般)只会试图找到一个令人满意的模型,所以不可能直接找到所有的解决方案。这里我找到了一个有用的命令(next-sat),但最新版本的Z3似乎不再支持这一点。

提问于
用户回答回答于

实现这一目标的一种方法是使用其中一个API以及模型生成能力。然后,可以使用从一个可满足性检查生成的模型添加约束,以防止以前的模型值用于后续的可满足性检查,直到没有更令人满意的分配。当然,必须使用有限排序(或者有一些约束来确保这一点),但是如果不想找到所有可能的模型(即,在生成一堆之后停止),也可以将其与无穷排序一起使用

下面是一个使用z3py的示例(链接到z3py脚本)

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

可以工作(例如,ab在这里)。的所有整数赋值。ab(之间)120)令人满意a >= 2b...。例如,如果我们限制ab夹在15相反,输出是:

[b = 1, a = 2]
[b = 2, a = 4]
[b = 1, a = 3]
[b = 2, a = 5]
[b = 1, a = 4]
[b = 1, a = 5]

扫码关注云+社区