Planning with Specialized SAT Solvers(Rintanen; 2011)

Jussi Rintanenhttps://users.ics.aalto.fi/rintanen/jussi/氏のPlanning as SAThttps://users.ics.aalto.fi/rintanen/satplan.htmlに関連する一連の著作についてのメモである。

この論文Planning with Specialized SAT Solvershttps://users.ics.aalto.fi/rintanen/papers/Rintanen11aaai.pdfは古典的プランニング問題をSATに帰着し、ソルバを使ってSAT問題の解を計算し、その解から元のプランニング問題の解を抽出する、という枠組みの中で、汎用SATソルバではなく、プランニング問題のヒューリスティックを入れたソルバを構築することで既存の探索ベースのソルバを上回る性能を得たというものである。

汎用SATソルバではChaffなどで採用されていたVSIDSヒューリスティックスを使ったCDCL探索が主流である。 一方で、古典的プランニング問題の知識として、アクションの列を決定すると状態の遷移は一意に決定される、というものがある。 また、命題変数の中にはゴール命題という特に充足に対する要求が強い命題があり、これらの命題を充足するようなアクションを実行するような変数割当てはより有望であるといえる。 以上の2つの知識をSATソルバの変数選択に取り込むための仕組みを提案している。 (具体的な手法はFigure.1 Computation of supports for (sub)goalsを参照)

実験結果を見ると、充足解を計算する探索ベースのプランナのLAMA(IPC2008優勝)やYAHSPという当時state-of-the-artなプランナに対して、Mpという提案手法を採用したSATベースプランナがかなりよい性能を示していることがわかる。

Rintanenさんは一連のSATベースプランナの研究の中で、多くの手法を提案しており、これらの手法を取り込んだプランナがMpなのであるが、そのうちこの論文で提案しているPlanning問題のための独自ヒューリスティックを使わず、汎用SATソルバの変数選択ヒューリスティックVSIDSを採用したプランナMはLAMA, YAHSPにout-performされていることから、この論文で提案されている変数選択ヒューリスティックのプランニング問題への有効性が確認できる。

https://users.ics.aalto.fi/rintanen/satplan.htmlにある関連した面白い話としては、グラフアルゴリズムをプランニング問題に帰着することで作られた、より"プランニング色"の低い問題に関してはMがLAMA, YAHSP, Mpをout-performしているというものがある。 これはIPCプランニング問題のある種の"偏り"を示しているものと見ることができ、探索ベースのプランナやIPC問題に特化したプランナのチューニングの"脆さ"を示しているようで興味深い。