| 研究課題/領域番号 |
16H02803
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 神戸大学 |
|---|
研究代表者 |
田村 直之 神戸大学, 情報基盤センター, 教授 (60207248)
|
|---|
| 研究分担者 |
番原 睦則 名古屋大学, 情報学研究科, 教授 (80290774)
宋 剛秀 神戸大学, 情報基盤センター, 助教 (00625121)
井上 克巳 国立情報学研究所, 情報学プリンシプル研究系, 教授 (10252321)
鍋島 英知 山梨大学, 大学院総合研究部, 准教授 (10334848)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2019-03-31
|
| 研究課題ステータス |
完了 (2018年度)
|
| 配分額 *注記 |
16,900千円 (直接経費: 13,000千円、間接経費: 3,900千円)
2018年度: 5,200千円 (直接経費: 4,000千円、間接経費: 1,200千円)
2017年度: 5,460千円 (直接経費: 4,200千円、間接経費: 1,260千円)
2016年度: 6,240千円 (直接経費: 4,800千円、間接経費: 1,440千円)
|
|---|
| キーワード | 制約プログラミング / 充足可能性判定問題 / 命題論理 / 情報システム / SATソルバー |
|---|
| 研究成果の概要 |
高性能な推論を必要とする種々の分野において，SAT技術を活用したSAT型システムが成功を収めている．本研究では，SAT技術を基盤とした制約プログラミングシステム (以下，SAT型CPシステム)を対象とし，従来のSAT技術の適用範囲を超えた範囲に拡張することを目的として(A) 時相論理に対する拡張，(B) 多目的最適化問題に対する拡張，(C) 並列型ソルバー，(D) 応用システムに関する研究開発を行った．その結果，国際制約ソルバー競技会での優勝，既存手法では解けなかった問題の解決などの良い成果を得た．
|
| 研究成果の学術的意義や社会的意義 |
高度な推論を必要とする人工知能システムなどの実現を目的として，その基本技術となるSAT型CPシステムの研究開発を行った．開発したシステムの1つであるsCOPは，2018年の国際制約ソルバー競技会の2部門で優勝している．また，ペトリネットのデッドロック検出，研究室配属問題，時間割問題，テストケース生成，配線問題などへの応用研究を行い，これまでよりも優れた結果を得た．
|
