Towards SMT Solver Stability via Input Normalization

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

doi:10.34727/2025/isbn.978-3-85448-084-6_14

Back

Towards SMT Solver Stability via Input Normalization

Conference proceeding

Open access

Towards SMT Solver Stability via Input Normalization

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

2025 Formal Methods in Computer-Aided Design (FMCAD), pp.84-93

10/06/2025

DOI: 10.34727/2025/isbn.978-3-85448-084-6_14

Files and links (1)

url

https://doi.org/10.34727/2025/isbn.978-3-85448-084-6_14View

Published (Version of record) Open Access

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.

Logic

Approximation algorithms

Benchmark testing

Design automation

Prediction algorithms

Runtime

Thermal stability

Usability

Details

Title: Subtitle: Towards SMT Solver Stability via Input Normalization
Creators: Daneshvar Amrollahi - Stanford University
Mathias Preiner - Stanford University
Aina Niemetz - Stanford University
Andrew Reynolds - The University of Iowa,Iowa City,USA
Moses Charikar - Stanford University
Cesare Tinelli - The University of Iowa,Iowa City,USA
Clark Barrett - Stanford University
Resource Type: Conference proceeding
Publication Details: 2025 Formal Methods in Computer-Aided Design (FMCAD), pp.84-93
DOI: 10.34727/2025/isbn.978-3-85448-084-6_14
eISSN: 2708-7824
Publisher: Authors and FMCAD Association (non-exclusive)
Grant note: #2303489 / National Science Foundation (10.13039/100000001)
Language: English
Date published: 10/06/2025
Academic Unit: Computer Science
Record Identifier: 9985139273602771

Metrics

3 Record Views