2017 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)について以下の研究を行った．研究成果には1件の招待講演が含まれる．
(A) 時相論理WG: 時相論理を用いたペトリネットのデッドロック検出に関する雑誌論文執筆のために研究成果のとりまとめを行った．この研究は，本研究グループで開発したSAT符号化技術，インクリメンタルSAT解法を利用したものである．既存研究よりも優れた結果が得られたため，現在雑誌論文として執筆し投稿中である．
(B) 多目的最適化WG: 多目的制約最適化問題・多目的分散制約最適化問題に関する論文発表を行った．特に，多目的制約最適化問題に関するものは海外共同研究者との共著であり，制約プログラミングに関する一流の国際会議(CP 2017)で高い評価を得た．また，関連する研究として，新しいSAT符号化に関する論文発表と学会発表を行った．
(C) 並列ソルバーWG: SATソルバーGlueMiniSatの開発を進め，新しく考案した手法に関する論文発表を行った．発表を行った国際会議 (SAT 2017)はSAT技術に関する一流の国際会議であり，発表した成果は高い評価を得た．また，並列ポートフォリオ型SATソルバー・GPUを用いたSATソルバーに関する学会発表を行った．
(D) 応用システムWG: 時間割問題に関する論文発表を行った．これらは海外共同研究者との共著である．また，テストケース生成・回路の配線問題と関連したナンバーリンク問題・研究室配属問題への応用に関し，良い結果が得られたため，それらの内容について学会発表を行った．特に，ナンバーリンクについては情報処理学会のアルゴリズムデザインコンテストに関する小特集に解説記事を発表した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究テーマ(A)--(D)について，それぞれ順調に進展している．2017年度中に全体会合を2回行い研究進捗状況について確認した．研究分担者の1名は，2017年9月から1年間フランスのアルトワ大学に客員研究員として滞在し，共同研究を進めている．また，滞在先である相手方研究機関の研究者らと神戸大学の研究者とでCRIL-Kobe-Louvain共同ワークショップを2017年12月にベルギーの神戸大学ブリュッセル・オフィスで開催した．また，日本ソフトウェア科学会全国大会・人工知能学会全国大会オーガナイズドセッションなどで，研究分担者以外の研究者を含めた研究交流を行い，今後の研究推進方針について示唆を得た．
|
| Strategy for Future Research Activity |
研究テーマ(A)--(D)について，以下を計画している．
(A) 時相論理WG: ペトリネットのデッドロック検出に関し雑誌論文発表を行う．また様相命題論理の充足可能性判定に関する研究を行う．
(B) 多目的最適化WG: 論文発表を行った多目的最適問題のパレート最適解を列挙する方法について，改良を検討する．
(C) 並列ソルバーWG: 開発したSATソルバーGlueMiniSatの改良に関する研究を進める．また，並列SATソルバーに関する研究を進める．
(D) 応用システムWG: 時間割問題・多目的時間割問題・研究室配属問題への応用に関し研究を勧め，論文発表および学会発表を行う．
|
| Remarks |
本研究で開発したソフトウェアは，上記URLから入手可能である．
|
