z3规划问题与积木世界

Question

我对使用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？我见过形式主义，但我不清楚如何将pre+post条件编码到逻辑道具中。我会认为这意味着，但我没有多少运气，而且这种技术似乎依赖于在模型中满足先决条件之后，从效果/后条件中产生的新的约束。如果不对post条件进行显式编程，z3似乎无法做到这一点。

Answer 1

这样的问题当然可以通过Z3解决，也可以通过任何SMT求解者来解决。但是，由于明显的原因，您将无法获得专用系统的优秀功能。编码可能更冗长，正如您所发现的，解释模型可能相当棘手。

我认为您的编码是一个很好的开始，但是通过使Block成为枚举排序并显式声明系统中的块，您会得到更好的服务。这将使编码更接近于规划系统的典型编码方式，也将有助于解释模型本身。

基于此，下面是我如何编写您的问题的代码，假设我们生活在一个名为A、B和C的宇宙中

from z3 import *

Block, (A, B, C) = EnumSort('Block', ('A', 'B', 'C'))
On    = Function ("On",    Block, Block, BoolSort())
Above = Function ("Above", Block, Block, BoolSort())

objects = [A, B, C]

solver = Solver()
solver.add(And(On(A, B), On(B, C)))

x, y, z = Consts ("x y z", Block)
solver.add(ForAll([x, y], Implies(On(x, y), Above(x, y))))
solver.add(ForAll([x, y, z], Implies(And(On(x, z), Above(z, y)), Above(x, y))))
solver.add(ForAll([x], Not(On(x, x))))
solver.add(ForAll([x], Not(Above(x, x))))

if solver.check() == sat:
    print "sat"
    m = solver.model()
    for i in objects:
        for j in objects:
            if m.evaluate(On(i, j)):
                print "On(%s, %s)" % (i, j)
            if m.evaluate(Above(i, j)):
                print "Above(%s, %s)" % (i, j)
else:
    print "unsat"

(请注意，我必须调整您的P2，这看起来不太对。我还添加了两个公理，表示On和Above是反自反的。但是你可以修改和使用不同的公理，看看你得到了什么样的模型。)

对于这个输入，z3说：

sat
On(A, B)
Above(A, B)
Above(A, C)
On(B, C)
Above(B, C)

这是一个有效的场景，满足所有的约束条件。

我应该指出，SMT求解者通常不擅长量化推理。但是，通过保持宇宙的有限(和小！)，它们可以很好地处理任意数量的这样的公理。如果您从无限域(如Int、Real等)引入对象，那么事情会变得更有趣，而且可能对z3来说太难处理了。但是，对于经典的块/规划问题，您不应该需要那种花哨的编码。

希望这能让你开始！