2005 Fiscal Year Annual Research Report
補題の活用による高速SATプランニングシステムの構築
| Project/Area Number |
16700136
|
|---|
| Research Institution | University of Yamanashi |
|---|
Principal Investigator |
鍋島 英知 山梨大学, 大学院・医学工学総合研究部, 助手 (10334848)
|
|---|
| Keywords | 充足可能性問題 / プランニング / 補題の再利用 |
|---|
| Research Abstract |
本年度は,これまでに提案してきた補題再利用手法を一般化し,補題を再利用可能な条件を明らかにした.すなわち,任意のSAT問題P,Qに対し,P中のすべての非単位節をQが含むならば,Pを解く際に生成された補題を,Qを解く際に再利用可能であることを証明した.
SATプランニングにおいては,プランニング問題をSAT問題に変換する様々な符号化手法が提案されているが,我々はGraphplanベースの符号化だけでなく,アクションベースの符号化に対しても補題が再利用できることを証明した.このアクションベースの符号化は,International Planning Competition (IPC) 2004のoptimal deterministic planning部門において優勝したプランナSATPLAN04が採用する符号化手法であり,様々な種類のプランニング問題に対して安定した性能を示している.
我々は,アクションベースの符号化と最新のSATソルバMiniSAT(2004年のSAT Competitionで優勝)を組み込んだプランナを実装し,IPC 2004において使用されたベンチマーク問題に対しSATPLAN04との比較実験を行った.その結果,(1)補題再利用によってプランニング速度が約2倍改善すること,また(2)補題再利用とMiniSATを組み合わせることにより,2004年の最速のソルバSATPLAN04よりも約4倍高速であることを実証した.
この成果は,2006年6月に開催されるプランニングとスケジューリングに関する国際会議ICAPS(International Conference on Automated Planning & Scheduling)2006において発表予定である.
|
