2022 Fiscal Year Final Research Report
A study on deterministic parallel SAT solvers
| 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
|
| Keywords | 充足可能性判定(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.
|
| Free Research Field |
制約充足処理系の設計・開発
|
| Academic Significance and Societal Importance of the Research Achievements |
SAT問題の高速解法は，それを推論技術として利用する様々な応用分野にとって重要である．これまで並列SATソルバーのほとんどは求解の効率を優先するため再現性のある挙動の担保ができていなかった．これは例えばシステム検証では実行のたびに異なる不具合が見つかることを意味し，実応用に向けた課題の１つであった．我々が開発した決定的並列SATソルバーのためのフレームワークは，再現性のある挙動を担保しつつ，既存の逐次SATソルバーを少ない手間で並列化することが可能である．このフレームワークは既存の非決定的並列SATソルバーに匹敵する性能を示しており，並列SATソルバーの実用化にむけた基盤となるものといえる．
|
