Partitioning Strategies for Distributed SMT Solving

Amalee Wilson; Andres Noetzli; Andrew Reynolds; Byron Cook; Cesare Tinelli; Clark Barrett

doi:10.34727/2023/isbn.978-3-85448-060-0_28

Back

Partitioning Strategies for Distributed SMT Solving

Conference proceeding

Open access

Partitioning Strategies for Distributed SMT Solving

Amalee Wilson, Andres Noetzli, Andrew Reynolds, Byron Cook, Cesare Tinelli and Clark Barrett

2023 Formal Methods in Computer-Aided Design (FMCAD), pp.199-208

10/24/2023

DOI: 10.34727/2023/isbn.978-3-85448-060-0_28

Files and links (1)

url

https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_28View

Published (Version of record) Open Access

Abstract

For many users of Satisfiability Modulo Theories (SMT) solvers, the solver's performance is the main bottleneck in their application. One promising approach for improving performance is to leverage the increasing availability of parallel and cloud computing. However, despite many efforts, the best parallel approach to date consists of running a portfolio of solvers, meaning that performance is still limited by the best possible sequential performance. In this paper, we revisit divide-and-conquer approaches to parallel SMT, in which a challenging problem is partitioned into several subproblems. We introduce several new partitioning strategies and evaluate their performance, both alone as well as within portfolios, on a large set of difficult SMT benchmarks. We show that hybrid portfolios that include our new strategies can significantly outperform traditional portfolios for parallel SMT.

Cloud Computing

Benchmark testing

Design automation

Heuristic algorithms

Information sharing

Partitioning algorithms

Portfolios

Details

Title: Subtitle: Partitioning Strategies for Distributed SMT Solving
Creators: Amalee Wilson - Stanford University
Andres Noetzli - Cubist, Inc.,San Diego,USA
Andrew Reynolds - The University of Iowa,Iowa City,USA
Byron Cook - Amazon Web Services,Seattle,USA
Cesare Tinelli - The University of Iowa,Iowa City,USA
Clark Barrett - Stanford University
Resource Type: Conference proceeding
Publication Details: 2023 Formal Methods in Computer-Aided Design (FMCAD), pp.199-208
DOI: 10.34727/2023/isbn.978-3-85448-060-0_28
eISSN: 2708-7824
Publisher: FMCAD Association and individual authors
Grant note: Office of Science (10.13039/100006132) Advanced Scientific Computing Research (10.13039/100006192) U.S. Department of Energy (10.13039/100000015)
Language: English
Date published: 10/24/2023
Academic Unit: Computer Science
Record Identifier: 9984528100902771

Metrics

74 Record Views