2019 Fiscal Year Final Research Report
A fast Boolean satisfiability problem solver by shortening the proof
| Project/Area Number |
17K00300
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Intelligent informatics
|
|---|
| Research Institution | University of Yamanashi |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2017-04-01 – 2020-03-31
|
| Keywords | 充足可能性判定（SAT）問題 / SATソルバー / 決定的並列SATソルバー / 圧縮 |
|---|
| Outline of Final Research Achievements |
In order to improve the performance of propositional satisfiability problem solver (SAT solver), we have implemented a deterministic portfolio parallel SAT solver and a solver that can directly solve a compressed instance. The former parallel SAT solver ensures reproducible behavior and achieves comparable performance with non-deterministic parallel solvers by allowing delayed clause exchange. The latter approach compresses regular clauses in a given SAT instance and can solve the compressed instance without expansion. We have experimentally confirmed that this approach is effective to solve the huge SAT instances. Although this has no effect for proof shortening at the moment, it will be the foundation of the study to acquire compressed learned clauses.
|
| Free Research Field |
制約充足処理系の設計・開発
|
| Academic Significance and Societal Importance of the Research Achievements |
SAT問題は，計算機科学において最も基本的かつ本質的な組合せ問題であり，SAT問題を解くソルバーは様々な応用領域における基盤推論技術として幅広く利用されている．よってSATソルバーの高速化は，それを基盤とする様々な応用領域にとって重要である．我々の考案した遅延学習節交換法に基づく並列SATソルバーは，再現性のある挙動を保証しているため並列SATソルバーの実応用を容易にする．また巨大なSAT問題を圧縮したまま解く手法の開発は，SATの応用範囲の拡大のために重要であり，圧縮節の学習による証明短縮手法を検討するための基盤となる．
|
