GradSAT：通过梯度归一化加速浮点 SMT 求解

研究人员提出 GradSAT 框架，将多任务学习与动态梯度归一化（GradNorm）引入基于优化的浮点 SMT 求解，解决复杂子句主导梯度导致的局部极小值问题。该框架在运行时平衡各子句梯度幅度，并通过 GPU 加速的 PyTorch 连续松弛优化与精确局部搜索组成两阶段混合管线。这种设计显著稳定了连续搜索动态，为复杂约束求解提供了高并行度架构。