Fazekas, K., Pollitt, F., Fleury, M., & Biere, A. (2024, July 23). Certifying Incremental SAT Solving [Conference Presentation]. 22nd International Workshop on Satisfiability Modulo Theories (SMT 2024), Montreal, Canada.
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Date (published):
23-Jul-2024
-
Event name:
22nd International Workshop on Satisfiability Modulo Theories (SMT 2024)
en
Event date:
22-Jul-2024 - 23-Jul-2024
-
Event place:
Montreal, Canada
-
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%