A Study of Accelerating Boolean Satisfiability Solvers
Project/Area Number |
26330248
|
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) |
2014-04-01 – 2017-03-31
|
Project Status |
Completed (Fiscal Year 2016)
|
Budget Amount *help |
¥4,810,000 (Direct Cost: ¥3,700,000、Indirect Cost: ¥1,110,000)
Fiscal Year 2016: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2015: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2014: ¥2,600,000 (Direct Cost: ¥2,000,000、Indirect Cost: ¥600,000)
|
Keywords | 充足可能性判定問題 / SATソルバー / 充足可能性判定(SAT)問題 / 動的簡単化 |
Outline of Final Research Achievements |
A SAT solver that determines satisfiability of a given propositional formula is a key technique to solve hard combinatorial instances, and is used in various fields such as system verification and scheduling. The purpose of this research project is performance improvement of SAT solvers. We studied and developed lightweight simplification techniques that are applied during solving, robust heuristics for restarts and clause database reductions, parallel solving and so on. We have achieved the performance improvement by using these techniques compared with previous work.
|
Report
(4 results)
Research Products
(17 results)