2018 Fiscal Year Annual Research Report
Research and Development of a New Constraint Programming System based on SAT
| Project/Area Number |
16H02803
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
田村 直之 神戸大学, 情報基盤センター, 教授 (60207248)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
番原 睦則 名古屋大学, 情報学研究科, 教授 (80290774)
宋 剛秀 神戸大学, 情報基盤センター, 助教 (00625121)
井上 克巳 国立情報学研究所, 情報学プリンシプル研究系, 教授 (10252321)
鍋島 英知 山梨大学, 大学院総合研究部, 准教授 (10334848)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | 情報システム / 制約プログラミング / SATソルバー |
|---|
| Outline of Annual Research Achievements |
研究テーマ(A)--(D)について以下の研究を行い，関連する成果を学会等で発表した．
(A) 時相論理WG: 本研究グループで開発したSAT符号化技術，インクリメンタルSAT解法を適用し，時相論理を用いたペトリネットのデッドロック検出のための手法を研究し，その成果を雑誌論文として発表した．本論文は，情報処理学会論文誌の2018年度特選論文に選定されている．また，様相命題論理S4の充足可能性判定に関する研究も行った．
(B) 多目的最適化WG: 多目的分散制約最適化問題に対して，動的プログラミングに基づきパレート解を保障するアルゴリズムを開発した．またメッセージ数を抑えるための近似アルゴリズムも示した．
(C) 並列ソルバーWG: 決定的並列SATソルバーの多数コア環境下での通信コストを抑えるため，学習節交換に関する排他制御の低減手法とリテラル走査数に基づき節交換間隔を精密化する手法を提案・実装した．評価実験の結果，多数コア環境においても節交換ならびに同期待ち時間を大幅に低減できることを確認した．
(D) 応用システムWG: ペトリネットのデッドロック検出手法，カリキュラムベース・コース時間割問題，研究室配属問題，グラフ彩色問題などに関する応用研究を進めた．またSAT技術を用いた制約ソルバーsCOPを開発し，公開した．sCOPは出場した国際制約ソルバー競技会 (XCSP3 Competition 2018)において逐次CSPソルバー部門と並列CSPソルバー部門の2部門で優勝し，国際的に高い評価を受けた．
|
| Research Progress Status |
平成30年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
平成30年度が最終年度であるため、記入しない。
|
| Remarks |
本研究で開発したソフトウェアは，上記URLから入手可能である．
|
