PaperlayerView exact revision on arXiv

Source-linked AI summary

Verified Linear Programming through Tolerance-Aware Precision Boosting

Ernesto Casablanca, Martin Sidaway, Paolo Zuliani, Sadegh Soudjani

arXiv:2609.11721v2math.OCcs.NAmath.NA

TL;DR

Exact LP guarantees matter in verification and SMT solving, yet rational arithmetic can be costly. The paper proves conditions for tolerance-aware floating-point simplex to match exact simplex decisions and develops a δ-complete procedure that returns certified outcomes with a user-controlled optimality gap.

  • Problem

    Formal verification and SMT solvers need guaranteed LP correctness, but floating-point errors can compromise soundness and exact rational arithmetic can dominate runtime.

    Source: §1 · pp. 1–2

  • Method

    The paper derives Bartels–Golub error bounds, proves decision agreement for suitable problem-dependent precision and tolerance, and combines tolerance-aware simplex with Phase I and diagonal parameter enumeration.

    Source: §1 · p. 2, §5 · p. 13

  • Results

    The procedure can reproduce exact simplex decisions under suitable parameters and returns a δ-optimality certificate with gap at most user-specified δ, or a certified infeasibility or unboundedness result.

    Source: §4.2 · p. 12, §7 · p. 16

  • Takeaways & Limitations

    For rational LPs in standard form, users can obtain a certified, user-controlled optimality gap or a certified infeasibility or unboundedness result.

    Source: §7 · p. 16

    Efficiently computable non-trivial bounds for suitable precision and tolerance are not known; in practice, the paper uses a heuristic of decreasing both until the algorithm behaves correctly.

    Source: §4.1 · p. 11

Abstract

from arXiv · show

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.

1 Introduction

LP solvers are used across computing, but exact guarantees can require costly rational arithmetic where floating-point error is unacceptable. The paper develops theoretical guarantees for tolerance-aware precision boosting and a δ-complete simplex procedure.

1 Introduction

  • LP is used in optimization, software analysis, formal verification, and SMT solving, where increasing problem sizes sharpen the need for efficient and reliable solvers.Floating-point solvers are widely used when exactness is not required.Source: §1 · p. 1
  • Exact rational arithmetic supports verified LP outcomes, but its operation costs can dominate runtime, while floating-point solvers offer greater speed without the same guarantees.The paper defines verified outcomes as floating-point results validated with exact rational certificates; it notes that correctness proofs are not mechanized.Source: §1 · p. 2
  • Existing precision-boosting and iterative-refinement solvers work well in practice, but conditions guaranteeing that precision-boosting simplex reproduces exact simplex decisions had not been established.The paper addresses this theoretical gap for precision boosting based on the Bartels–Golub update.Source: §1 · p. 2
  • The paper derives error bounds and proves that suitable problem-dependent precision and tolerance values make floating-point simplex follow the exact rational pivot sequence and return the same solution.Its δ-complete procedure maintains exactly validated objective bounds and stops when their difference is at most user-specified δ.Source: §1 · p. 2

2 Preliminaries

The preliminaries establish notation and floating-point error conventions, review revised simplex and duality, define δ-optimal certificates, and introduce Bartels–Golub basis updates.

2 Preliminaries

  • The notation distinguishes rational scalars, matrices, and vectors; floating-point numbers use a radix, precision, significand, and bounded exponent.The stated floating-point error model applies to IEEE 754 arithmetic.Source: §2 · pp. 2–3, §2.1 · p. 3

2.1 Floating-point Arithmetic

  • Floating-point operations are modeled as exact operations perturbed by bounded relative error; the analysis assumes no overflow or underflow.For IEEE 754 double precision, unit roundoff is approximately 1.1 × 10^-16.Source: §2.1 · p. 3

2.2 Linear Programming and Simplex Algorithm

  • Revised simplex selects a basis, sets nonbasic variables to zero, and pivots to improve the objective; reduced costs and the ratio test guide choices, while no positive direction signals unboundedness.The standard-form LP assumes a full-row-rank constraint matrix.Source: §2.2 · pp. 4–5

2.3 Delta-Optimality Certificates

  • A δ-optimality certificate pairs primal- and dual-feasible solutions; their objective values bound the optimum, and δ-completeness also reports infeasibility or unboundedness.Exact optimality is the special case δ = 0.Source: §2.3 · p. 5

