| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2019: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2018: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2017: ¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000)
|
|---|
| 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.
|
