| 研究課題/領域番号 |
20K11934
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分61030:知能情報学関連
|
|---|
| 研究機関 | 山梨大学 |
|---|
研究代表者 |
鍋島 英知 山梨大学, 大学院総合研究部, 准教授 (10334848)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2023-03-31
|
| キーワード | 充足可能性判定(SAT)問題 / SATソルバー / 決定的並列SATソルバー |
|---|
| 研究成果の概要 |
命題論理の充足可能性判定器(SATソルバー)は，システム検証やプランニング，スケジューリングなど様々な応用領域における基盤推論技術として幅広く利用されている．SAT問題の高速な求解にむけて，本研究では共有メモリ環境向けの決定的並列SATソルバーのためのフレームワークを実現した．これは並列SATソルバーの実用化に向けて重要となる再現性のある挙動を担保しており，また既存の高速な逐次SATソルバーを少ない手間で並列化することが可能である．我々の開発したソルバーは2022年の国際SAT競技会の並列部門の複数カテゴリで入賞しており，非決定的並列SATソルバーに匹敵する性能を達成できることを示している．
|
| 自由記述の分野 |
制約充足処理系の設計・開発
|
| 研究成果の学術的意義や社会的意義 |
SAT問題の高速解法は，それを推論技術として利用する様々な応用分野にとって重要である．これまで並列SATソルバーのほとんどは求解の効率を優先するため再現性のある挙動の担保ができていなかった．これは例えばシステム検証では実行のたびに異なる不具合が見つかることを意味し，実応用に向けた課題の１つであった．我々が開発した決定的並列SATソルバーのためのフレームワークは，再現性のある挙動を担保しつつ，既存の逐次SATソルバーを少ない手間で並列化することが可能である．このフレームワークは既存の非決定的並列SATソルバーに匹敵する性能を示しており，並列SATソルバーの実用化にむけた基盤となるものといえる．
|
