“Partitioning Strategies for Distributed SMT Solving” by Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, and Clark Barrett. In Proceedings of the 23^rd International Conference on Formal Methods In Computer-Aided Design (FMCAD '23), (Alexander Nadel and Kristin Yvonne Rozier, eds.), Oct. 2023, pp. 199-208. Ames, IA.
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.
BibTeX entry:
@inproceedings{WNR+23,
author = {Amalee Wilson and Andres N{\"o}tzli and Andrew Reynolds and
Byron Cook and Cesare Tinelli and Clark Barrett},
editor = {Alexander Nadel and Kristin Yvonne Rozier},
title = {Partitioning Strategies for Distributed {SMT} Solving},
booktitle = {Proceedings of the {\it 23^{rd}} International Conference
on Formal Methods In Computer-Aided Design (FMCAD '23)},
pages = {199--208},
publisher = {TU Wien Academic Press},
month = oct,
year = {2023},
doi = {10.34727/2023/isbn.978-3-85448-060-0_28},
note = {Ames, IA},
url = {https://repositum.tuwien.at/handle/20.500.12708/188827}
}
(This webpage was created with bibtex2web.)