Scalable Floating-Point Satisfiability via Staged Optimization

This work introduces StageSAT, a new approach to solving floating-point satisfiability that bridges SMT solving with numerical optimization. StageSAT reframes a floating-point formula as a series of optimization problems in three stages, each with increasing precision. It begins with a fast, projection-aided descent objective to efficiently guide the search toward a feasible region, then proceeds to bit-level accuracy with ULP 2 optimization and a final 𝑛-ULP lattice refinement to ensure correctness. By construction, the final stage uses a representing function that evaluates to zero if and only if a candidate satisfies all constraints. Thus, whenever optimization drives the final-stage objective to zero, the resulting assignment is a valid solution, providing a built-in guarantee of soundness (no spurious SAT results). To further improve the search, StageSAT introduces a partial monotone descent property on linear constraints via an orthogonal projection technique, which prevents the optimizer from stalling on flat or misleading objective landscapes. Critically, this solver requires no heavy bit-level reasoning or specialized abstractions of floating-point arithmetic; it treats complex arithmetic as a black-box, using runtime evaluations to navigate the input space.

We implement StageSAT and evaluate it on extensive benchmarks, including the SMT-COMP'25 floatingpoint suites and difficult cases from prior work. In our experiments, StageSAT proved both more scalable and more accurate than state-of-the-art optimization-based alternatives. It solved strictly more formulas than any competing solver under the same time budget -in fact, StageSAT found most of the satisfiable instance in our benchmarks and never produced a spurious model for an unsatisfiable formula. This amounts to 99.4% recall on satisfiable cases with 0% false SAT in our benchmarks, exceeding the reliability of prior optimization-based solvers we tested. StageSAT also delivered significant speedups (often 5-10× faster) over traditional bit-precise SMT solvers and earlier numeric solvers. These results demonstrate that our staged optimization strategy can significantly improve both the performance and correctness of floating-point satisfiability solving. To facilitate reproduction, we provide an anonymized artifact (implementation, benchmarks, and evaluation results) as supplementary material in the submission system.