Towards SMT Solver Stability via Input Normalization

TL;DR

This paper presents an input normalization approach to improve the stability of SMT solver performance, reducing variability with minimal overhead by approximating a perfect normalization algorithm.

Contribution

It introduces an approximate normalization algorithm that mitigates SMT solver stability issues, addressing a significant usability challenge.

Findings

Reduces runtime variability in SMT solving

Normalizes a large class of mutated benchmarks

Minimal overhead introduced by the normalization process

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.