専攻名
研究指導名 氏 名
指 導
教 員 印
研 究 題 目
2011 年 1 月提出 学籍番号
修 士 論 文 概 要 書
CD 5109B083 – 3
情報理工学
並列知識情報処理
村岡 崇章 上田 和紀
補題再利用を用いた並列 SAT プランナの設計と実装 1 はじめに
プランニング問題は，初期状態・目標状態・アクション の集合が与えられた時，初期状態から目標状態へ変化さ せるまでのアクションの順序を求める問題である．この ようなプランニング問題はNP完全であるため多項式時 間で解くことはできない．しかし，プランニングは自律 型ロボットや無人航空機の経路設定など多くの実用的な 問題に適用可能であり，プランニングを高速に解く意義 は大きい．また近年プランニングを高速に解く手法の一 つとして，並列化の研究も行われるようになったが，こ れらの研究は始められて日が浅く，並列プランナはごく わずかしか存在していないなど，並列化による高速化の 余地はまだ多く残っている．
本研究ではSATプランニングを用いたSATプランナ，
COPLANをベースに，補題を再利用する手法 (Lemma
Reusing Plannig:LRP)と，高速な並列SATソルバc-satを 使うことによる高速化の両方の手法を用いた並列SATプ ランナの設計と実装を行った．
2 充足可能性問題： SAT
充足可能性問題SAT問題とはある論理式が与えられた とき，その論理式がしんとなる変数割り当てが存在する かを求める問題である．SAT問題は以下のような形式で 表現される．この論理式は，a=T，b =F，c=F，d =T とすることで充足可能(SATISFIABLE)となる．
論理式=(a∨ ¬d)∧(¬a∨ ¬b∨c)∧(b∨ ¬c∨d) ソフトウェアであるSATソルバの多くはCDCLアルゴ リズムに基づいており，変数選択，推論，衝突解析，バッ クトラックの４つのフェイズを繰り返し，解を探索する．
解の探索域は巨大だが，衝突解析フェーズで生成される，
特定の探索域に解が存在しないことを示す補題(Lemma) を用いることにより解の探索の高速化が得られる．
2.1 c-sat
c-sat[2]はCDCLアルゴリズムを用いたSATソルバを MPIで並列に実行し，lemmaの共有と探索域の動的分割 によって探索域の大幅な剪定と高速な動作を実現した並 列SATソルバである．SATソルバでは並列化における 通信がボトルネックとなりやすいため，c-satでは冗長な
lemmaは共有したいといったルールの適用等によって通
信料の削減を図っている．また，通信による解探索効率
低下を防ぐため，lemmaの共有には専用のマスタを用い たマスタワーカ構造を用いている．
3 COPLAN
COPLAN[3]はIPC2008(International Planningu Compe- tition)に出場した，SATプランニングアルゴリズムを用 いたプランナである．COPLANは探索空間を削るために，
プランニンググラフと呼ばれる有向付き探索グラフ作成 してからCNFに変換し，それをSATソルバRSATで解 くアルゴリズムになっている．
以下にCOPLANのアルゴリズムを示す．
1. プラン長を１とし，プランニンググラフを作成する．
2. プランニンググラフをCNFに変換する．
3. CNFをRSATで解く．SATISFIABLEならば，この プラン長にプランが存在するため，COPLANを終 了する．
4. プラン長を１大きくして，手順２からやり直す．
4 補題再利用
この章では補題再利用(Lemma Reusing Planning:LRP)[1]
について述べる．一般的にあるSAT問題から生成された
lemmaは別のSAT問題において利用することはできな
い．しかし，LRPは特定のアルゴリズム，CDCLで生成
されたlemmaが同じプランニング問題から生成された別
のSAT問題においても利用導出可能であることを用いて，
SATプランニングの解探索の高速化を図るアルゴリズム である．
以下の図1にLRPの概念を示す．
図1: LRP
5 C2P の設計と実装
C2PはCOPLANをベースに並列化したプランナであ
る．下の図2に流れを示す．C2Pはプラン長をnとした プランニンググラフを作成後，CNFに変換する．それを c-satで解く．SATISFIABLEならば，終了する．UNSAT ならば，プラン長を１追加し，プランニンググラフを作 成，CNFに変換する．それをc-satで解く際に，プラン長 nで生成されたlemmaを保持したままc-satで解く．これ を繰り返す．
図2: C2Pの動作図
6 評価実験
今回の実験は独立行政法人産業技術総合研究所が配備 管理している検証クラスタさつきを使用した．以下に実 験環境を示す．
実験環境 CPU：Quad Core Intel Xeon 2.93GHz×16 Memory：1TB
Middle ware：Mpich2 version 1.2.1 gcc：4.3.2
今回の実験はCOPLNA，C2P，LRPを用いたC2Pそれ ぞれに31PEを用いて行った．また，本実験ではIPCで 使用した問題の中からCOPLANが１秒かかった問題を使 用して，全実行時間と速度向上比を計算している．実験 結果を表1，図3に示す．
表1: COPLANと，C2P，C2P-lrpの性能評価 COPLAN C2P C2P-LRP
alltime 6674.23 371.27 4121.28
speedup 1 25.44 24.82
図3:実験結果
実験結果，表1からC2Pは平均向上比は約25倍，LRP を用いると約25倍になった．また，LRPを用いる場と 用いない場合ではX倍の向上比になった．実験結果から
c-satを入れることによる効果はかなりの効果がでたと思
われる．しかし，図3LRPを用いた際はそれほどの効果 が出なかった．これはlemmaがあるせいで，SATの解の 探索の邪魔をしているものと思われる．元々lemmaは冗 長なので，探索域の削減には効果はあるが，探索の邪魔 をしてしまうことがあるためと思われる．
7 まとめと今後の課題
本研究ではLRPを用いた並列SATプランナを実装し，
31PEsで問題を解かせた．結果として，c-satを用いたC2P はCOPLANに比べて平均X倍の速度向上に成功し，LRP
を用いたC2P-LRPは速度向上としては変わらない結果に
なった．以下に今後の課題を挙げる．
• 保持するlemma量の変更
今回のLRPは一つ前のレベルのlemmaのみを保持 していた．しかし，現在のレベルより前のlemmaは すべて再利用可能なので，lemma量の変更をするこ とにより，より高速な解の探索を行う．
• 複数のレベルの同時探索
今回のC2Pでは一つのレベルをc-satで探索してい たが，同時に複数のレベルを探索することによって，
早くプランが存在するレベルに達成することができ るため，更なる高速化が期待できる．
• lemma masterの導入
上記の複数のレベルの同時探索の際に，lemmaを違 うレベルの解いているc-satに受け渡すlemma master を導入する．そうすることによって，様々なlemma を受け取ることができ，更なる高速化が見込まれる．
参考文献
[1] Nabeshima,H., Soh,T.,Inoue, K.,: Lemam reusing for SAT based planning and scheduling, In Proc.ICAPS, 2006
[2] ohmura，K.,Ueda，K.,c-sat: A Parallel SAT Solver for Clus- ters,In Proc.SAT2009,pp. 239-253,2009.
[3] Robinson, N., Gretton, C., Pham, D.N.: Co-plan: Com- bining SAT-based planning with forward-search. In:
Proc. IPC-6 (2008)
[4] Jussi Rintanen: Planning as satisfiability: parallel plans and algorithms for plan search, Artificial Intelligence Volume 170, September 2006, pp. 1031- 1080.
