Picky CDCL: SMT-Solving with Flexible Literal Selection
Pages 1 - 19
Abstract
SMT solvers have traditionally been optimized for determining the satisfiability of a query as quickly as possible. However, they are increasingly being used in applications where the time required to determine satisfiability might not be the main concern, such as mining inductive invariants for safety proofs.
This paper studies how lookahead-inspired SMT solving, when made sufficiently efficient and integrated into a conflict-driven, clause learning SMT core, can be a valuable component in a portfolio for proof-based interpolation in model checking.
We implemented the algorithmic idea, called Picky CDCL, in the SMT solver OpenSMT and show its efficiency in the Horn solver Golem using a range of model checking approaches and in SMT proof validation applications.
References
[1]
Alt L, Fedyukovich G, Hyvärinen AEJ, and Sharygina N Gurfinkel A and Seshia SA A proof-sensitive approach for small propositional interpolants Verified Software: Theories, Tools, and Experiments 2016 Cham Springer 1-18
[2]
Barbosa, H., et al.: Flexible proof production in an industrial-strength SMT solver. In: Blanchette, J., Kovács, L., Pattinson, D. (eds.) Proceedings of the 11th International Joint Conference on Automated Reasoning, IJCAR 2022, Haifa, Israel, 8–10 August 2022. LNCS, vol. 13385, pp. 15–35. Springer, Heidelberg (2022).
[3]
Barrett C, de Moura L, and Stump A Etessami K and Rajamani SK SMT-COMP: satisfiability modulo theories competition Computer Aided Verification 2005 Heidelberg Springer 20-23
[4]
Barrett C, Nieuwenhuis R, Oliveras A, and Tinelli C Hermann M and Voronkov A Splitting on demand in SAT modulo theories Logic for Programming, Artificial Intelligence, and Reasoning 2006 Heidelberg Springer 512-526
[5]
Blicha, M., Britikov, K., Sharygina, N.: The golem Horn solver. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, CAV 2023. LNCS, vol. 13965, pp. 209–223. Springer, Cham (2023).
[6]
Blicha, M., Fedyukovich, G., Hyvärinen, A.E.J., Sharygina, N.: Split transition power abstraction for unbounded safety. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, 17–21 October 2022, pp. 349–358. IEEE (2022).
[7]
Blicha M, Hyvärinen AEJ, Kofroň J, and Sharygina N Vojnar T and Zhang L Decomposing Farkas interpolants Tools and Algorithms for the Construction and Analysis of Systems 2019 Cham Springer 3-20
[8]
Böhm M and Speckenmeyer E A fast parallel SAT-solver - efficient workload balancing Ann. Math. Artif. Intell. 1996 17 381-400
[9]
Bruttomesso R, Pek E, Sharygina N, and Tsitovich A Esparza J and Majumdar R The OpenSMT solver Tools and Algorithms for the Construction and Analysis of Systems 2010 Heidelberg Springer 150-153
[10]
Craig W Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory J. Symb. Log. 1957 22 269-285
[11]
Davis M, Logemann G, and Loveland DW A machine program for theorem-proving Commun. ACM 1962 5 394-397
[12]
De Angelis, E., Hari Govind, V.K.: CHC-COMP 2022: competition report. In: Hamilton, G.W., Kahsai, T., Proietti, M. (eds.) Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation, HCVS/VPT@ETAPS 2022 and 10th International Workshop on Verification and Program Transformation, Munich, Germany, 3 April 2022, EPTCS, vol. 373, pp. 44–62 (2022).
[13]
D’Silva V Gordon AD Propositional interpolation and abstract interpretation Programming Languages and Systems 2010 Heidelberg Springer 185-204
[14]
Gurfinkel, A.: Program verification with constrained horn clauses (invited paper). In: Shoham, S., Vizel, Y. (eds.) Proceedings of the 34th International Conference on Computer Aided Verification, CAV 2022, Part I. LNCS, Haifa, Israel, 7–10 August 2022, vol. 13371, pp. 19–29. Springer, Heidelberg (2022).
[15]
Heule MJH, Kullmann O, Wieringa S, and Biere A Eder K, Lourenço J, and Shehory O Cube and conquer: guiding CDCL SAT solvers by lookaheads Hardware and Software: Verification and Testing 2012 Heidelberg Springer 50-65
[16]
Heule, M.J.H.: The DRAT format and drat-trim checker. CoRR abs/1610.06229 (2016)
[17]
Heule, M.J.H., van Maaren, H.: Look-ahead based SAT solvers, 2nd edn. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 183–212. IOS Press (2021).
[18]
Hojjat, H., Rümmer, P.: The ELDARICA horn solver. In: Bjørner, N.S., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, 30 October–2 November 2018, pp. 1–7. IEEE (2018).
[19]
Hyvärinen AEJ, Marescotti M, Alt L, and Sharygina N Creignou N and Le Berre D OpenSMT2: an SMT solver for multi-core and cloud computing Theory and Applications of Satisfiability Testing – SAT 2016 2016 Cham Springer 547-553
[20]
Hyvärinen, A.E.J., Marescotti, M., Sadigova, P., Chockler, H., Sharygina, N.: Lookahead-based SMT solving. In: Barthe, G., Sutcliffe, G., Veanes, M. (eds.) 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-22. EPiC Series in Computing, Awassa, Ethiopia, 16–21 November 2018, vol. 57, pp. 418–434. EasyChair (2018).
[21]
Komuravelli A, Gurfinkel A, and Chaki S SMT-based model checking for recursive programs Formal Meth. Syst. Des. 2016 48 175-205
[22]
Konnov I Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (eds):Handbook of model checking Formal Aspects Comput. 2019 31 4 455-456
[23]
McMillan KL Hunt WA and Somenzi F Interpolation and SAT-based model checking Computer Aided Verification 2003 Heidelberg Springer 1-13
[24]
McMillan KL Halbwachs N and Zuck LD Applications of Craig interpolants in model checking Tools and Algorithms for the Construction and Analysis of Systems 2005 Heidelberg Springer 1-12
[25]
McMillan KL Ball T and Jones RB Lazy abstraction with interpolants Computer Aided Verification 2006 Heidelberg Springer 123-136
[26]
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, 18–22 June 2001, pp. 530–535. ACM (2001).
[27]
de Moura L and Bjørner N Ramakrishnan CR and Rehof J Z3: an efficient SMT solver Tools and Algorithms for the Construction and Analysis of Systems 2008 Heidelberg Springer 337-340
[28]
Nadel A and Ryvchin V Beyersdorff O and Wintersteiger CM Chronological backtracking Theory and Applications of Satisfiability Testing – SAT 2018 2018 Cham Springer 111-121
[29]
Oh C Heule M and Weaver S Between SAT and UNSAT: the fundamental difference in CDCL SAT Theory and Applications of Satisfiability Testing – SAT 2015 2015 Cham Springer 307-323
[30]
Otoni, R., Blicha, M., Eugster, P., Hyvärinen, A.E.J., Sharygina, N.: Theory-specific proof steps witnessing correctness of SMT executions. In: 58th ACM/IEEE Design Automation Conference, DAC 2021, San Francisco, CA, USA, 5–9 December 2021, pp. 541–546. IEEE (2021).
[31]
Silva, J.P.M., Sakallah, K.A.: Conflict analysis in search algorithms for satisfiability. In: Eigth International Conference on Tools with Artificial Intelligence, ICTAI ’96, Toulouse, France, 16–19 November 1996, pp. 467–469. IEEE Computer Society (1996).
[32]
Wetzler N, Heule MJH, and Hunt WA Sinz C and Egly U DRAT-trim: efficient checking and trimming using expressive clausal proofs Theory and Applications of Satisfiability Testing – SAT 2014 2014 Cham Springer 422-429
[33]
Xiao F, Li C-M, Luo M, Manyà F, Lü Z, and Li Yu A branching heuristic for SAT solvers based on complete implication graphs Sci. China Inf. Sci. 2019 62 7 72103:1-72103:13
Index Terms
- Picky CDCL: SMT-Solving with Flexible Literal Selection
Index terms have been assigned to the content through auto-classification.
Recommendations
Evaluation of SMT solvers in abstraction-based software model checking
LADC '22: Proceedings of the 11th Latin-American Symposium on Dependable ComputingThe verification of safety-critical software systems is an algorithmically complex task, which often utilizes SMT (Satisfiability Modulo Theory) solvers for computing abstractions and refinements. It follows that the performance of SMT solvers impacts ...
Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some theory or combination of theories; Verification Modulo Theories (VMT) is the problem of analyzing the reachability for ...
SMT-based variability analyses in FeatureIDE
VaMoS '20: Proceedings of the 14th International Working Conference on Variability Modelling of Software-Intensive SystemsHandling configurable systems with thousands of configuration options is a challenging problem in research and industry. One of the most common approaches to manage the configuration options of large systems is variability modelling. The verification ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Oct 2023
115 pages
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 27 July 2024
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 03 Jan 2025