我对使用z3解决规划问题感兴趣,但我很难找到例子。例如,我真的很想在z3中找到一个Sussman异常/块世界的例子,但没有找到任何东西。我的尝试看起来像
#!/usr/bin/env python
from z3 import *
blk = DeclareSort ("Block")
On = Function ("On", blk , blk, BoolSort () )
Above = Function ("Above", blk , blk, BoolSort () )
a, b, c, x, y, z = Consts ("a b c x y z", blk )
P0 = And(On(a,b), On(b,c))
P1 = ForAll([x, y], Implies(On(x,y), Above(x,y)))
P2 = ForAll([x, y, z], Implies(And(On(x,y), Above(z, y)), Above(x,y)))
solver = Solver()
solver.add(And(P0,P1,P2))
print solver.check()
print solver.model()
但这输出的东西在我看来像胡言乱语。我怎样才能解决这个问题?我在哪里可以找到一个好的资源来编码计划SAT问题?我见过形式主义,但我不清楚如何将前置+后置条件编码为逻辑支柱。我认为这可能意味着什么,但我在这方面运气不太好,而且这项技术似乎依赖于在模型中满足前提条件后,从效果/后条件生成的新约束。如果没有明确编程的post条件,z3似乎无法做到这一点
这些问题肯定可以通过Z3和任何SMT解决方案解决。但是,由于明显的原因,您将无法获得专用系统的良好功能。编码可能更加冗长,正如您所发现的,解释模型可能相当棘手
我认为您的编码是一个很好的开始,但是最好将
Block
作为枚举排序并显式声明系统中的块。这将使编码更接近规划系统通常的编码方式,并有助于解释模型本身基于此,假设我们生活在一个有三个块的宇宙中,分别命名为
A
、B
和C
,我将开始编写您的问题代码:(请注意,我不得不调整你的
P2
,这看起来不太正确。我还添加了两个公理,说On
和Above
是不可伸缩的。但是你可以修改和使用不同的公理,看看你得到了什么样的模型。)对于该输入,z3表示:
这是一个有效的场景,满足所有约束条件
我应该注意到,SMT求解者通常不擅长量化推理。但是通过保持宇宙的有限性(和小性!),他们可以很好地处理任何数量的这样的公理。如果从无限域中引入对象,如
Int
、Real
等,事情会变得更有趣,而且可能对z3来说太难处理。但是,对于经典的块/规划问题,您不应该需要那种奇特的编码希望这能让你开始
相关问题 更多 >
编程相关推荐