趣味ラボ

RintanenさんのPlanningをSATソルバを使って解く一連の論文の2010のもの

Planning-specificなheuristicをSATソルバに入れることで、satソルバの探索を効率的に行うというもので、Rintanen 2011で構築されたプランナM, Mpに取り込まれている技術のうちの一つである。

Conflict Driven Clause Learning(CDCL)に深さ優先探索をさせるように変更したもの(時期的にはChaffの改造だろうか?2010の別のRintanen氏の論文で記述があるそうだ)が当時のプランニング用のSATソルバの最先端だったそうだが、さらに一方踏み込んで、ソルバの変数選択や、値の割当てのヒューリスティックとして、プランニングの知識を入れようとしている。

よく知られたプランニングをモデル化した際のソルバ側の探索ヒューリスティックとしては、命題変数とアクション変数が存在するが、全てのアクション変数の割当が決定すると命題変数の値は一意に定まるため、アクション変数に優先的に(あるいはアクション変数のみに)値を割り当てる、というものがある。このような割当てを実現する方法として(僕が知っているの)は、

この論文では帰着先のモデルとしてSATを利用しているが、どのモデルでも通用するのはソルバを改造(または実装)することである
しかしながら、できれば汎用ソルバをそのまま使って性能が出るに越したことはないと思う
IP(MIP)を使う場合には、探索の際に決定変数になるのは整数制約の付いている変数であることに着目して、関数的に決定される変数が整数変数によって抑えられるように制約を加え、その上で連続変数とすることで割当順序の操作が可能である
CPの場合には、多くのソルバでドメインが小さい変数から決定変数として採用されるという汎用ヒューリスティックが採用されるのでそうなるようにモデルを工夫して設計するか、またはソルバにヒントを与える仕組みがMinizincという中間言語で導入されているのでこれを利用することが考えられる

この論文で提案されている変数選択、値の割当ての際のヒューリスティックは上に挙げたような自明なものよりももう一歩踏み込んだもので、この実現のために、SATソルバにRintanen氏は手を加えているようである。具体的なヒューリスティックとしては、後ろ向き推論のようなことを実現するための仕組みを提案している。

これは * ゴール命題(top-level goal)は最終的に真となる必要がある * するとゴール命題を真とするようなアクションが実行される必要がある * すると今度はそのアクションの前提条件(subgoalと呼んでいる)がその前に真になっている必要がある

というのを繰り返しながら、必要度の高そうな変数から割当てを行うというものである。さらなる工夫として、goalの未割当てであるような深さをプライオリティーとしてプライオリティーキューを構築することで、ゴールに近いんだがまだ真になっていないような命題から割当てを行うような工夫もしている。ここでは、subgoalの必要度の高さをtop-level goalから何回目の展開で現れたsubgoalか、で見積もり、より必要そうなsubgoalから順に割当てを行うような工夫もありうるのではないだろうかと思う。

もう一つ、actionからsubgoalを生成する際に、最初に見つけたものを採用するのではなく、N個ののsubgoalを見つけ、その中から一つ適当に引く、ということをしている。ただし、素朴にこれを行うと、以前に展開した残りがその後の探索の邪魔をすることがあり、N=2よりも大きいと性能が上がらなかったそうである。ここで、time-stampという概念を導入し、展開した残り物がqueueにたくさん入ってきたら展開を打ち切る、ということをすると、最もよい結果が出たそうである。

より具体的なアルゴリズムと性能評価は論文に譲ることとする。

メモ: * Rintanen;2011とExperimental Resultsの様子がだいぶ変わっている。 * IPC1998, 2008のドメインがいくらか追加されている * その結果、この論文ではM > LAMAだったのが2011の論文では逆転している

趣味ラボ

Heuristic Planning with SAT(Rintanen; 2010)

Heuristic Planning with SAT: Beyond Uninformed Depth-First Search(Rintanen; 2010)