Towards SMT Solver Stability via Input Normalization
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918020941611008 |
|---|---|
| author | Amrollahi, Daneshvar Preiner, Mathias Niemetz, Aina Reynolds, Andrew Charikar, Moses Tinelli, Cesare Barrett, Clark |
| author_facet | Amrollahi, Daneshvar Preiner, Mathias Niemetz, Aina Reynolds, Andrew Charikar, Moses Tinelli, Cesare Barrett, Clark |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_22419 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Towards SMT Solver Stability via Input Normalization Amrollahi, Daneshvar Preiner, Mathias Niemetz, Aina Reynolds, Andrew Charikar, Moses Tinelli, Cesare Barrett, Clark Logic in Computer Science 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. |
| title | Towards SMT Solver Stability via Input Normalization |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2410.22419 |