dc.contributor.author | Scott, Joseph | |
dc.contributor.author | Niemetz, Aina | |
dc.contributor.author | Preiner, Mathias | |
dc.contributor.author | Ganesh, Vijay | |
dc.date.accessioned | 2020-04-14 20:04:29 (GMT) | |
dc.date.available | 2020-04-14 20:04:29 (GMT) | |
dc.date.issued | 2020 | |
dc.identifier.uri | http://hdl.handle.net/10012/15755 | |
dc.description.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. | en |
dc.language.iso | en | en |
dc.relation.uri | https://github.com/j29scott/MachSMT | en |
dc.title | MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers | en |
dc.type | Preprint | en |
uws.contributor.affiliation1 | Faculty of Mathematics | en |
uws.contributor.affiliation2 | David R. Cheriton School of Computer Science | en |
uws.typeOfResource | Text | en |
uws.peerReviewStatus | Unreviewed | en |
uws.scholarLevel | Graduate | en |