一句话：提出基于数学优化的 SMT 浮点约束求解器 Grater，求解数量媲美最强求解器且速度快一个数量级以上。
浮点约束的可满足性求解因不连续性和搜索复杂性而极具挑战，现有 SMT 求解器难以处理大规模复杂约束；近期基于数学优化（MO）的方法又受函数不连续、搜索不精确和可扩展性不足困扰。本文提出一种新的 MO 驱动方法并实现求解器 Grater。在 JFS 基准上，Grater 求解数量与 Bitwuzla 持平、比 CVC5 多一个，但中位求解时间比二者快 10 倍和 40 倍以上；在精选的 100 余个最难 FP SMT-LIB 基准上，求解数量与 Bitwuzla/CVC5 相同，平均时间快 10 倍以上，中位时间分别快 50 倍和 30 倍。代码与评测数据已开源。
The Satisfiability Modulo Theory (SMT) problem over floating-point operations presents a significant challenge. State-of-the-art SMT solvers often run into difficulties when dealing with large, complex floating-point constraints. Recently, a new approach to floating-point constraint solving emerges, utilizing mathematical optimization (MO) methods as an engine of their solving approach. Despite the novelty, these methods can fall short in both effectiveness and efficiency due to issues of the translated functions ( e.g ., discontinuity) and inherent limitations of their underlying MO method ( e.g ., imprecise search process, scalability issues). Driven by these weaknesses of prior solvers, this paper introduces a new MO-based approach that is shown highly potent in solving floating-point constraints. Specifically, on the benchmarks of JFS (a recent solver based on fuzzing), Grater, a realization of our approach, solves as many constraints as Bitwuzla and one more than CVC5 but runs over 10 times faster and over 40 times faster than Bitwuzla and CVC5 in median solving time across all benchmarks. It is worth mentioning that Bitwuzla and CVC5 are the strongest solvers for floating-point constraints according to results of the annual international SMT solver competition (SMT-COMP). Together, they have won all gold medals for QF_FPArith and FPArith divisions, which focus on floating-point constraints solving, over the past three years. To further evaluate Grater, we select over 100 most difficult benchmarks from the FP SMT-LIB, a logic regularly used in SMT-COMP. The difficulty is measured by the complexity of the composition ( e.g ., number of variables, clauses) and the interdependencies within constraints. Grater again solves the same number of constraints as Bitwuzla and CVC5 while running over 10 times faster than both solvers in average solving time, and over 50 times ( resp . 30 times) faster than Bitwuzla ( resp . CVC5) in median solving time. We release the source code of Grater, along with all evaluation data, including detailed comparisons of Grater against each baseline solver ( i.e ., Z3, CVC5, Bitwuzla, JFS, XSat, and CoverMe), at https://github.com/grater-exp/grater-experiment to facilitate reproducibility.
@article{paperbot3076,
title = {Solving Floating-Point Constraints with Continuous Optimization},
author = {Qian Chen and Chenqi Cui and Fengjuan Gao and Yu Wang and Ke Wang and Linzhang Wang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729279}
}