International Transactions in Operational Research

Improving complex SMT strategies with learning

Early View

Abstract 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.

Related Topics

Related Publications

Related Content

Site Footer


This website is provided by John Wiley & Sons Limited, The Atrium, Southern Gate, Chichester, West Sussex PO19 8SQ (Company No: 00641132, VAT No: 376766987)

Published features on are checked for statistical accuracy by a panel from the European Network for Business and Industrial Statistics (ENBIS)   to whom Wiley and express their gratitude. This panel are: Ron Kenett, David Steinberg, Shirley Coleman, Irena Ograjenšek, Fabrizio Ruggeri, Rainer Göb, Philippe Castagliola, Xavier Tort-Martorell, Bart De Ketelaere, Antonio Pievatolo, Martina Vandebroek, Lance Mitchell, Gilbert Saporta, Helmut Waldl and Stelios Psarakis.