© 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.
|Number of pages||27|
|Journal||International Transactions in Operational Research|
|Publication status||Published - 1 Mar 2020|
Gálvez Ramírez, N., Monfroy, E., Saubion, F., & Castro, C. (2020). Improving complex SMT strategies with learning. International Transactions in Operational Research, 1162-1188. https://doi.org/10.1111/itor.12650