| 研究課題/領域番号 |
25330085
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
越村 三幸 九州大学, システム情報科学研究科(研究院, 助教 (30274492)
|
|---|
| 研究分担者 |
長谷川 隆三 九州大学, 大学院システム情報科学研究院, 教授 (20274483)
藤田 博 九州大学, 大学院システム情報科学研究院, 准教授 (70284552)
力 規晃 徳山工業高等学校, 情報電子工学科, 助手 (50290804)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| 研究課題ステータス |
完了 (2015年度)
|
| 配分額 *注記 |
4,940千円 (直接経費: 3,800千円、間接経費: 1,140千円)
2015年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2014年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
2013年度: 1,820千円 (直接経費: 1,400千円、間接経費: 420千円)
|
|---|
| キーワード | SATソルバー / 基数制約 / SAT符号化 / MaxSAT応用 / MaxSATソルバー / 組合せ最適 |
|---|
| 研究成果の概要 |
本研究で得られた主要な研究成果は次の通り．
(1)複数の戦略を切り替えながら探索を進める方法をSATソルバーに導入することにより性能向上を図る手法の効果を示した．(2)基数制約のSAT符号化の新手法Modulo TotalizerとWeighted Totalizerを考案しその空間計算量を示すとともにその効果をMaxSAT問題を解くことにより示した．(3)MaxSATを利用して以下の問題を解く手法を確立した．①帰納論理プログラミング、②提携構造形成問題、③AES暗号鍵の復元．(4)MaxSATソルバーQMaxSATにUNSATコアを利用する機構を導入した．
|
