Development of a SAT Solver Based on Extened Resolution
| Project/Area Number |
17K12742
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Intelligent informatics
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
Sonobe Tomohiro 国立情報学研究所, ビッグデータ数理国際研究センター, 特任研究員 (50747269)
|
|---|
| Project Period (FY) |
2017-04-01 – 2023-03-31
|
| Project Status |
Completed (Fiscal Year 2022)
|
| Budget Amount *help |
¥2,470,000 (Direct Cost: ¥1,900,000、Indirect Cost: ¥570,000)
Fiscal Year 2019: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2018: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2017: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
|
|---|
| Keywords | 充足可能性問題 / SATソルバ / 探索 |
|---|
| Outline of Final Research Achievements |
The satisfiability problem (SAT problem) is known as an important problem in computer science. The SAT solver is a computer program for this problem, and the enhancement of SAT solvers is essential because they are useful to resolve various real-world problems. In this research, we utilize the extended resolution, considered to be more powerful than general resolution used in the state-of-the-art SAT solvers, on the pigeonhole principle. Experimental results indicate that our method can improve the existing solvers.
|
| Academic Significance and Societal Importance of the Research Achievements |
充足可能性問題(SAT問題)を解くSATソルバは、回路検証、コンピュータプログラムのバグ発見、数学的問題の解決、暗号解析等、現実世界の様々な問題の解を高速に求められる水準に達し、更なる発展が期待されている。本研究では、SATソルバに対して、より理論的に強力であると考えられている拡張融合法を組み込むことを目的として、鳩の巣原理問題に対して、従来のSATソルバの高速化を達成した。
|
Report
(7 results)
Research Products
(3 results)
