| 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)
|
|---|
| 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.
|
