MedleySolver: Online SMT Algorithm Selection
Nikhil Pimpalkhare, Federico Mora, Elizabeth Polgreen, and Sanjit A. Seshia. MedleySolver: Online SMT Algorithm Selection. In 24th International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 453–470, Lecture Notes in Computer Science 12831, Springer, 2021.
Download
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.
BibTeX
@inproceedings{pimpalkhare-sat21, author = {Nikhil Pimpalkhare and Federico Mora and Elizabeth Polgreen and Sanjit A. Seshia}, title = {{MedleySolver}: Online {SMT} Algorithm Selection}, booktitle = {24th International Conference on Theory and Applications of Satisfiability Testing (SAT)}, series = {Lecture Notes in Computer Science}, volume = {12831}, pages = {453--470}, publisher = {Springer}, year = {2021}, 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.}, }