Fazekas, K., Niemetz, A., Preiner, M., Kirchweger, M., Szeider, S., & Biere, A. (2024). Satisfiability Modulo User Propagators. Journal of Artificial Intelligence Research, 81, 989–1017. https://doi.org/10.1613/jair.1.16163
E192-01 - Forschungsbereich Algorithms and Complexity E056-13 - Fachbereich LogiCS E056-23 - Fachbereich Innovative Combinations and Applications of AI and ML (iCAIML) E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Journal:
Journal of Artificial Intelligence Research
-
ISSN:
1076-9757
-
Date (published):
27-Dec-2024
-
Number of Pages:
29
-
Publisher:
AI ACCESS FOUNDATION
-
Peer reviewed:
Yes
-
Keywords:
Automated Reasoning; Satisfiability; User Interfaces
en
Abstract:
Modern SAT solvers are often integrated as sub-reasoning engines into more complex tools to address problems beyond the Boolean satisfiability problem. Consider, for example, solvers for Satisfiability Modulo Theories (SMT), combinatorial optimization, model enumeration, and model counting. There, the SAT solver can often provide relevant information beyond the satisfiability answer and the domain knowledge of the embedding system, such as symmetry properties or theory axioms, may benefit the CDCL search. However, this knowledge can often not be efficiently represented in clausal form.
This paper proposes a general interface to inspect and influence the internal behaviour of CDCL SAT solvers. The aim is to capture the essential functionalities that simplify and improve use cases requiring a more fine-grained interaction with the SAT solver than provided via the standard IPASIR interface. For our experiments, the state-of-the-art SAT solver CaDiCaL is extended with the proposed interface and evaluated on two representative use cases: enumerating graphs within the SAT modulo Symmetries framework (SMS), and as the main CDCL(T) SAT engine of the SMT solver cvc5.
en
Project title:
Inkrementelles SAT und SMT für skalierbare Verifikation: T 1306-N (FWF - Österr. Wissenschaftsfonds) SAT-Basierende lokale Verbesserungsmethoden: P32441-N35 (FWF - Österr. Wissenschaftsfonds) Revealing and Utilizing the Hidden Structure for Solving Hard Problems in AI: ICT19-065 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds)
-
Research Areas:
Logic and Computation: 20% Computer Engineering and Software-Intensive Systems: 80%