| 研究課題/領域番号 |
20K11748
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 神戸大学 |
|---|
研究代表者 |
宋 剛秀 神戸大学, DX・情報統括本部, 准教授 (00625121)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2023-03-31
|
| 研究課題ステータス |
完了 (2022年度)
|
| 配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2022年度: 520千円 (直接経費: 400千円、間接経費: 120千円)
2021年度: 520千円 (直接経費: 400千円、間接経費: 120千円)
2020年度: 3,250千円 (直接経費: 2,500千円、間接経費: 750千円)
|
|---|
| キーワード | SATソルバー / SAT符号化 / MDD / 制約充足問題 / 制約プログラミング / SAT (充足可能性判定問題) / CSP (制約充足問題) |
|---|
| 研究開始時の研究の概要 |
近年，SAT問題を解くプログラムであるSATソルバーの飛躍的な進歩にともない，制約充足問題 (CSP) をSAT問題に符号化（SAT符号化）して解くSAT型CSPソルバーが成功している．
本研究の目的は，SAT型CSPソルバーの高速化であり，そのためにMDD (Multi-valued Decision Diagram) を用いたCSPの正規化と，MDDが表す制約 (MDD制約) のSAT符号化を研究開発する．
本研究の意義は，SAT型CSPソルバーの新しい一方式を開拓できる点，既存のCSPソルバーでは求解困難な問題に対して，より高性能な推論基盤を提供できる点である．
|
| 研究成果の概要 |
制約充足問題 (CSP) は，与えられた制約を満たす解を探索する問題である．CSP には産学問わず様々な応用があり，人工知能分野などにおける重要な研究課題となっている．本研究では,SATソルバーを用いた高性能な CSP を解くシステムを実現するために，制約のMDD表現とSAT符号化を用いた方法を研究開発した．結果として，国際競技会における入賞とシステムの高速化に成功した．また応用研究として生物学における細胞内で起こる遺伝子の相互作用のネットワークの数理モデルであるオートマタネットワークの定常状態の計算にSAT型解法を応用した．さらにハミルトン閉路問題のSAT型解法の提案も行った．
|
| 研究成果の学術的意義や社会的意義 |
本研究成果の意義は，SAT符号化の新しい方向性を開拓した点，既存のCSPソルバーでは求解困難な問題に対して．より高性能な推論基盤の候補を提供した点である．またシステム生物学における定常状態の解析への応用を示したことも貢献として挙げられる．CSPソルバーは様々な分野に応用される実用性が高いシステムであり，研究成果の産業分野への応用も期待できると考えられる．
|
