2011 Fiscal Year Annual Research Report
制約最適化問題のSAT変換による解法とその並列分散処理に関する研究
| Project/Area Number |
20240003
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
田村 直之 神戸大学, 情報基盤センター, 教授 (60207248)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
番原 睦則 神戸大学, 情報基盤センター, 准教授 (80290774)
井上 克巳 国立情報学研究所, 情報学プリンシプル研究系, 教授 (10252321)
岩沼 宏治 山梨大学, 医学工学総合研究部, 教授 (30176557)
横尾 真 九州大学, システム情報科学研究院, 教授 (20380678)
長谷川 隆三 九州大学, システム情報科学研究院, 教授 (20274483)
|
|---|
| Keywords | SAT / 制約最適化問題 / 並列処理・分散処理 |
|---|
| Research Abstract |
最終年度として研究開発を行い,33件の学会誌論文・国際会議論文(うち査読付論文32件,ベストペーパー2件)の公表,18件の学会発表(うちベストペーパー1件)を行った.
特筆すべき研究開発成果としては以下のものが挙げられる,(1)SATソルバーGlueMiniSatが,SAT2011競技会の逐次型ソルバートラックのApplication部門においてUNSATクラスで1位,SAT+UNSATクラスで2位,さらに並列型ソルバートラックのApplication部門UNSATクラスで2位を獲得という非常に優秀な成績を収めた.(2)MaxSATソルバーQMaxSATが,MaxSAT Evaluation 2011のPartial MaxSAT部門において前年に引き続きIndustrialで1位,Craftedで2位という優れた成績を収めた.
その他,以下の研究を進めた:CSPのコンパクトかつ効率的な新しいSAT符号化;値変更コスト付き動的SATおよび動的CSPの解法;複数の背景理論を持つSMTへの部分評価法の導入;分散CSPの応用としての提携構造形成問題とメカニズムデザイン;SATソルバーにおける局所対称性除去手法;極小モデル生成器MiniMGの高速化手法;SAT技術の釣合い型不完備ブロック計画構成問題への応用;擬似ブールソルバーを応用した部分MaxSATソルバーの開発;SATソルバーを利用した極小モデル生成器を用いた代謝パスウェイの解析;GlueMiniSatの技術を応用した並列SATソルバーの開発;セマフォを利用した並列SATソルバーの開発.
また,全研究者の参加するCSPSAT研究会を3回,CSPSAT講演会を1回開催し(参加者数のべ93名),第25回人工知能学会全国大会のオーガナイズドセッションrSAT技術の理論,実装,応用」を企画した.
|
