Improving complex SMT strategies with learning

Nicolás Gálvez Ramírez, Eric Monfroy, Frédéric Saubion, Carlos Castro

Research output: Contribution to journalArticle

Abstract

© 2019 The Authors. International Transactions in Operational Research © 2019 International Federation of Operational Research Societies Satisfiability modulo theory (SMT) solving strategies are composed of various components and parameters that can dramatically affect the performance of an SMT solver. Each of these elements includes a huge amount of options that cannot be exploited without expert knowledge. In this work, we analyze separately the different strategy components of the Z3 theorem prover, which is one of the most important solvers of the SMT community. We propose some rules for modifying components, parameters, and structures of solving strategies. Using these rules inside different engines leads to an automated strategy learning process which does not require any end-user expert knowledge to generate optimized strategies. Our algorithms and rules are validated by optimizing some solving strategies for some selected SMT logics. These strategies are then tested for solving some SMT library benchmarks issued from the SMT competitions. The strategies we automatically generated turn out to be very efficient.
Original languageEnglish
Pages (from-to)1162-1188
Number of pages27
JournalInternational Transactions in Operational Research
DOIs
Publication statusPublished - 1 Mar 2020

Fingerprint Dive into the research topics of 'Improving complex SMT strategies with learning'. Together they form a unique fingerprint.

  • Cite this