Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards SMT Solver Stability via Input Normalization

Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark Barrett

TL;DR

This work addresses the stability problem of SMT solvers under small, semantics-preserving input mutations by proposing an input normalization strategy. It formalizes the mutation space, proves that exact normalization is GI-hard, and presents a practical approximate algorithm that sorts, renames, and reorders assertions using patterns and super-patterns, with additional optimizations for large benchmarks. Empirical results on SMT-LIB and Mariposa benchmarks show that normalization substantially reduces runtime variability (MAD) while incurring minimal overhead, and that high normalization effectiveness is achievable for many inputs. The approach is solver-agnostic and has potential applications in preprocessing, caching, and improved usability of SMT-based workflows.

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.

Towards SMT Solver Stability via Input Normalization

TL;DR

This work addresses the stability problem of SMT solvers under small, semantics-preserving input mutations by proposing an input normalization strategy. It formalizes the mutation space, proves that exact normalization is GI-hard, and presents a practical approximate algorithm that sorts, renames, and reorders assertions using patterns and super-patterns, with additional optimizations for large benchmarks. Empirical results on SMT-LIB and Mariposa benchmarks show that normalization substantially reduces runtime variability (MAD) while incurring minimal overhead, and that high normalization effectiveness is achievable for many inputs. The approach is solver-agnostic and has potential applications in preprocessing, caching, and improved usability of SMT-based workflows.

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.

Paper Structure

This paper contains 15 sections, 6 theorems, 2 equations, 6 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background
  3. Formalization
  4. Complexity
  5. Anti-symmetric Operators
  6. Approximating a Normalization Algorithm
  7. Experiments
  8. Normalization Effectiveness
  9. Stability
  10. Code Optimizations
  11. Pattern Compression
  12. Super-pattern Computation
  13. Super-pattern Compression
  14. Conclusion
  15. Appendix

Key Result

Theorem 3.8

Function $\mathpzc{N}\xspace$ is normalizing.

Figures (6)

  • Figure 1: Running Example.
  • Figure 2: Two different mutated versions of the same assertions.
  • Figure 3: Original (top) and normalized (bottom) assertions.
  • Figure 4: Assertions sorted by pattern.
  • Figure 5: Assertions after sorting and renaming.
  • ...and 1 more figures

Theorems & Definitions (21)

  • Definition 3.1: Shuffle Set
  • Definition 3.2: Commutative Reordering Set
  • Definition 3.3: Pattern
  • Definition 3.4
  • Definition 3.5: Renaming
  • Definition 3.6: Normalizing Function
  • Definition 3.7: Normalizing Function
  • Theorem 3.8
  • Theorem 3.9
  • Definition 4.1: Role
  • ...and 11 more