| 研究課題/領域番号 |
16H02803
|
|---|
| 研究機関 | 神戸大学 |
|---|
研究代表者 |
田村 直之 神戸大学, 情報基盤センター, 教授 (60207248)
|
|---|
| 研究分担者 |
番原 睦則 神戸大学, 情報基盤センター, 准教授 (80290774)
宋 剛秀 神戸大学, 情報基盤センター, 助教 (00625121)
井上 克巳 国立情報学研究所, 大学共同利用機関等の部局等, 教授 (10252321)
鍋島 英知 山梨大学, 大学院総合研究部, 准教授 (10334848)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2019-03-31
|
| キーワード | 情報システム / 制約プログラミング / SATソルバー |
|---|
| 研究実績の概要 |
研究テーマ(A)--(D)について以下の研究を行った．研究成果には2件の招待講演と1件の発表賞が含まれる．また，情報処理学会学会誌の小特集としてSAT技術に関する解説記事4件を分担で執筆した．
(A) 時相論理WG: 時相論理の解法に必要となる技術であるインクリメンタルSAT解法に関し，論文発表を行った．また，時相論理を用いたペトリネットのデッドロック検出に関する学会発表を行い，雑誌論文執筆のために研究成果のとりまとめを行った．
(B) 多目的最適化WG: 多目的時間割問題・SAT問題の全解列挙に関する論文発表を行った．また，海外共同研究者と共にSATソルバーを利用して多目的最適化問題のパレート最適解を列挙する方法について研究を進め，新しい手法が考案できたため，研究成果のとりまとめを行った．この成果は国際会議での発表を計画している．
(C) 並列ソルバーWG: SATソルバーGlueMiniSatの開発を進め，そのシステムに関する論文発表を行った．また，並列ソルバー実現のため，ポートフォリオ型SATソルバーに関する研究を進め学会発表を行った．
(D) 応用システムWG: 時間割問題・多目的時間割問題に関する論文発表を行った．これらは海外共同研究者と共同して進めた研究である．また，部分グラフ探索・回路の配線問題と関連したナンバーリンク問題・研究室配属問題への応用に関し，良い結果が得られたため，それらの内容について学会発表を行った．特にナンバーリンクについては，情報処理学会のアルゴリズムデザインコンテストに参加し優秀な成績を収めた．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究テーマ(A)--(D)について，それぞれ順調に進展している．2016年度中に全体会合を3回行い研究進捗状況について確認した．11月に海外共同研究者であるDaniel Le Berre教授を招聘し共同研究に関する意見交換を行った．また，日本ソフトウェア科学会全国大会・人工知能学会全国大会オーガナイズドセッションなどで，研究分担者以外の研究者を含めた研究交流を行い，今後の研究推進方針について示唆を得た．
|
| 今後の研究の推進方策 |
研究テーマ(A)--(D)について，以下を計画している．
(A) 時相論理WG: ペトリネットのデッドロック検出に関し，雑誌論文執筆を進める．時相論理LTLに関する検討を進める．
(B) 多目的最適化WG: 多目的最適問題のパレート最適解を列挙する方法について研究成果のとりまとめを行い，論文執筆を進める．
(C) 並列ソルバーWG: SATソルバーGlueMiniSatの改良に関する研究を進める．また，並列ポートフォリオ型SATソルバーに関する研究を進める．
(D) 応用システムWG: 時間割問題・多目的時間割問題・ナンバーリンク問題・研究室配属問題への応用に関し研究を進め，論文発表および学会発表を行う．
|
| 備考 |
本研究で開発したソフトウェアは，上記URLから入手可能である．
|
