PV2 MachSMTdecides which solver to call per instance based on pairwise ranking comparators

MachSMT is an algorithm selection tool for Satisfiability Modulo Theories (SMT) solvers, based on empirical hardness models inferred with machine learning

Application domain/field

Type of tool

Solver selector for SMT problems

Expected input

Input benchmark and its library files

Format:

SMT-LIB

Expected output

Ranking of solvers that are expected to have the lowest runtime

Internals

It uses empirical hardness models (EHMs) and pairwise ranking comparators (PWCs) to perform algorithm selection. To do this, it uses frequencies of grammatical constructs from the SMT-LIB language, an some other syntactical metrics. Uses Bitwuzla, COLIBRI, CVC4, MathSAT 5, Q3B, SPASS-SATT, Vampire, Yices, Z3.

Comments

There are in total 3 'tools' that are part of MachSMT, our description above focuses on the primary interface of MachSMT. There is also a tool for building MachSMT's database (machsmt_build), and a tool to evaluate the results of machsmt_build under k-fold cross validation (machtsmt_eval)

Links

Last commit date

29 June 2021 (for the repository with the TACAS '21 artifact)

Related papers

https://doi.org/10.1007/978-3-030-72013-1_16 (TACAS '21)

Last publication date

23 March 2021

Related tools

SATzilla

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.