計画の問題を解決するために 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にエンコードするための適切なリソースはどこにありますか? 私は STRIPS 形式を見てきましたが、プリ + ポスト条件をロジック プロップにエンコードする方法が不明です。私は含意だと思いますが、これについてはあまり運がありませんでした。この手法は、モデルで前提条件が満たされた後に効果/事後条件から生成される新しい制約に依存しているようです。そして、ポスト条件を明示的にプログラムしないと、z3はこれを行うことができないようです。