2008 Fiscal Year Annual Research Report
SATプランニングとスケジューリングの高度化・高速化に関する研究
| Project/Area Number |
19700135
|
|---|
| Research Institution | University of Yamanashi |
|---|
Principal Investigator |
鍋島 英知 University of Yamanashi, 大学院・医学工学総合研究部, 准教授 (10334848)
|
|---|
| Keywords | 充足可能性問題 / プランニング / スケジューリング / 分散協調 |
|---|
| Research Abstract |
本年度は, マルチコア環境向け高速並列SATソルバの試作と分散協調SATシステムのための問題分割手法の改善に取り組んだ.
複数のCPUコアを搭載したPCが普及傾向にあることを踏まえ, 最新の逐次型SATソルバを基にマルチコア環境向け並列SATソルバの試作を行った. 従来のマルチコア環境向けの並列SATソルバの多くは, 複数のSATソルバスレッドを並行して実行し, 学習節の交換等により性能の改善を図っている. 我々は, 単に複数のSATソルバスレッドを並列に実行するのではなく, アルゴリズムの中でも処理時間が最もかかる単位節発見と真偽値伝搬処理の並列化について検討を行った. その結果, 最新の逐次型SATソルバを基に並列化することは細やかな排他処理を必要とするためオーバーヘッドが大きく非常に困難であり, データ構造の抜本的な見直しが必要になることが分かった.
また分散協調SATシステムのための問題分割手法の改善では, 最新のSATソルバにおいては従来型の単純な網羅的問題分割では探索空間が重複し, PCの台数増加とともに性能向上の鈍化が見られることを改善するため, 複数の異なるリテラルに適当な真偽値を割り当て, 適度な規模の部分問題に分割する手法を考案した. 評価実験の結果, 従来手法よりも効率良く求解可能になることを確認した. 今後は約100台程度のPC群で動作させ, より詳細な評価を実施する予定である.
|