2.4 Bartels–Golub Basis Updates

  • Bartels–Golub updates factor the basis as Π^-1LU and use partial pivoting to restore triangular form after a simplex pivot.The update replaces a leaving column, appends the entering column, and adjusts the factorization; the paper notes that pivoting is vital for numerical stability.Source: §2.4 · p. 6

3 Stability Analysis of Bartels–Golub Basis Updates

The section derives rigorous error bounds for the Bartels–Golub basis update under floating-point arithmetic. The combined a priori backward error is O(ϵ), supporting stability when the iteration count is limited; sufficiently long runs require refactorization to avoid catastrophic error accumulation.

3 Stability Analysis of Bartels–Golub Basis Updates

  • The analysis updates Bartels’s error analysis by unifying addition and subtraction error factors, using one unit roundoff, and rigorously bounding ∥H(i)∥.The supplied passages also identify a more rigorous bound for ∥·∥1 than the original paper’s approximation.Source: §3 · p. 7
  • The asymptotic bounds treat the LP data and iteration index as constants, so hidden constants may depend on both but not on ϵ.The bounds are interpreted as ϵ →0.Source: §3 · pp. 7–8
  • ∥E(i)∥1 = O(ϵ) as ϵ →0, giving a linear-in-roundoff bound on the combined a priori backward error.The bound is for a fixed LP instance and iteration index; after sufficiently many iterations, the basis must be refactorized to avoid catastrophic error accumulation.Source: §3 · pp. 7–8

4 Tolerance-Aware Floating-Point Simplex

The section develops a floating-point simplex method whose numerical tolerances must be chosen consistently with arithmetic precision. Error bounds support conditions for matching exact rational decision steps, and the resulting algorithm terminates.

4 Tolerance-Aware Floating-Point Simplex

  • Tolerance τ must be chosen consistently with ϵ because simplex decisions compare computed quantities against numerical thresholds.The algorithm uses the Bartels–Golub update and Bland’s pivot rule, and its input requires τ > ϵ.Source: §4 · pp. 8–9, §4.1 · p. 10

4.1 Error Bounds for Simplex Computations

  • The error analysis accounts for input rounding, basis-update error, substitution error, and update-factor error when deriving conditions for correct decisions.The inputs are converted to dyadic floating-point values, and the passage gives O(ϵ) bounds for initial input-rounding errors.Source: §4.1 · pp. 9, 11
  • The authors report no efficiently computable nontrivial bounds for the instance-specific τ⋆ and ϵ⋆; decreasing an arbitrary starting pair is sufficient for most problems.The passage says that rigorous proofs for most theorems and lemmas are provided in Appendix B.Source: §4.1 · p. 11

4.2 Termination and Correctness

  • Lemma 5 establishes that Algorithm 1 always terminates, and the proof attributes this to Bland’s rule.The proof states that the number of iterations is bounded by 2n.Source: §4.2 · p. 12
  • The theorem guarantees that problem-dependent τ⋆ and ϵ⋆ make the floating-point algorithm match the exact algorithm at optimality, entering-variable, unboundedness, and leaving-variable decisions.The conditions depend on exact quantities across admissible bases, which the authors say are not explicitly computed.Source: §4.1 · p. 10, §4.2 · p. 12

5 Certifying Delta-Complete Linear Programming

Algorithm 3 combines a tolerance-aware simplex procedure with Phase I and diagonal enumeration of increasing precisions and decreasing tolerances to certify arbitrary rational LP instances. Exact rational validation supports its returned classifications and δ-optimality certificates, and the algorithm is proved to terminate and be correct.

5 Certifying Delta-Complete Linear Programming

  • Algorithm 3 combines Phase I with diagonal enumeration of increasing precisions and decreasing tolerances to handle arbitrary rational LP instances without a known feasible basis or parameter pair.A certified positive Phase-I optimum proves infeasibility; a certified zero optimum yields a feasible basis after artificial variables are removed.Source: §5 · p. 13
  • Exactly validated primal- and dual-feasible solutions certify a δ-optimal result when their objective-value gap is at most δ.The primal and dual values provide upper and lower bounds, respectively.Source: §5 · pp. 13–14
  • Algorithm 3 always terminates in finite time because diagonal enumeration eventually tests sufficiently accurate precision and tolerance values.The proof uses termination of Algorithm 1 and sequences of tolerances and unit roundoffs converging to zero.Source: §5 · p. 13
  • Theorem 5 states that Algorithm 3 always returns results correct under the paper’s δ-completeness definition.Each return is validated using exact rational arithmetic.Source: §5 · p. 13
  • Exact validation certifies infeasibility, unboundedness, and δ-optimality only when their respective conditions are met.Unboundedness requires an exactly primal-feasible basis, a negative reduced cost, and an exactly nonpositive direction.Source: §5 · pp. 13–14

