Fazekas, K., Pollitt, F., Fleury, M., & Biere, A. (2024). Certifying Incremental SAT Solving. In Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 321–340). https://doi.org/10.29007/pdcc
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Published in:
Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
-
Volume:
100
-
Date (published):
26-May-2024
-
Event name:
25th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2024)
en
Event date:
23-May-2024 - 29-May-2024
-
Event place:
Port Louis, Mauritius
-
Number of Pages:
20
-
Peer reviewed:
Yes
-
Keywords:
certification; incremental SAT; proof checking
en
Abstract:
Certifying results by checking proofs and models is an essential feature of modern SAT solving. While incremental solving with assumptions and core extraction is crucial for many applications, support for incremental proof certificates remains lacking. We propose a proof format and corresponding checkers for incremental SAT solving. We further extend it to leverage resolution hints. Experiments on incremental SAT solving for Bounded Model Checking and Satisfiability Modulo Theories demonstrate the feasibility of our approach, further confirming that resolution hints substantially reduce checking time.
en
Project title:
Inkrementelles SAT und SMT für skalierbare Verifikation: T 1306-N (FWF - Österr. Wissenschaftsfonds)
-
Research Areas:
Logic and Computation: 40% Computer Engineering and Software-Intensive Systems: 40% Computer Science Foundations: 20%
