SATアプローチに基づく高速プランニングシステムの構築

SATプランニングの高速化のため,本年度はSAT問題を解く過程で生成される補題のよりよい再利用方法に関して研究を行った.KautzとSelmanによるSATプランナBlackboxは,プランニング問題を解く過程で複数のSAT問題P1,P2,P3,…を生成する.Blackboxは,これらのSAT問題を世界最速のSATソルバの1つであるMoskewiczらによるChaffにより解く.ここで我々は,ChaffがPiを解く際に生成する補題がPi+1を解くときにも再利用できることを証明し,補題を再利用する新しいプランニングアルゴリズムLRP(Lemma-Reusing Planning)を提案した.LRPはBlackboxと比較して,平均して約1.6倍高速にプランニング問題を解くことができる.しかし一般にChaffが生成する補題は莫大な数になる.補題は,無駄な探索の枝刈りを行うために生成された失敗の記録であるが,補題が適用可能かどうか調べるためには,その莫大な数の失敗の記録を検索する必要がある.そこで,無駄な探索空間を大きく枝刈りする補題のみを残し,あまり効果を持たない補題を削除することで,さらなるプランニング速度の向上が期待できる.また補題の数が膨大であるため,「有用かどうか」の判断は高速に行う必要がある.そこで我々は,補題再利用の判断基準をいくつかのヒューリスティクスに基づき設計し,実験を行った.その結果,SAT問題の解探索空間の上位において使用される補題のみを再利用することで,Blackboxと比較して平均して約1.8倍の高速化が可能であることを示した.特に補題が莫大に生成される問題では顕著な効果を示している.

SATプランニングの高速化のため,本年度はSAT問題を解く過程で生成される補題のよりよい再利用方法に関して研究を行った.KautzとSelmanによるSATプランナBlackboxは,プランニング問題を解く過程で複数のSAT問題P1,P2,P3,…を生成する.Blackboxは,これらのSAT問題を世界最速のSATソルバの1つであるMoskewiczらによるChaffにより解く.ここで我々は,ChaffがPiを解く際に生成する補題がPi+1を解くときにも再利用できることを証明し,補題を再利用する新しいプランニングアルゴリズムLRP(Lemma-Reusing Planning)を提案した.LRPはBlackboxと比較して,平均して約1.6倍高速にプランニング問題を解くことができる.しかし一般にChaffが生成する補題は莫大な数になる.補題は,無駄な探索の枝刈りを行うために生成された失敗の記録であるが,補題が適用可能かどうか調べるためには,その莫大な数の失敗の記録を検索する必要がある.そこで,無駄な探索空間を大きく枝刈りする補題のみを残し,あまり効果を持たない補題を削除することで,さらなるプランニング速度の向上が期待できる.また補題の数が膨大であるため,「有用かどうか」の判断は高速に行う必要がある.そこで我々は,補題再利用の判断基準をいくつかのヒューリスティクスに基づき設計し,実験を行った.その結果,SAT問題の解探索空間の上位において使用される補題のみを再利用することで,Blackboxと比較して平均して約1.8倍の高速化が可能であることを示した.特に補題が莫大に生成される問題では顕著な効果を示している.