6 Experimental Evaluation

The evaluation tests Delpi on numerically challenging Sloane–Stufken LP benchmarks and compares its running times with SoPlex. Delpi solves most instances faster than other solvers, while pure precision boosting improves SoPlex performance without changing outcomes.

6 Experimental Evaluation

  • Delpi extends QSoptex with a δ-complete mode and compares its running times with standalone SoPlex.The framework can be built with either QSoptex or SoPlex.Source: §6 · p. 14
  • Experiments use one core, 4 GB of memory, and a six-hour timeout per run on an AMD EPYC 9745 system.The platform runs RHEL 11.4.1.Source: §6 · p. 14
  • Delpi solves most of the 67 evaluated SK instances faster than other solvers; SoPlex’s pure precision-boosting configuration improves performance without changing outcomes.The instances are dense and feasible; Gurobi incorrectly declares all instances infeasible, while HiGHS cannot handle their large input coefficients.Source: §6 · p. 16
  • The benchmark set contains 67 SK instances generated by varying s1, s2, k1, k2, and t, and includes cases on which at least one solver reports a solution.The SK problems are dense, feasible, and numerically challenging for state-of-the-art floating-point solvers.Source: §6 · p. 16

7 Conclusion

The paper derives numerical foundations for reliable LP reasoning and builds a δ-complete simplex procedure for rational LPs in standard form. It reports that experimental evaluation on the numerically challenging Sloane–Stufken benchmarks demonstrates the approach’s practical potential.

7 Conclusion

  • A suitable problem-dependent precision and tolerance pair lets the floating-point procedure reproduce the decisions of its exact rational counterpart.The analysis derives a priori bounds on backward-error propagation for the Bartels–Golub update.Source: §7 · p. 16
  • The δ-complete procedure returns a certificate with optimality gap at most user-specified δ, or a certified infeasibility or unboundedness result.Source: §7 · p. 16
  • The guarantees are particularly relevant to SMT solvers for linear arithmetic, where incorrect numerical decisions can compromise verification soundness.Source: §7 · p. 16
  • Experiments on the numerically challenging Sloane–Stufken benchmark family demonstrate the approach’s practical potential.The paper identifies broader exploitation of the δ-complete algorithm, especially in SMT solving, as future work.Source: §7 · p. 16

A Experimental Results

The appendix describes performance profiles for the SK benchmarks and presents proof material for matrix product-difference and floating-point growth bounds. Its bounds cover triangular factors and Hessenberg factorization under partial pivoting.

A Experimental Results

B Proofs

B.1 Product-Difference Identity

  • The product-difference identity expresses a difference of matrix products as a sum of terms, each replacing one factor at a time.Source: §B.1 · p. 22

B.2 Floating-Point Growth Bounds for Gaussian Elimination

  • The growth-factor analysis for Gaussian elimination with partial pivoting extends its bounds to account for floating-point arithmetic.The analysis begins from the growth factor defined using matrices after successive elimination steps.Source: §B.2 · p. 22

B.3 Bounds for the Lower Triangular Factor

  • Partial pivoting bounds the elements of L by 1 before rounding, and the analysis derives an element-wise bound accounting for floating-point perturbation.Source: §B.3 · p. 23

B.4 Bounds for the Inverse Lower Triangular Factor

  • The inverse lower-triangular bound considers the worst case with non-diagonal entries set to -1 - ϵ.The diagonal entries of L are 1.Source: §B.4 · p. 23

B.5 Bounds for the Upper Triangular Factor

  • For general partial pivoting, the growth factor is bounded by 2^n - 1; floating-point analysis uses a per-step multiplier of 2(1 + ϵ)^3.Source: §B.5 · p. 23

B.6 Bounds for the Hessenberg Factorization

  • For upper Hessenberg matrices under partial pivoting, the growth factor is at most n, while floating-point perturbation remains at each step.The text notes that the perturbation factor remains (1 + ϵ)^3 per step.Source: §B.6 · p. 23

B.7 Backward Error in Solving with the Lower Triangular Factor

The appendix bounds floating-point error in triangular solves, update-factor operations, and basis updates. Its assumptions and intermediate bounds feed the weighted-norm and updated-basis analyses.

