可扩展的浮点可满足性求解 via 阶段优化
Scalable Floating-Point Satisfiability via Staged Optimization
AI总结：
StageSAT通过阶段优化方法提升浮点可满足性求解的性能和正确性，实现更高的可扩展性和准确性。
摘要：
本文介绍了StageSAT，一种新的求解浮点可满足性的方法，将SMT求解与数值优化相结合。StageSAT将浮点公式重新表述为三个精度递增阶段的优化问题。它首先使用快速的投影辅助下降目标引导搜索向可行区域发展，接着使用ULP²优化进行位级精度，最终进行n-ULP晶格细化。通过构造，最终阶段使用一个代表函数，当且仅当候选体满足所有约束时该函数为零。因此，当优化驱动目标为零时，得到的赋值是一个有效解，提供内置的正确性保证。为了提高搜索效率，StageSAT引入了通过正交投影在线性约束上实现的部分单调下降属性，防止优化器在平坦或误导的景观上停滞。关键的是，该求解器不需要重的位级推理或专门的抽象；它将复杂的算术视为黑箱，使用运行时评估来导航输入空间。我们实现了StageSAT并在广泛的基准测试中评估了它，包括SMT-COMP'25套件和先前工作的困难案例。StageSAT比最先进的基于优化的替代方法更具可扩展性和准确性。在相同的时间预算下，StageSAT解决了比任何竞争求解器更多的公式，大多数可满足实例无需产生虚假模型。这相当于在可满足案例中达到99.4%的召回率，0%的假阳性，超过了先前基于优化的求解器的可靠性。StageSAT还提供了显著的速度提升（通常5-10倍）超过传统的位精确SMT和数值求解器。这些结果表明，阶段优化显著提高了浮点可满足性求解的性能和正确性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
