MedleySolver: Online SMT Algorithm Selection

Nikhil Pimpalkhare, Federico Mora, Elizabeth Polgreen, Sanjit A. Seshia

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing - SAT 2021
Subtitle of host publication24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings
EditorsChu-Min Li, Felip Manyà
Place of PublicationCham
PublisherSpringer International Publishing Switzerland
Pages453-470
Number of pages18
ISBN (Electronic)978-3-030-80223-3
ISBN (Print)978-3-030-80222-6
DOIs
Publication statusPublished - 2 Jul 2021
Event24th International Conference on Theory and Applications of Satisfiability Testing - Barcelona, Spain
Duration: 5 Jul 20219 Jul 2021
https://www.iiia.csic.es/sat2021/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Cham
Volume12831
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference24th International Conference on Theory and Applications of Satisfiability Testing
Abbreviated titleSAT 2021
Country/TerritorySpain
CityBarcelona
Period5/07/219/07/21
Internet address

Cite this