Towards SMT Solver Stability via Input Normalization
Abstract
In many applications, SMT solvers are utilized to solve similar or identical tasks over time. Significant variations in performance due to small changes in the input are not uncommon and lead to frustration for users. This sort of stability problem represents an important usability challenge for SMT solvers. 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.
Cite
@article{arxiv.2410.22419,
title = {Towards SMT Solver Stability via Input Normalization},
author = {Daneshvar Amrollahi and Mathias Preiner and Aina Niemetz and Andrew Reynolds and Moses Charikar and Cesare Tinelli and Clark Barrett},
journal= {arXiv preprint arXiv:2410.22419},
year = {2025}
}