Scalable Floating-Point Satisfiability via Staged Optimization
Yuanzhuo Zhang, Zhoulai Fu, Binoy Ravindran
TL;DR
StageSAT tackles QF_FP satisfiability by decomposing the search into three progressively precise optimization stages. It begins with a fast projection-aided descent to steer toward feasibility, then employs a squared-ULP objective for bit-precise alignment, and finally performs a bounded n-ULP lattice refinement to snap to exact IEEE-754 models. The method guarantees SAT when a model is found and avoids false SAT through its representing-function design, while unsat-guess and timeout remain incomplete outcomes. Empirical results show StageSAT significantly improves scalability and accuracy over prior optimization-based solvers, delivering 99.4% recall with 0% false SAT and 5–10x speedups on challenging benchmarks, while remaining competitive with complete solvers. The work demonstrates that staged optimization can robustly bridge numerical search with bit-level correctness, offering a practical front-end to traditional SMT FP solving and improving coverage on large-scale FP problems.
Abstract
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 of increasing precision. It begins with a fast, projection-aided descent objective to guide the search toward a feasible region, proceeding to bit-level accuracy with ULP$^2$ optimization and a final $n$-ULP lattice refinement. By construction, the final stage uses a representing function that is zero if and only if a candidate satisfies all constraints. Thus, when optimization drives the objective to zero, the resulting assignment is a valid solution, providing a built-in guarantee of soundness. To improve search, StageSAT introduces a partial monotone descent property on linear constraints via orthogonal projection, preventing the optimizer from stalling on flat or misleading landscapes. Critically, this solver requires no heavy bit-level reasoning or specialized abstractions; 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 SMT-COMP'25 suites and difficult cases from prior work. StageSAT proved more scalable and accurate than state-of-the-art optimization-based alternatives. It solved strictly more formulas than any competing solver under the same time budget, finding most satisfiable instances without producing spurious models. This amounts to 99.4% recall on satisfiable cases with 0% false SAT, exceeding the reliability of prior optimization-based solvers. StageSAT also delivered significant speedups (often 5--10$\times$) over traditional bit-precise SMT and numeric solvers. These results demonstrate that staged optimization significantly improves performance and correctness of floating-point satisfiability solving.