parSAT: Parallel Solving of Floating-Point Satisfiability
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911165067558912 |
|---|---|
| author | Krahl, Markus Güdemann, Matthias Wallentowitz, Stefan |
| author_facet | Krahl, Markus Güdemann, Matthias Wallentowitz, Stefan |
| contents | Satisfiability-based verification techniques, leveraging modern Boolean satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers, have demonstrated efficacy in addressing practical problem instances within program analysis. However, current SMT solver implementations often encounter limitations when addressing non-linear arithmetic problems, particularly those involving floating point (FP) operations. This poses a significant challenge for safety critical applications, where accurate and reliable calculations based on FP numbers and elementary mathematical functions are essential.
This paper shows how an alternative formulation of the satisfiability problem for FP calculations allows for exploiting parallelism for FP constraint solving. By combining global optimization approaches with parallel execution on modern multi-core CPUs, we construct a portfolio-based semi-decision procedure specifically tailored to handle FP arithmetic. We demonstrate the potential of this approach to complement conventional methods through the evaluation of various benchmarks. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_16237 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | parSAT: Parallel Solving of Floating-Point Satisfiability Krahl, Markus Güdemann, Matthias Wallentowitz, Stefan Logic in Computer Science Satisfiability-based verification techniques, leveraging modern Boolean satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers, have demonstrated efficacy in addressing practical problem instances within program analysis. However, current SMT solver implementations often encounter limitations when addressing non-linear arithmetic problems, particularly those involving floating point (FP) operations. This poses a significant challenge for safety critical applications, where accurate and reliable calculations based on FP numbers and elementary mathematical functions are essential. This paper shows how an alternative formulation of the satisfiability problem for FP calculations allows for exploiting parallelism for FP constraint solving. By combining global optimization approaches with parallel execution on modern multi-core CPUs, we construct a portfolio-based semi-decision procedure specifically tailored to handle FP arithmetic. We demonstrate the potential of this approach to complement conventional methods through the evaluation of various benchmarks. |
| title | parSAT: Parallel Solving of Floating-Point Satisfiability |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2509.16237 |