一句话：提出混合 SMT(NRA) 求解器 NRAgo，将梯度优化与代数求解结合，大幅加速可满足实例。
非线性实数算术（NRA）的可满足性问题是模型检测、程序分析与软件测试等重要应用的基础，但由于计算复杂度高，开发高效求解算法一直面临巨大挑战。本文提出混合 SMT(NRA) 求解器 NRAgo，将基于梯度的优化方法的高效性与代数求解算法的完备性相结合，从而显著改善许多可满足实例上的实际性能。实验在现有先进 SMT 求解器也难以处理的挑战性 SMT(NRA) 基准上进行评估，结果表明 NRAgo 取得了显著的加速效果。
The satisfiability problem modulo the nonlinear real arithmetic (NRA) theory serves as the foundation for a wide range of important applications, such as model checking, program analysis, and software testing. However, due to the high computational complexity, developing efficient solving algorithms for this problem has consistently presented a substantial challenge. We present a hybrid SMT(NRA) solver, called NRAgo, which combines the efficiency of gradient-based optimization method with the completeness of algebraic solving algorithm. With our approach, the practical performance on many satisfiable instances is substantially improved. The experimental evaluation shows that NRAgo achieves remarkable acceleration effects on a set of challenging SMT(NRA) benchmarks that are hard to solve for state-of-the-art SMT solvers.
@inproceedings{LiuLHHJZMZ23,
title = {NRAgo: Solving SMT(NRA) Formulas with Gradient-Based Optimization},
author = {Minghao Liu and Kunhang Lv and Pei Huang and Rui Han and Fuqi Jia and Yu Zhang and Feifei Ma and Jian Zhang},
booktitle = {ASE},
year = {2023},
doi = {10.1109/ase56229.2023.00013}
}