Abstract
IsaSAT is the most advanced verified SAT solver, but it did not yet feature inprocessing (to simplify and strengthen clauses). In order to improve performance, we enriched the base calculus to not only do CDCL but also inprocess clauses. We also replaced the target of our code synthesis by Isabelle/LLVM. With these improvements, we can solve 4 times more SAT Competition 2022 problems than the original IsaSAT version, and 4.5 times more problems than any other verified SAT solver we are aware of. Additionally, our changes significantly reduce the trusted code base of our verification.
| Original language | English |
|---|---|
| Title of host publication | Automated Deduction – CADE 29 |
| Subtitle of host publication | 29th International Conference on Automated Deduction Rome, Italy, July 1–4, 2023 Proceedings |
| Editors | Randy Goebel, Wolfgang Wahlster, Zhi-Hua Zhou |
| Publisher | Springer |
| Pages | 207-219 |
| Number of pages | 13 |
| ISBN (Electronic) | 978-3-031-38499-8 |
| ISBN (Print) | 978-3-031-38498-1 |
| DOIs | |
| Publication status | Published - 2023 |
| Event | 29th International Conference on Automated Deduction, CADE 29 - Sapienza University of Rome, Rome, Italy Duration: 1 Jul 2023 → 4 Jul 2023 Conference number: 29 https://easyconferences.eu/cade2023/ |
Publication series
| Name | Lecture Notes in Artificial Intelligence |
|---|---|
| Publisher | Springer |
| Volume | 14132 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | 29th International Conference on Automated Deduction, CADE 29 |
|---|---|
| Abbreviated title | CADE 2023 |
| Country/Territory | Italy |
| City | Rome |
| Period | 1/07/23 → 4/07/23 |
| Internet address |