UWSpace is currently experiencing technical difficulties resulting from its recent migration to a new version of its software. These technical issues are not affecting the submission and browse features of the site. UWaterloo community members may continue submitting items to UWSpace. We apologize for the inconvenience, and are actively working to resolve these technical issues.
 

MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers

Thumbnail Image

Files

machsmt_final.pdf (2.8 MB)

Date

2020

Authors

Scott, Joseph
Niemetz, Aina
Preiner, Mathias
Ganesh, Vijay

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

In this paper, we present MachSMT, an algorithm selection tool for state-of-the-art Satisfiability Modulo Theories (SMT) solvers. MachSMT supports the entirety of the logics within the SMT-LIB initiative. MachSMT uses machine learning to learn empirical hardness models (a mapping from SMT-LIB instances to solvers) for state-of-the-art SMT solvers to compute a ranking of which solver is most likely to solve a particular instance the fastest. We analyzed the performance of MachSMT on 102 logics/tracks of SMT-COMP 2019 and observe that it improves on competition winners in 49 logics (with up to 240% in performance for certain logics). MachSMT is clearly not a replacement for any particular SMT solver, but rather a tool that enables users to leverage the collective strength of the diverse set of algorithms implemented as part of these sophisticated solvers. Our MachSMT artifact is available at https://github.com/j29scott/MachSMT.

Description

Keywords

LC Keywords

Citation

URI

http://hdl.handle.net/10012/15755

Collections

Waterloo Research
Computer Science