Preprint
Using Normalization to Improve SMT Solver Stability
ArXiv.org
Cornell University
10/29/2024
DOI: 10.48550/arxiv.2410.22419
Abstract
In many applications, SMT solvers are used to solve similar or identical tasks over time. When the performance of the solver varies significantly despite only small changes, this leads to frustration for users. This has been called the stability problem, and it represents an important usability challenge for SMT solvers. In this paper, we introduce an approach for mitigating the stability problem based on normalizing solver inputs. We show that a perfect normalizing algorithm exists but is computationally expensive. We then describe an approximate algorithm and evaluate it on a set of benchmarks from related work, as well as a large set of benchmarks sampled from SMT-LIB. Our evaluation shows that our approximate normalizer reduces runtime variability with minimal overhead and is able to normalize a large class of mutated benchmarks to a unique normal form.
Details
- Title: Subtitle
- Using Normalization to Improve SMT Solver Stability
- Creators
- Daneshvar Amrollahi - Stanford UniversityMathias Preiner - Stanford UniversityAina Niemetz - Stanford UniversityAndrew Reynolds - University of IowaMoses Charikar - Stanford UniversityCesare Tinelli - University of IowaClark Barrett - Stanford University
- Resource Type
- Preprint
- Publication Details
- ArXiv.org
- DOI
- 10.48550/arxiv.2410.22419
- ISSN
- 2331-8422
- Publisher
- Cornell University; Ithaca, New York
- Language
- English
- Date posted
- 10/29/2024
- Academic Unit
- Computer Science
- Record Identifier
- 9984742659902771
Metrics
69 Record Views