# Towards SMT Solver Stability via Input Normalization

arXiv: https://arxiv.org/abs/2410.22419 · HTML: https://mlsanity.com/paper/2410.22419/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Oct 2024.

## Built on by (most cited first, 1 of 1)

- [Scaling Observation-aware Planning in Uncertain Domains](https://mlsanity.com/paper/2605.22364/) (2026)

## Abstract (arXiv)

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.