研究課題/領域番号 |
16K16036
|
研究種目 |
若手研究(B)
|
配分区分 | 基金 |
研究分野 |
ソフトウェア
|
研究機関 | 神戸大学 |
研究代表者 |
宋 剛秀 神戸大学, 情報基盤センター, 助教 (00625121)
|
研究期間 (年度) |
2016-04-01 – 2019-03-31
|
研究課題ステータス |
完了 (2018年度)
|
配分額 *注記 |
3,900千円 (直接経費: 3,000千円、間接経費: 900千円)
2018年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2017年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2016年度: 2,600千円 (直接経費: 2,000千円、間接経費: 600千円)
|
キーワード | SATソルバー / SAT符号化 / 順序符号化 / 対数符号化 / ハイブリッド符号化 / 制約充足問題 / 制約プログラミング / 情報システム |
研究成果の概要 |
制約充足問題 (CSP) は,与えられた制約を満たす解を探索する問題である.CSP には産学問わず様々な応用があり,人工知能分野などにおける重要な研究課題となっている.本研究では, SATソルバーを用いた高性能な CSP を解くシステム (SAT型CPシステム) を実現するために,ハイブリッド符号化を用いた方法を研究開発した.結果として,国際競技会における優勝や, 従来システムでは解けない問題を解くことに成功した.
|
研究成果の学術的意義や社会的意義 |
本研究成果の意義は,SAT符号化の新しい方向性を開拓した点,既存のCPシステムでは求解困難な問題に対して,より高性能な推論基盤の候補を提供した点である.また重要な応用の1つとして,システム生物学やグラフ上の問題にも適用可能な多目的最適化問題への応用を示したことも挙げられる.CPシステムは様々な分野に応用される実用性が高いシステムであり,研究成果の産業分野への応用も期待できると考えられる.
|