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

[HTML] 

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.},
}