| 研究概要 |
SATプランニングの高速化のため,本年度はSAT問題を解く過程で生成される補題のよりよい再利用方法に関して研究を行った.一般的にSATプランニングでは,プランニング問題を解く過程で複数のSAT問題P1,P2,P3,【triple bond】を生成する.これらのSAT問題を高速に解くために,我々は,多くの最新のSATソルバがSAT問題を解く過程で生成する補題に着目し,これを再利用する手法を考案した.世界最速のSATソルバの1つであるMoskewiczらによるChaffは,SAT問題を解く際にconflict clausesと呼ばれる補題を生成する.我々は,2つのSAT問題PiとPi+1が,単位節を除いてPi⊆Pi+1の関係にある場合,Piから生成されたconflict clausesをPi+1を解く際にそのまま再利用できることを証明した.また,我々のこの補題再利用法は,SATプランニングだけでなく,SAT問題をベースとした他分野のアルゴリズム(例えば制約充足問題など)にも適用可能であることを示した.
|
