“SMT-D: New Strategies for Portfolio-Based SMT Solving” by Clark Barrett, Pei-Wei Chen, Byron Cook, Bruno Dutertre, Robert Jones, Nham Le, Andrew Reynolds, Kunal Sheth, Mike Whalen, and Chriss Stephens. In Proceedings of the 24^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '24), (Nina Narodytska and Philipp Rümmer, eds.), Oct. 2024, pp. 39-48. Prague, Czech Republic.
We introduce SMT-D, a tool for portfolio-based distributed SMT solving. We propose a general architecture consisting of two main components: (i) solvers extended with the capability of sharing and importing information on the fly while solving; and (ii) a central manager that orchestrates and monitors solvers while also deciding which information to share with which solvers. We introduce new information-sharing strategies based on the idea of maximizing the amount of useful diversity in the system. We show that on hard benchmarks from recent related work, SMT-D instantiated with the cvc5 SMT solver achieves significant speed-up over sequential performance, is competitive with existing portfolio approaches, and contributes a number of unique solutions.
BibTeX entry:
@inproceedings{BCC+24,
author = {Clark Barrett and Pei-Wei Chen and Byron Cook and Bruno
Dutertre and Robert Jones and Nham Le and Andrew Reynolds and
Kunal Sheth and Mike Whalen and Chriss Stephens},
editor = {Nina Narodytska and Philipp R{\"u}mmer},
title = {SMT-D: New Strategies for Portfolio-Based SMT Solving},
booktitle = {Proceedings of the {\it 24^{th}} International Conference
on Formal Methods In Computer-Aided Design (FMCAD '24)},
pages = {39--48},
publisher = {TU Wien Academic Press},
month = oct,
year = {2024},
doi = {10.34727/2024/isbn.978-3-85448-065-5_10},
note = {Prague, Czech Republic},
url = {https://repositum.tuwien.at/handle/20.500.12708/200777}
}
(This webpage was created with bibtex2web.)