<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Joseph Scott, Aina Niemetz, Mathias Preiner, and Vijay Ganesh</article-title>
      </title-group>
      <pub-date>
        <year>2020</year>
      </pub-date>
      <abstract>
        <p />
      </abstract>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>-</title>
      <p>In this paper, we present MachSMT, an algorithm selection tool for state-of-the-art
Satis ability 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.</p>
    </sec>
  </body>
  <back>
    <ref-list />
  </back>
</article>