Learning to Solve SMT Formulas Fast

Augment your SMT solver by learning to optimize its performance for your dataset of formulas.

Machine Learning + Synthesis

Learn strategy that is fast at solving formulas in your dataset

Usage

Augment state-of-the-art SMT solver with the learned strategy

Up to 100x Speed-up Over Z3 Solver

Download

Experiments

We learned strategies on five different benchmarks AProVE, lepzig, hycomp, core and Sage2. These contain formulas of varying complexity across 3 logics QF_NRA, QF_BV and QF_NIA. Below we provide runtime comparison of our learned strategies against the handcrafted strategy used by Z3 version 4.6.2. We provide more experiments in our paper.

Speed-up of learned strategy vs Z3 v4.6.2

Materials

Additional materials that describe the FastSMT tool in more detail

Team

Mislav Balunovic
Mislav Balunović

MSc Student
SRI Lab
ETH Zurich
Website

Pavol Bielik
Pavol Bielik

PhD Student
SRI Lab
ETH Zurich
Website

Martin Vechev
Martin Vechev

Professor
SRI Lab
ETH Zurich
Website

To Top