Using Normalization to Improve SMT Solver Stability

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.