mar*_*oid 24 theorem-proving smt z3
我正在尝试使用微软研究院开发的SMT求解器Z3检索所有可能的一阶理论模型.这是一个最小的工作示例:
(declare-const f Bool)
(assert (or (= f true) (= f false)))
在这个命题案例中,有两个令人满意的任务:f->true和f->false.因为Z3(以及一般的SMT求解器)只会尝试找到一个令人满意的模型,所以找不到所有解决方案是不可能的.在这里,我发现了一个有用的命令(next-sat),但似乎最新版本的Z3不再支持这一点.这对我来说有点不幸,总的来说我觉得这个命令非常有用.还有另一种方法吗？
Tay*_*son 27
实现此目的的一种方法是使用其中一个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]