2008 Fiscal Year Annual Research Report
制約最適化問題のSAT変換による解法とその並列分散処理に関する研究
| Project/Area Number |
20240003
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
田村 直之 Kobe University, 学術情報基盤センター, 教授 (60207248)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
番原 睦則 神戸大学, 学術情報基盤センター, 准教授 (80290774)
平山 勝敏 神戸大学, 海事科学研究科, 准教授 (00273813)
井上 克巳 国立情報学研究所, 情報学プリンシプル研究系, 教授 (10252321)
岩沼 宏治 山梨大学, 医学工学総合研究部, 教授 (30176557)
鍋島 英知 山梨大学, 医学工学総合研究部, 准教授 (10334848)
|
|---|
| Keywords | 制約最適化問題 / 並列処理・分散処理 / 計算機システム |
|---|
| Research Abstract |
当初の研究計画に沿い各テーマの研究を進め,以下の主な成果を得た.
(A1)SAT変換型CSPソルバーを開発し,国際CSPソルバー競技会のグローバル制約部門で第1位となった.また,2次元Stripパッキング問題への応用研究を行い,未解決問題の解決に成功した.(A2)動的CSPのSAT変換について,得られるSAT問題の系列間に一致制約を導入し,ソフト制約あるいはMax-SAT問題として記述する方法を考案した.(A3)命題時相論理ののSAT変換について,有限モデル検査技術の拡張適用の可能性について検討を行い,予備的な結果を得た.(A4)分散CSPのSAT変換に関連して,分散プランニングおよびメカニズムデザインに関する研究を進め,論文発表を行った(最優秀論文賞1件,最優秀学生論文賞1件).(B1)DPLLに基づくSATソルバーにOrder encoding専用のアルゴリズムを組み込み,高速化を実現する方法を考案した.
(B2)モデル生成型定理証明器およびSATソルバーに極小モデル生成機能を付加する方法を考案し,システムの実装および性能評価を行った.(C1,D1)学習節を共有・再利用しながら複数のソルバーが協調的に解く並列ソルバーのプロトタイプを作成し,予備実験を行った.従来型の網羅的な問題分割手法を適用した場合,クライアントの台数増加に伴い性能向上の鈍化が見られるため,これを克服するためにランダムな問題分割と複数の探索戦略を併用する手法を考案し,評価実験によりその有用性を示した.また,学習節の再利用が有効に働くと想定されるMax-CSP/COPについて.ソルバーシステムの開発を進めた.
|
