GradSAT：用梯度归一化加速浮点可满足性求解

针对基于优化的 SMT 求解器受梯度支配问题，研究者提出 GradSAT 框架，将每条 SMT 子句视为独立的多任务学习任务，通过动态梯度归一化（GradNorm）在运行时平衡各子句梯度幅度。GradSAT 采用两阶段流水线：先用 GPU 加速的 PyTorch 后端结合符号编译与算子融合导航连续松弛，再交由位精确局部搜索求解精确赋值。