| 研究課題/領域番号 |
20K11934
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分61030:知能情報学関連
|
|---|
| 研究機関 | 山梨大学 |
|---|
研究代表者 |
鍋島 英知 山梨大学, 大学院総合研究部, 准教授 (10334848)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2023-03-31
|
| 研究課題ステータス |
完了 (2022年度)
|
| 配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2022年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2021年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2020年度: 2,470千円 (直接経費: 1,900千円、間接経費: 570千円)
|
|---|
| キーワード | 充足可能性判定(SAT)問題 / SATソルバー / 決定的並列SATソルバー / 充足可能性判定（SAT）問題 / 決定的SATソルバー / 並列SATソルバー / 決定的並列SAT解法 |
|---|
| 研究開始時の研究の概要 |
命題論理の充足可能性判定問題(SAT)を解くソルバーは，システム検証やプランニング，スケジューリングなど実社会における様々な応用領域の基盤推論技術として幅広く利用されている．複数のCPUやPCを利用してSAT問題を並列に解く並列SATソルバーはSAT問題の強力な解決法であるが，ほとんどの並列SATソルバーは実行結果に再現性がなく，安定性・頑健性に欠けるという実用上の課題がある．本研究では実社会における並列SATソルバーの応用を促進するため，我々が考案した遅延学習節交換法に基づく決定的な振る舞いをする並列SATソルバーの高速化ならびに高機能化の実現を目指す．
|
| 研究成果の概要 |
命題論理の充足可能性判定器(SATソルバー)は，システム検証やプランニング，スケジューリングなど様々な応用領域における基盤推論技術として幅広く利用されている．SAT問題の高速な求解にむけて，本研究では共有メモリ環境向けの決定的並列SATソルバーのためのフレームワークを実現した．これは並列SATソルバーの実用化に向けて重要となる再現性のある挙動を担保しており，また既存の高速な逐次SATソルバーを少ない手間で並列化することが可能である．我々の開発したソルバーは2022年の国際SAT競技会の並列部門の複数カテゴリで入賞しており，非決定的並列SATソルバーに匹敵する性能を達成できることを示している．
|
| 研究成果の学術的意義や社会的意義 |
SAT問題の高速解法は，それを推論技術として利用する様々な応用分野にとって重要である．これまで並列SATソルバーのほとんどは求解の効率を優先するため再現性のある挙動の担保ができていなかった．これは例えばシステム検証では実行のたびに異なる不具合が見つかることを意味し，実応用に向けた課題の１つであった．我々が開発した決定的並列SATソルバーのためのフレームワークは，再現性のある挙動を担保しつつ，既存の逐次SATソルバーを少ない手間で並列化することが可能である．このフレームワークは既存の非決定的並列SATソルバーに匹敵する性能を示しており，並列SATソルバーの実用化にむけた基盤となるものといえる．
|
