| 研究概要 |
SATプランニングの高速化のため,本年度は次の特に2点に関して研究を行った:(1)SATソルバの投機的実行による高速化,および,(2)補題の再利用によるSATソルバの高速化である.SATプランニングにおいては,充足可能なSAT問題が発見されるまで,複数のSAT問題P_1,P_2,P_3,...,P_nが生成される.ここでP_1,...,P_<n-1>は充足不可能,P_nは充足可能である.
前者の研究(1)は,各SAT問題P_iが独立して生成可能であることに着目し,P_iの充足可能性にかかわらず,P_<i+1>についても並行して解く手法である.SATプランニングでは一般的に,充足可能なSAT問題の直前の問題(P_<n-1>)の充足不可能性の証明に多大な時間を消費する.これは後一歩で目標条件を達成可能であることの証明が困難であるためと考えられる.我々の手法は,そのようなSAT問題の充足不可能性のための証明時間を,多くの場合において避けることができる.
後者の研究(2)は,SATプランニングにおいて生成されるSAT問題が特有の性質を持っことに着目し,SAT問題P_iを解く過程において生成された補題をP_<i+1>を解く際に利用し高速化を図る手法である.一般的に,あるSAT問題Qから生成された補題は,別のSAT問題Rに対して適用することはできない.しかしSATプランニングにおいて生成される各SAT問題は,単位節を除いて包含関係(P_i ⊆P_<i+1>)にあるという特徴がある.我々は,SATプランニングにおいては,補題を再利用することが可能であるということを証明し,平均して約1.6倍の高速化が可能であることを示した.
|
