AI 中文总结
针对浮点SMT求解中梯度支配导致的局部最优问题，提出GradSAT框架，将每个子句视为多任务学习任务，通过动态梯度归一化平衡梯度，结合GPU加速连续松弛与位精确局部搜索，实现稳健高效的求解。
AI 中文摘要
可满足性模理论（SMT）求解器是软件验证、程序分析和编译器测试的基础，特别是在无量词浮点（QF_FP）理论中。虽然近期基于优化的SMT求解器已成功将梯度下降应用于逻辑公式的连续松弛，但它们从根本上受到梯度支配现象的瓶颈限制，即一小部分困难子句劫持优化轨迹，阻止求解器满足更广泛的公式，并使其陷入局部最小值。为克服这一问题，我们提出了GradSAT，一个将基于优化的SMT求解与多任务学习（MTL）相结合的新颖框架。GradSAT将约束满足过程重新表述为将每个SMT子句视为独立的MTL任务。通过应用动态梯度归一化（GradNorm），GradSAT在运行时主动平衡所有子句的梯度幅度，系统地惩罚主导梯度并加速滞后子句，以确保均匀收敛。GradSAT通过一个高度优化的两阶段混合流水线实现这一点。首先，一个利用符号编译和算子融合的GPU加速PyTorch后端将连续松弛导航至高质量盆地。其次，候选赋值被移交给位精确的局部搜索引擎，以快速解析精确、严格的赋值。通过稳定连续搜索动态，GradSAT缓解了先前基于梯度的求解器的脆弱性，并为复杂约束求解提供了稳健、高度可并行化的架构。
英文摘要
Satisfiability Modulo Theories (SMT) solvers are foundational to software verification, program analysis, and compiler testing, particularly over the theory of Quantifier-Free Floating-Point (QF_FP). While recent optimization-based SMT solvers have successfully applied gradient descent to continuous relaxations of logical formulas, they are fundamentally bottlenecked by gradient domination, a phenomenon where a small subset of difficult clauses hijacks the optimization trajectory, preventing the solver from satisfying the broader formula and trapping it in local minima. To overcome this, we present GradSAT, a novel framework that bridges optimization-based SMT solving with Multi-Task Learning (MTL). GradSAT reformulates the constraint satisfaction process by treating each SMT clause as an independent MTL task. By applying dynamic gradient normalization (GradNorm), GradSAT actively balances the gradient magnitudes across all clauses at runtime, systematically penalizing dominant gradients and accelerating lagging clauses to ensure uniform convergence. GradSAT implements this through a highly optimized, two-stage hybrid pipeline. First, a GPU-accelerated PyTorch backend leveraging symbolic compilation and operator fusion navigates the continuous relaxation to a high-quality basin. Second, the candidate assignment is handed off to a bit-precise local search engine to rapidly resolve the exact, rigorous assignment. By stabilizing the continuous search dynamics, GradSAT mitigates the brittleness of prior gradient-based solvers and provides a robust, highly parallelizable architecture for complex constraint solving.
