Verified Linear Programming via Tolerance-Aware Precision Boosting
Abstract
Linear programming plays a fundamental role in computer science, with applications in optimization, formal verification, SMT solving, and numerous other domains. When exactness guarantees are required, numerical inaccuracies arising from floating-point arithmetic can compromise soundness, whereas exact rational arithmetic often incurs significant computational overhead. In this paper, we investigate the numerical stability of the simplex algorithm and establish conditions under which a precision-boosting floating-point implementation provably produces the same pivot decisions and final basis as an exact rational implementation, from which the final result is reconstructed and certified exactly. Our analysis shows that correctness depends on both arithmetic precision and a careful handling of numerical tolerances. Based on these results, we develop a tolerance-aware, precision-boosting simplex algorithm with formal correctness guarantees. Finally, we introduce a delta-complete termination criterion that allows the algorithm to terminate once certified upper and lower bounds on the optimal objective differ by at most a user-specified threshold delta, providing a certified, user-controlled optimality gap.
Related
- Integer linear programming based methods for computing the maximum chordal subgraph of an arbitrary graph
- Subgraph Isomorphism, Integer Linear Programming, and Lattices: A Linear Algebraic Framework
- Faster Linear Programming with √(rank) Linear System Solves
- Recent Developments in HPR Methods for Large-Scale Linear Programming
- Linear programming bounds for binary and ternary LCD Codes
BibTeX
@misc{casablanca2026verified,
title = {{Verified Linear Programming via Tolerance-Aware Precision Boosting}},
author = {Ernesto Casablanca and Martin Sidaway and Sadegh Soudjani and Paolo Zuliani},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2609.11721},
eprint = {2609.11721},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.11721},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Verified Linear Programming via Tolerance-Aware Precision Boosting
AU - Ernesto Casablanca
AU - Martin Sidaway
AU - Sadegh Soudjani
AU - Paolo Zuliani
PY - 2026
DA - 2026/10/29
PB - arXiv
DO - 10.48550/arxiv.2609.11721
UR - https://arxiv.org/abs/2609.11721
AB - Linear programming plays a fundamental role in computer science, with applications in optimization, formal verification, SMT solving, and numerous other domains. When exactness guarantees are required, numerical inaccuracies arising from floating-point arithmetic can compromise soundness, whereas exact rational arithmetic often incurs significant computational overhead. In this paper, we investigate the numerical stability of the simplex algorithm and establish conditions under which a precision-boosting floating-point implementation provably produces the same pivot decisions and final basis as an exact rational implementation, from which the final result is reconstructed and certified exactly. Our analysis shows that correctness depends on both arithmetic precision and a careful handling of numerical tolerances. Based on these results, we develop a tolerance-aware, precision-boosting simplex algorithm with formal correctness guarantees. Finally, we introduce a delta-complete termination criterion that allows the algorithm to terminate once certified upper and lower bounds on the optimal objective differ by at most a user-specified threshold delta, providing a certified, user-controlled optimality gap.
ER -