GradSAT Accelerates Floating-Point Satisfiability Solving with Gradient Normalization

Summary

Satisfiability Modulo Theories solvers are widely used in software verification, program analysis, and compiler testing, including quantifier-free floating-point constraints. The paper identifies gradient domination as a bottleneck in optimization-based SMT solvers: a small number of difficult clauses can control the optimization trajectory, leaving other clauses unsatisfied and trapping the search in local minima. It introduces GradSAT, which treats each SMT clause as an independent multi-task learning task and uses dynamic GradNorm normalization to balance gradient magnitudes during optimization. The system has a two-stage hybrid design. A GPU-accelerated PyTorch backend uses symbolic compilation and operator fusion to find a high-quality region in the continuous relaxation, after which a bit-precise local-search engine finds an exact assignment. The authors present this stabilization strategy as a way to make gradient-based solving more robust and highly parallelizable for complex floating-point constraints.