通过梯度归一化加速浮点可满足性求解

arXiv:2610.08808v1 公告类型：新 摘要：可满足性模理论 (SMT) 求解器是软件验证、程序分析和编译器测试的基础，特别是在无量词浮点 (QF_FP) 理论方面。虽然最近基于优化的 SMT 求解器已成功地将梯度下降应用于逻辑公式的连续松弛，但它们从根本上受到梯度支配的瓶颈，梯度支配是一种现象，即一小部分困难子句劫持优化轨迹，阻止求解器满足更广泛的公式并将其陷入局部最小值。为了克服这个问题，我们提出了 GradSAT，这是一种将基于优化的 SMT 求解与多任务学习 (MTL) 结合起来的新颖框架。 GradSAT 通过将每个 SMT 子句视为独立的 MTL 任务来重新制定约束满足流程。通过应用动态梯度归一化（GradNorm），GradSAT 在运行时主动平衡所有子句的梯度大小，系统地惩罚主导梯度并加速滞后子句，以确保均匀收敛。 GradSAT 通过高度优化的两级混合管道来实现这一点。首先，GPU 加速的 PyTorch 后端利用符号编译和运算符融合将连续松弛导航到高质量盆地。其次，候选作业被移交给位精确的本地搜索引擎，以快速解决准确、严格的作业。通过稳定连续搜索动态，GradSAT 减轻了先前基于梯度的求解器的脆弱性，并为复杂约束求解提供了强大的、高度并行化的架构。