| 研究課題/領域番号 |
17K00300
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
知能情報学
|
|---|
| 研究機関 | 山梨大学 |
|---|
研究代表者 |
鍋島 英知 山梨大学, 大学院総合研究部, 准教授 (10334848)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2020-03-31
|
| 研究課題ステータス |
完了 (2019年度)
|
| 配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2019年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2018年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2017年度: 2,080千円 (直接経費: 1,600千円、間接経費: 480千円)
|
|---|
| キーワード | 充足可能性判定（SAT）問題 / SATソルバー / 決定的並列SATソルバー / 圧縮 / 圧縮節 / ヒューリスティクス / 動的対称性除去 / アルゴリズム / 充足可能性判定問題 |
|---|
| 研究成果の概要 |
命題論理の充足可能性判定器(SATソルバー)の高速化のため，本研究では決定的並列SATソルバーと圧縮節を展開せず直接求解可能なソルバーを実現した．前者の並列SATソルバーは，再現性のある挙動を担保しつつ学習節交換に遅延を許容することで非決定的ソルバーに匹敵する性能を持つことが特徴である．後者はSAT問題に含まれる規則的な節集合を圧縮し，それを展開せずに求解する手法を実装したソルバーであり，巨大なSAT問題の求解に効果的であることを確認した．現時点では証明短縮の効果はないものの，今後圧縮した学習節獲得による高速化手法実現のための基盤となる．
|
| 研究成果の学術的意義や社会的意義 |
SAT問題は，計算機科学において最も基本的かつ本質的な組合せ問題であり，SAT問題を解くソルバーは様々な応用領域における基盤推論技術として幅広く利用されている．よってSATソルバーの高速化は，それを基盤とする様々な応用領域にとって重要である．我々の考案した遅延学習節交換法に基づく並列SATソルバーは，再現性のある挙動を保証しているため並列SATソルバーの実応用を容易にする．また巨大なSAT問題を圧縮したまま解く手法の開発は，SATの応用範囲の拡大のために重要であり，圧縮節の学習による証明短縮手法を検討するための基盤となる．
|
