Paper Info
Title
MedleySolver: Online SMT Algorithm Selection
Abstract
Satisfiability modulo theories (SMT) solvers implement a wide range of optimizations that are often tailored to a particular class of problems, and that differ significantly between solvers. As a result, one solver may solve a query quickly while another might be flummoxed completely. Predicting the performance of a given solver is difficult for users of SMT-driven applications, particularly when the problems they have to solve do not fall neatly into a well-understood category. In this paper, we propose an online algorithm selection framework for SMT called MedleySolver that predicts the relative performances of a set of SMT solvers on a given query, distributes time amongst the solvers, and deploys the solvers in sequence until a solution is obtained. We evaluate MedleySolver against the best available alternative, an offline learning technique, in terms of pure performance and practical usability for a typical SMT user. We find that with no prior training, MedleySolver solves 93.9% of the queries solved by the virtual best solver selector achieving 59.8% of the par-2 score of the most successful individual solver, which solves 87.3%. For comparison, the best available alternative takes longer to train than MedleySolver takes to solve our entire set of 2000 queries.
Year
DOI
Venue
2021
10.1007/978-3-030-80223-3_31
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, SAT 2021
DocType
Volume
ISSN
Conference
12831
0302-9743
Citations 
PageRank 
References 
0
0.34
0
Authors
4
Name
Order
Citations
PageRank
Nikhil Pimpalkhare100.34
Federico Mora201.69
Elizabeth Polgreen300.68
Sanjit A. Seshia42226168.09