B.7 Backward Error in Solving with the Lower Triangular Factor

  • With partial pivoting, the elements of L are bounded by 1 + ϵ.The exact-arithmetic bound of 1 is perturbed by the floating-point model.Source: §B.7 · p. 24

B.8 Backward Error in Applying the Update Factors

  • The update-factor error analysis uses a product-difference identity, while permutation matrices add no rounding error because they are used directly.The identity expresses the difference of matrix products as a sum of terms differing in one factor.Source: §B.8 · p. 25

B.9 Bounds for the Inverse Updated Factorization

  • The inverse updated-factor analysis extends an element-wise bound across C(i)^−1 using the stronger factor (1 + ϵ)^3.The text says this inequality is made arbitrarily stronger than using (1 + ϵ).Source: §B.9 · pp. 28–29

B.10 Weighted-Norm Bound for the Update Factors

  • For the specified weighted norm, the update-factor bound is ∥T a∥⋆ ≤ 2(1 + ϵ)^3∥a∥⋆.The proof proceeds by induction on the square matrix size m.Source: §B.10 · p. 29

B.11 Backward Error in Solving with the Upper Triangular Factor

  • Applying update factors to H(i) computes U(i) through Gaussian elimination over an upper Hessenberg matrix.The analysis then bounds H(i) and the resulting triangular-factor computation.Source: §B.11 · p. 30

B.12 Backward Error of the Updated Basis

  • Each basis update removes the leaving-variable column and appends the entering column, with error terms tracked in the resulting updated basis.The factor update likewise drops the corresponding U(i) column and appends a computed column.Source: §B.12 · pp. 31–32

B.13 Proof of Lemma 2

The proof establishes invertibility of a perturbed matrix for sufficiently small ϵ and uses a Neumann-series expansion to bound the resulting error.

B.13 Proof of Lemma 2

  • Every term in the expansion is proportional to O(ϵ).The proof first uses bounded K and diagonal dominance of J = I + K for sufficiently small ϵ to establish invertibility.Source: §B.13 · pp. 32–33

B.14 Proof of Lemma 3

These proofs bound floating-point errors by O(ϵ) and use precision conditions relative to tolerance to preserve the simplex algorithm’s classifications and choices.

B.14 Proof of Lemma 3

  • Every component erj in the Lemma 3 proof is proportional to O(ϵ).The proof uses a known bound from.Source: §B.14 · p. 33

B.15 Proof of Lemma 4

  • The Lemma 4 proof concludes that ∥eu∥1 is proportional to O(ϵ).Its error bound is assembled from terms involving perturbations in d, zB, and η.Source: §B.15 · pp. 33–34

B.16 Proof of Theorem 3 - Optimality determination and entering variable choice

  • For optimality and entering-variable decisions, the proof requires reduced-cost error ∥er∥1 ≤ τ and a sufficiently small ϵ for each τ > 0.It bounds negative reduced costs across the finite set of possible bases to choose the tolerance condition.Source: §B.16 · p. 34

B.17 Proof of Theorem 3 - Unboundedness determination

  • For unboundedness decisions, the proof requires entering-coefficient error ∥ed∥1 ≤ τ and a sufficiently small ϵ for each τ > 0.The tolerance is constrained by the minimum positive coefficient across bases.Source: §B.17 · pp. 34–35

B.18 Proof of Theorem 3 - Leaving variable choice

  • Leaving-variable selection is preserved when the tolerance is small relative to the gap between distinct candidate ratios and their error.The proof defines β as the gap between the two smallest distinct candidate values, or infinity when there is only one.Source: §B.18 · pp. 35–36

B.19 Proof of Theorem 5

The proof verifies the algorithm’s infeasible and unbounded outputs and its δ-optimal termination result. The latter provides exact primal and dual feasible solutions whose objective gap is at most δ.

B.19 Proof of Theorem 5

  • An infeasible output certifies that the original LP is infeasible because the minimized sum of its infeasibilities is strictly positive.The proof establishes exact primal and dual feasibility for the auxiliary feasibility LP.Source: §B.19 · p. 36
  • An unbounded output gives an exactly primal-feasible basis and a negative reduced cost whose non-positive direction can increase the variable arbitrarily.Increasing that variable preserves primal feasibility.Source: §B.19 · p. 36
  • A δ-optimal output has exact primal and dual feasible solutions with objective gap ωU − ωL ≤ δ.Weak duality ensures ωU ≥ ωL.Source: §B.19 · p. 36
Loading 2609.11721v2…