| Project/Area Number |
20K11934
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 61030:Intelligent informatics-related
|
|---|
| Research Institution | University of Yamanashi |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2020-04-01 – 2023-03-31
|
| Project Status |
Completed (Fiscal Year 2022)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2022: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2021: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2020: ¥2,470,000 (Direct Cost: ¥1,900,000、Indirect Cost: ¥570,000)
|
|---|
| Keywords | 充足可能性判定(SAT)問題 / SATソルバー / 決定的並列SATソルバー / 充足可能性判定（SAT）問題 / 決定的SATソルバー / 並列SATソルバー / 決定的並列SAT解法 |
|---|
| Outline of Research at the Start |
命題論理の充足可能性判定問題(SAT)を解くソルバーは，システム検証やプランニング，スケジューリングなど実社会における様々な応用領域の基盤推論技術として幅広く利用されている．複数のCPUやPCを利用してSAT問題を並列に解く並列SATソルバーはSAT問題の強力な解決法であるが，ほとんどの並列SATソルバーは実行結果に再現性がなく，安定性・頑健性に欠けるという実用上の課題がある．本研究では実社会における並列SATソルバーの応用を促進するため，我々が考案した遅延学習節交換法に基づく決定的な振る舞いをする並列SATソルバーの高速化ならびに高機能化の実現を目指す．
|
| Outline of Final Research Achievements |
SAT (propositional satisfiability testing) solvers are widely used as a fundamental reasoning technique in various application domains such as system verification, planning and scheduling. In order to achieve fast solving of SAT instances, this research has developed a framework for a shared-memory deterministic parallel SAT solver. It ensures reproducible behaviour, which is important for the practical application of parallel SAT solvers, and allows existing fast sequential SAT solvers to be parallelised with less effort. Our solver has won prizes in several categories in the parallel track of the International SAT Competition 2022, showing performance comparable to non-deterministic parallel SAT solvers.
|
| Academic Significance and Societal Importance of the Research Achievements |
SAT問題の高速解法は，それを推論技術として利用する様々な応用分野にとって重要である．これまで並列SATソルバーのほとんどは求解の効率を優先するため再現性のある挙動の担保ができていなかった．これは例えばシステム検証では実行のたびに異なる不具合が見つかることを意味し，実応用に向けた課題の１つであった．我々が開発した決定的並列SATソルバーのためのフレームワークは，再現性のある挙動を担保しつつ，既存の逐次SATソルバーを少ない手間で並列化することが可能である．このフレームワークは既存の非決定的並列SATソルバーに匹敵する性能を示しており，並列SATソルバーの実用化にむけた基盤となるものといえる．
|
