SMTS


SMTS is a framework for organising and visualizing executions of SMT and PDR in distributed computing environments.  The design is based on a general parallelization technique that supports recursively combining algorithm portfolios and divide-and-conquer with the exchange of learned information.  In addition, it allows the user to visually inspect both the parallel execution and the instance structure, and supports interactive, high-level guidance of the algorithm through a web interface.

A PDF accompanying the virtual image and describing SMTS architecture is available at http://verify.inf.usi.ch/sites/default/files/smts_artifact.pdf

 

Instructions on how to compile smts are available from http://verify.inf.usi.ch/P3.
To run the system, type:
$  ./smts.py -g -o2 -d prova
 
GUI demo:
A visualisation of an SMT instance

Published papers:

  1. SMTS: Distributed, Visualized Constraint SolvingMatteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina, LPAR 2018: 534-542
  2. Search-Space Partitioning for Parallelizing SMT SolversAntti E. J. Hyvärinen, Matteo Marescotti, Natasha Sharygina, SAT 2015: 369-386
  3. Clause Sharing and Partitioning for Cloud-Based SMT SolvingMatteo Marescotti, Antti E. J. Hyvärinen, Natasha Sharygina, ATVA 2016: 428-443
  4. OpenSMT2: An SMT Solver for Multi-core and Cloud ComputingAntti E. J. Hyvärinen, Matteo Marescotti, Leonardo Alt, Natasha Sharygina, SAT 2016: 547-553