2022 Fiscal Year Annual Research Report
Development of a SAT Solver Based on Extened Resolution
| Project/Area Number |
17K12742
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
薗部 知大 国立情報学研究所, ビッグデータ数理国際研究センター, 特任研究員 (50747269)
|
|---|
| Project Period (FY) |
2017-04-01 – 2023-03-31
|
| Keywords | 充足可能性問題 / SATソルバ |
|---|
| Outline of Annual Research Achievements |
充足可能性問題(Satisfiability problem, SAT問題)とは、真偽の値を取るBoolean変数から構成された論理式に対して、その論理式を真にするような変数割り当てが存在するか証明する問題であり、計算機科学の重要な問題として知られている。この問題を解くプログラムであるSATソルバは、回路検証や定理証明などの現実世界の問題の解決にも応用されていて、現在も様々な手法の研究開発が積極的に行われている。
本研究では、従来のSATソルバの学習機能の基礎となっている融合法と比べて、より理論的に強力と考えられている拡張融合法を用いたSATソルバの実現を目指す。拡張融合法は、鳩の巣原理問題において、問題を多項式処理ステップで解の発見が可能であることが理論的に証明されているものの、そのアルゴリズムを用いた高速なSATソルバに関する研究の余地は多く残されていると考えられる。
最終年度である本年度は、鳩の巣原理問題に対して、拡張融合法を用いた問題に対する変換を行った後に、その問題に対して拡張された変数を探索中に有効的に活用する手法の提案および実装を行い、既存のSATソルバの性能向上に成功した。具体的には、現在の高水準なSATソルバの基盤となっているMiniSATおよびGlucoseに対して、拡張融合法によって追加された変数に対して優先的に値を割り振る処理を追加したところ、鳩の巣原理問題においてよりサイズの大きい問題を扱うことが可能になった。本成果は論文誌Algorithmsに採録された。
|
Research Products
(1 results)
