Dynamic Algorithm Selection for SMT

This paper presents MachSMT, an algorithm selection tool for Satisfiability Modulo Theories (SMT) solvers. MachSMT supports the entirety of the SMT-LIB language and standardized SMT-LIB theories, and is easy to extend with support for new theories. Mach-SMT deploys machine learning (ML) methods to construct both empirical hardness models (EHMs) and pairwise ranking comparators (PWCs) over state-of-the-art SMT solvers. Given an input formula in SMT-LIB format, MachSMT leverages these learnt models to output a ranking of solvers based on predicted runtimes. We provide an extensive empirical evaluation of Mach-SMT to demonstrate the efficiency and efficacy of Mach-SMT over three broad usage scenarios on theories and theory combinations of practical relevance (e.g., bitvectors, (non-)linear integer and real arithmetic, arrays, and floating-point arithmetic). First, we deploy Mach-SMT on state-of-the-art solvers in SMT-COMP 2019 and 2020. We observe MachSMT frequently improves on the best performing solvers in the competition, winning 57 divisions outright, with up to a 99.4% improvement in PAR-2 score. Second, we evaluate MachSMT to select configurations from a single underlying solver. We observe that MachSMT solves 898 more benchmarks and up to a 93.4% improvement in PAR-2 score across 23 configurations of the SMT solver cvc5. Last, we evaluate MachSMT on domain-specific problems, namely net-This work was supported in part by DARPA (award no. FA8650-18-2-7861) and ONR (award no. N68335-17-C-0558).