“Towards SMT Solver Stability via Input Normalization” by Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, and Clark Barrett. In Proceedings of the 25^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '25), (Ahmed Irfan and Daniela Kaufmann, eds.), Oct. 2025, pp. 84-93. Menlo Park, CA, USA.
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.
BibTeX entry:
@inproceedings{APN+25,
author = {Daneshvar Amrollahi and Mathias Preiner and Aina Niemetz and
Andrew Reynolds and Moses Charikar and Cesare Tinelli and Clark
Barrett},
editor = {Ahmed Irfan and Daniela Kaufmann},
title = {Towards SMT Solver Stability via Input Normalization},
booktitle = {Proceedings of the {\it 25^{th}} International Conference
on Formal Methods In Computer-Aided Design (FMCAD '25)},
pages = {84--93},
publisher = {TU Wien Academic Press},
month = oct,
year = {2025},
doi = {10.34727/2025/isbn.978-3-85448-084-6_14},
note = {Menlo Park, CA, USA},
url = {https://repositum.tuwien.at/handle/20.500.12708/219542}
}
(This webpage was created with bibtex2web.)