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()

但这输出的结果对我来说似乎是胡言乱语。我怎样才能解决这个问题？在哪里可以找到将planning问题编码为SAT的良好资源？我已经看到了STRIPS形式主义，但是我不清楚如何将前后条件编码为逻辑道具。我认为这很隐含，但是我对此没有多大的运气，而且似乎该技术依赖于在模型中满足先决条件后从效果/后置条件生成的新约束。似乎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可能难以处理。但是对于经典的块/计划问题，您不需要那种精美的编码。

希望这可以让您入门！