z3 规划问题和积木世界
z3 planning problems and blocks world
我对使用 z3 解决规划问题很感兴趣,但我很难找到示例。例如,我真的很想在 z3 中找到 Sussman anomaly/blocks 世界的示例,但一直找不到任何东西。我的尝试看起来像
#!/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 形式主义,但我不清楚如何将 pre+post 条件编码为逻辑道具。我会认为这是暗示,但我对此运气不佳,而且似乎这种技术依赖于模型中满足先决条件后从 effects/post-conditions 生成的新约束。如果没有明确编程的 post 条件,z3 似乎无法做到这一点。
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 来说太难处理了。但是对于经典的 block/planning 问题,您不需要那种花哨的编码。
希望这能让你入门!
我对使用 z3 解决规划问题很感兴趣,但我很难找到示例。例如,我真的很想在 z3 中找到 Sussman anomaly/blocks 世界的示例,但一直找不到任何东西。我的尝试看起来像
#!/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 形式主义,但我不清楚如何将 pre+post 条件编码为逻辑道具。我会认为这是暗示,但我对此运气不佳,而且似乎这种技术依赖于模型中满足先决条件后从 effects/post-conditions 生成的新约束。如果没有明确编程的 post 条件,z3 似乎无法做到这一点。
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 来说太难处理了。但是对于经典的 block/planning 问题,您不需要那种花哨的编码。
希望这能让你入门!