一句话：提出 StageSAT，用三阶段逐步提升精度的数值优化求解浮点可满足性，兼顾可扩展性与可靠性。
浮点可满足性求解通常依赖昂贵的位级推理或专门的浮点抽象，难以兼顾性能与正确性。本文提出 StageSAT，将浮点公式重构为三个精度递增的优化阶段：首先用投影辅助的下降目标快速引导搜索进入可行域，然后进行 ULP² 位级精度优化，最后用 n-ULP 格细化确保正确性。后两个阶段构造的表示函数当且仅当候选赋值满足所有约束时取零，因此优化到零即得到可靠解，从构造上保证无伪 SAT 结果。针对平坦或误导性目标景观，作者还引入线性约束上的部分单调下降性质与正交投影技术，避免优化器停滞。该方法将复杂算术视为黑盒，通过运行时求值导航输入空间，无需位级推理。在 SMT-COMP'25 浮点套件及已有困难实例上的实验表明，StageSAT 比现有基于优化的求解器更具可扩展性和准确性，SAT 召回率达 99.4%，且对不可满足公式不产生伪模型，相比传统位精确 SMT 求解器常有 5–10 倍加速。
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 units-in-the-last-place (ULP) 2 optimization and a final n -ULP lattice refinement to ensure correctness. By construction, the final two stages use a representing function that evaluates to zero if and only if a candidate satisfies all constraints. Thus, whenever optimization drives the bit-precise 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 floating-point 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 instances 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.
@article{paperbot3771,
title = {Scalable Floating-Point Satisfiability via Staged Optimization},
author = {Yuanzhuo Zhang and Zhoulai Fu and Binoy Ravindran},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808342}
}