2009 Fiscal Year Annual Research Report
SATプランニングとスケジューリングの高度化・高速化に関する研究
| Project/Area Number |
19700135
|
|---|
| Research Institution | University of Yamanashi |
|---|
Principal Investigator |
鍋島 英知 University of Yamanashi, 大学院・医学工学総合研究部, 准教授 (10334848)
|
|---|
| Keywords | 充足可能性問題 / プランニング / スケジューリング / 分散協調 |
|---|
| Research Abstract |
本年度は,スケジューリング問題への取り組みとして,これまで未解決であったジョブショップ・スケジューリング問題6問に対して,順序符号化法と大規模計算クラスタを利用することで,2問の最適値決定と,4問の下界更新,1問の上界更新に成功した.最適値決定に成功した2つの問題は20年以上も未解決であった問題である.また2SPP (two-dimensional strip packing problem)における38問のベンチマーク問題に対しても,順序符号化法に基づくSAT変換により,1問の未解決問題を含んだ29問の最適値の決定に成功している.
プランニング問題への取り組みでは,数値制約を含むプランニング問題に対して,Hoffmannらの手法を基に,順序符号化法を組み合わせる手法の検討を行った.Hoffmannらの手法は1つの数値を1つの命題に対応づける直接符号化であるが,我々の提案する手法では数値の特定の範囲を1つの命題に対応づける順序符号化法を利用する.実装と評価は今後の課題であるが,これまでの順序符号化法に対する各種の成果より,プランニング問題においても高速化されることが期待できる.
またSATソルバの高速化のために,Ashishにより提案されたシンメトリー情報を利用した多分木探索技術を最新のSATソルバMiniSatに導入したソルバSymMiniを試作した.240問のベンチマーク問題に対する評価実験の結果,シンメトリー情報を利用することで大幅に高速化できることを確認した.その他にも,極小集合被覆を列挙するアルゴリズムをベースに,最新のSATソルバにおける各種の高速化技術の導入することで,CNF/DNF変換を効率的に行う手法を考案した.
|
