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

• Algorithm selection/solver selection
• SMT solving

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)