Show simple item record

dc.contributor.authorScott, Joseph
dc.contributor.authorNiemetz, Aina
dc.contributor.authorPreiner, Mathias
dc.contributor.authorGanesh, Vijay
dc.date.accessioned2020-04-14 20:04:29 (GMT)
dc.date.available2020-04-14 20:04:29 (GMT)
dc.date.issued2020
dc.identifier.urihttp://hdl.handle.net/10012/15755
dc.description.abstractIn 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.isoenen
dc.relation.urihttps://github.com/j29scott/MachSMTen
dc.titleMachSMT: A Machine Learning-based Algorithm Selector for SMT Solversen
dc.typePreprinten
uws.contributor.affiliation1Faculty of Mathematicsen
uws.contributor.affiliation2David R. Cheriton School of Computer Scienceen
uws.typeOfResourceTexten
uws.peerReviewStatusUnrevieweden
uws.scholarLevelGraduateen


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record


UWSpace

University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages