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.

翻译：本文提出StageSAT，一种解决浮点可满足性问题的新方法，它将SMT求解与数值优化相结合。StageSAT将浮点公式重构为三个精度递增阶段的序列优化问题。该方法首先采用快速的投影辅助下降目标函数引导搜索进入可行域，随后通过ULP$^2$优化实现比特级精度，最终进行$n$-ULP格点精细化。在构造上，最终阶段使用的表示函数当且仅当候选解满足所有约束时取值为零。因此当优化过程将目标函数驱动至零时，所得赋值即为有效解，这提供了内在的正确性保证。为改进搜索性能，StageSAT通过正交投影在线性约束上引入部分单调下降特性，防止优化器在平坦或误导性曲面上停滞。关键的是，该求解器无需繁重的比特级推理或专用抽象机制；它将复杂算术运算视为黑箱，通过运行时评估来探索输入空间。我们实现了StageSAT并在广泛基准测试中进行了评估，包括SMT-COMP'25测试集及先前研究中的困难案例。StageSAT被证明比当前最先进的基于优化的替代方案更具可扩展性和精确性。在相同时间预算下，它严格求解了比任何竞争求解器更多的公式，且对大多数可满足实例的求解均未产生伪模型。这相当于在可满足案例中实现了99.4%的召回率且误报率为0%，超越了先前基于优化的求解器的可靠性。StageSAT相较于传统比特精度SMT求解器与数值求解器也实现了显著加速（通常达5--10$\times$）。这些结果表明分阶段优化能显著提升浮点可满足性求解的性能与正确性。