問題タブ [planning]

計画の問題を解決するために z3 を使用することに興味がありますが、例を見つけるのに苦労しています。たとえば、私は本当に z3 で Sussman の異常/ブロックの世界の例を見つけたいと思っていますが、何も見つけることができませんでした。私の試みは次のようになります

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

PDDL を使用して Pacman の問題を解決しようとしています。私がする必要がある主なことは、functionsまたはを使用せずに電力持続時間をソフトコーディングすることfluentsです。エラーは返されませんが、どういうわけか inits のように感じPowerlose(n2, n0)ます。効果を初期化Powerlose(n2, n0)または変更Powerloseすることはありません。しかし、それが与える初期値cは ですn2。では、何が問題なのですか？前もって感謝します。

このリンクから問題とドメインを確認できます: http://editor.planning.domains/#edit_session=bD5G0tIIl1vyWDf

existsドメイン ファイルの 34 行目の代わりにステートメントを使用しようとしましPowerlose(cPlus1, c)たが、機能しません。それはまだで初期化cしn2ます。私はとても混乱しています。ここに私のドメインファイルがあります:

問題のファイル:

それが返すプラン: (move a1 b1 n0 n2 n2) (move b1 b2 n0 n2 n2) (move b2 b3 n2 n2 n2) (move b3 b4 n2 n1 n2) (move b4 a4 n1 n0 n2) (move a4 a5 n0) n2 n2)

正しい計画: (move a1 b1) (move b1 b2) (move b2 b3) (move b3 b4) (move b4 b5) (move b5 b4) (move b4 a4) (move a4 a5)