Continuous Optimization for Satisfiability Modulo Theories on Linear Real Arithmetic

Yunuo Cen; Daniel Ebler; Xuanyao Fong

cs.AIMar 24, 2026

Continuous Optimization for Satisfiability Modulo Theories on Linear Real Arithmetic

Authors: Yunuo Cen, Daniel Ebler, Xuanyao Fong

Organizations: Department of Electrical and Computer Engineering, National University of Singapore, Singapore · School of Computing and Data Science, The University of Hong Kong, Hong Kong, China

Abstract

Efficient solutions for satisfiability modulo theories (SMT) are integral in industrial applications such as hardware verification and design automation. Existing approaches are predominantly based on conflict-driven clause learning, which is structurally difficult to parallelize and therefore scales poorly. In this work, we introduce FourierSMT as a scalable and highly parallelizable continuous-variable optimization framework for SMT. We generalize the Walsh-Fourier expansion (WFE), called extended WFE (xWFE), from the Boolean domain to a mixed Boolean-real domain, which allows the use of gradient methods for SMT. This addresses the challenge of finding satisfying variable assignments to high-arity constraints by local updates of discrete variables. To reduce the evaluation complexity of xWFE, we present the extended binary decision diagram (xBDD) and map the constraints from xWFE to xBDDs. We then show that sampling the circuit-output probability (COP) of xBDDs under randomized rounding is equivalent to the expectation value of the xWFEs. This allows for efficient computation of the constraints. We show that the reduced problem is guaranteed to converge and preserves satisfiability, ensuring the soundness of the solutions. The framework is benchmarked for large-scale scheduling and placement problems with up to 10,000 variables and 700,000 constraints, achieving 8-fold speedups compared to state-of-the-art SMT solvers. These results pave the way for GPU-based optimization of SMTs with continuous systems.

Figures & tables

Figure 1: The overall flow of FourierSMT . (a) A variety of combinatorial problems target to optimize propositional and real variables. (b) These problems can be encoded using an SMT(LRA) formula, which is a SAT formula with additional LRA theory. (c) A constraint in the SMT(LRA) formula can be transformed into a polynomial called xWFE. The amplitudes show the coefficients of the xWFE, described in Eq. ( 2 ). (d) The expectation of the xWFE can be obtained by randomized rounding on the Boolean variable and the Gaussian sampling on the real variables. (e) However, the xWFE has an exponential number of terms. We show that the circuit output probability of xBDDs is equivalent to the expectation of the xWFE. This avoids state enumeration and thereby preserves computation efficiency. (f) We recover the minima of the original function by annealing of the sampling parameters, gradually restoring the original piecewise objective.

Figure 2: Optimization trajectories and energy landscapes under different sampling parameters. The number of gradient steps required to reach an $\epsilon$ -projected critical point is shown for $\epsilon=10^{-2}$ . (a) The colorbar indicates the inverse sampling parameter ${1}/{\sigma}$ . 1. When $\sigma\to\infty$ ( i.e. , ${1}/{\sigma}=0$ ), the gradient with respect to the real-valued variables $y$ vanishes, as the smoothing effect becomes arbitrarily strong. 2. Moderately large sampling parameters, i.e. , ${1}/{\sigma}\in\{0.1,\ldots,0.5\}$ , yield slower convergence to the global minimum. 3. In contrast, smaller values of $\sigma$ , corresponding to ${1}/{\sigma}\in\{0.6,\ldots,2.0\}$ , lead to faster convergence to a local minimum. 4. The dashed gradient-colored curve denotes the annealing schedule, in which ${1}/{\sigma}$ is gradually increased in increments of 0.1, achieving both rapid convergence and a final solution close to the global optimum. (b) Visualization of the objective landscape and the corresponding optimization trajectory for different $\sigma$ . The horizontal and the vertical axes of each subplot correspond to $x$ and $y$ in the domain $[-1,1]$ . Each subplot shows the smoothed objective ( $\mathcal{C}_{\sigma}$ , greyscale background) and the path taken by the gradient descent (colorline, the color refers to the color bar in panel (a) as $1/\sigma$ ). The optimization trajectories start at the same initial point (black edge circle) and follow the gradients to global (red edge circle) or local minima (green edge circle).

Figure 3: Benchmark results on random instances with mixed Boolean-real hybrid constraints. (a) The results show the number of solved instances and runtime efficiency (average PAR-2 score of the solvers). It can be seen that the virtual-best solver ( VBS1 , including FourierSMT ) is 62.45 $\times$ faster and solves 50 more instances than its counterpart ( VBS2 , excluding FourierSMT ). The 20 easy instances (small-scale) are solved more efficiently by CDCL( $\mathcal{T}$ ) solvers, whereas all larger instances are solved most efficiently by FourierSMT . This pattern demonstrates that FourierSMT is substantially more scalable. (b) The average gradient computation time of FourierSMT using CPU (AMD EPYC 9654) and GPU (NVIDIA L40S). For each problem instance, we measure the time required to compute a single gradient step. The GPU exhibits near-constant runtime across all sizes, reflecting efficient parallel amortization of fixed overheads, e.g. , kernel launch, memory movement. In contrast, CPU runtime increases steadily with instance size, scaling approximately linearly.

Figure 4: Performance comparison of SMT solvers on combinatorial problems. The results show the number of solved instances and runtime efficiency (average PAR-2 score of the solvers). (a) Scheduling problems, which mainly consist of non-overlap, feasibility, and task-dependency constraints. The virtual-best solver ( VBS1 , including FourierSMT ) is 8.18 $\times$ faster and solves 20 more instances than the counterpart ( VBS2 , excluding FourierSMT ). (b) Placement problems, which mainly consist of non-overlap, feasibility, and routing-aware constraints. In this category, Z3 and Z3++ achieve the best performance cross CDCL( $\mathcal{T}$ ) solvers. VBS1 is 4.93 $\times$ faster and solves 10 more instances than VBS2 . All solvers operate on identical encodings, indicating that the performance gain stems purely from the optimization framework rather than from encoding-free advantages.

Appendix figures & tables8 assets

Supplementary material from the paper’s appendix.

Appendix

Instances	0	1	2	3	4	5	6	7
100_0	9.981	8.530	9.122	8.417	10.139	8.966	8.766	10.231
100_1	10.226	10.005	10.071	8.736	10.225	10.220	10.144	11.852
100_2	10.494	10.311	10.074	12.362	10.259	10.953	10.812	12.552
100_3	12.856	11.400	10.109	13.103	10.335	10.980	12.991	14.721
100_4	13.021	12.790	10.588	14.664	10.339	12.563	13.171	14.824
100_5	14.094	13.071	12.362	14.689	10.428	13.786	13.573	14.862

Appendix

Table 1: Per-instance runtime of FourierSMT for the random hybrid-constraint benchmark. Eight GPUs use different seed numbers. All runtimes are reported in seconds. The label “to” indicates that the solver exceeded the allotted time limit (1000 seconds) and did not return a solution.

Instances	0	1	2	3	4	5	6	7
16_2_0	27.110	28.163	27.517	27.472	26.969	24.363	21.773	16.021
16_2_1	15.058	17.114	13.984	29.762	16.877	16.968	13.735	17.574
16_2_2	12.492	13.120	12.740	12.345	12.997	13.266	13.477	12.797
16_2_3	12.292	12.423	11.667	22.216	11.524	12.735	11.093	27.390
16_2_4	9.836	11.120	11.540	10.510	11.032	11.607	12.166	11.090
16_2_5	8.723	9.064	10.555	9.773	9.173	9.884	10.575	8.529

Appendix

Table 2: Per-instance runtime of FourierSMT for the continuous time scheduling benchmark. Eight GPUs use different seed numbers. All runtimes are reported in seconds. The label “to” indicates that the solver exceeded the allotted time limit (1000 seconds) and did not return a solution.

Instances	0	1	2	3	4	5	6	7
2_2_0	13.273	9.910	9.556	7.955	7.523	9.020	8.813	7.594
2_2_1	9.251	12.525	11.632	7.698	7.608	8.719	7.870	7.994
2_2_2	8.830	8.555	8.196	8.370	7.447	9.899	8.880	8.172
2_2_3	9.070	10.114	9.298	11.977	7.769	10.307	9.330	8.419
2_2_4	12.097	9.784	9.146	12.242	7.909	11.541	11.187	8.727
2_2_5	11.684	13.602	11.329	8.226	9.902	10.300	8.976	8.887

Appendix

Table 3: Per-instance runtime of FourierSMT for the 3D placement benchmark. Eight GPUs use different seed numbers. All runtimes are reported in seconds. The label “to” indicates that the solver exceeded the allotted time limit (1000 seconds) and did not return a solution.

Instances	FourierSMT	Yices2	SMTS	MathSAT5	Z3	Z3PP	SMT-RAT	CVC5
100_0	10.320	0.667	2.056	1.206	51.959	127.370	1.774	2.860
100_1	10.520	0.683	2.260	1.190	51.131	98.331	1.554	2.693
100_2	11.720	0.673	2.402	1.201	45.104	60.249	1.608	2.737
100_3	13.660	0.663	2.342	1.155	41.762	95.694	1.631	2.874
100_4	14.290	0.698	2.386	1.232	58.014	99.942	1.596	2.981
100_5	14.500	0.669	19.931	1.200	46.701	52.544	1.583	2.711

Appendix

Table 4: Per-instance runtime for the random hybrid-constraint benchmark. All runtimes are reported in seconds. The label “to” indicates that the solver exceeded the allotted time limit (1000 seconds) and did not return a solution.

Instances	FourierSMT	Yices2	SMTS	MathSAT5	Z3	Z3PP	SMT-RAT	CVC5
16_2_0	27.040	0.230	1.172	0.299	0.862	0.331	9.956	1.179
16_2_1	16.922	0.062	0.195	0.163	0.083	0.163	9.952	0.332
16_2_2	12.897	0.030	0.358	0.252	0.092	0.154	7.262	0.288
16_2_3	12.357	0.044	0.212	0.324	0.096	0.159	5.562	0.267
16_2_4	11.105	0.032	0.199	0.261	0.086	0.145	6.632	0.252
16_2_5	9.473	0.033	0.194	0.323	0.086	0.157	7.903	0.266

Appendix

Table 5: Per-instance runtime for the continuous time scheduling benchmark. All runtimes are reported in seconds. The label “to” indicates that the solver exceeded the allotted time limit (1000 seconds) and did not return a solution.

Instances	FourierSMT	Yices2	SMTS	MathSAT5	Z3	Z3PP	SMT-RAT	CVC5
2_2_0	8.357	0.005	0.120	0.020	0.034	0.050	0.213	0.023
2_2_1	8.462	0.005	0.122	0.021	0.036	0.051	0.214	0.024
2_2_2	8.464	0.006	0.132	0.021	0.036	0.052	0.228	0.024
2_2_3	8.573	0.006	0.136	0.021	0.036	0.052	0.373	0.025
2_2_4	8.851	0.006	0.136	0.021	0.036	0.052	0.373	0.025
2_2_5	8.908	0.006	0.138	0.021	0.036	0.053	0.379	0.025

Appendix

Table 6: Per-instance runtime for the 3D placement benchmark. All runtimes are reported in seconds. The label “to” indicates that the solver exceeded the allotted time limit (1000 seconds) and did not return a solution.

Figure 5: Detailed solver performance on benchmark categories. (a) Results on the scheduling problems. Z3++ , CVC5 , MathSAT5 , SMT-RAT wins non of the instances in this category. Yices2 performs best on the small-scale instances ( $n_{w}=16$ ), while SMTS attains the best results on the medium-scale cases ( $n_{w}\in\{32,64\}$ ). As the instance size increases further, FourierSMT can handle cases that cause timeouts among competing solvers. (b) Results on the placement problems. SMTS , CVC5 , MathSAT5 , SMT-RAT wins non of the instances in this category. Yices2 still performs best on the small-scale instances ( $n_{m}=2$ ), while Z3 and Z3++ attains the best results on the medium-scale cases ( $n_{w}\in\{8,16,32\}$ ). The landscape of solvers exhibits pronounced variability: different solvers excel in different problem scales, and no classical solver maintains uniformly strong performance. FourierSMT benefits from GPU acceleration, resulting in relatively similar solving times across instance sizes because the fixed parallelization overhead of the GPU amortizes most of the computational cost. For the largest category, FourierSMT remains scalable and continues to solve instances that all other solvers time out on.

Instances	CPU	GPU
100_0	4.841	12.890
100_1	4.993	12.848
100_2	4.975	12.126
100_3	5.300	12.370
100_4	4.930	12.902
100_5	4.886	12.942

Appendix

Table 7: Per-instance average gradient runtime of FourierSMT for the random hybrid-constraint benchmark. All runtimes are reported in milliseconds. The label “to” indicates that the solver exceeded the allotted time limit (1000 seconds) and did not return a solution.

Satisfiability Modulo Theories

Satisfiability modulo theories (SMT) checks whether logical formulas are satisfiable under theories such as arithmetic, strings, and bit-vectors.

See all 19 papers

Accelerating Floating-Point Satisfiability Solving via Gradient Normalization
Sep 14, 2026Yuanzhuo ZhangSatisfiability Modulo Theories
Independent, China
Accelerated Fourier SAT (AFSAT): Fully Realising a GPU-based Symmetric Pseudo-Boolean SAT Solver
Jun 4, 2026Cody J Christopher, Charles GrettonGPU Acceleration High-Performance Computing
School of Computing, Australian National University, Canberra, Australia.
SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification
Sep 1, 2026Swapnil Bhattacharyya, Mayank BaranwalLarge Language Model-Guided Optimization
TCS Research, Mumbai · Indian Institute of Technology Bombay

Sep 14, 2026J/K move · Enter open · S save

Accelerating Floating-Point Satisfiability Solving via Gradient Normalization

Yuanzhuo Zhang

Independent, China

Satisfiability Modulo Theories

Open paper AskPDF arXiv

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.

Abstract

Satisfiability Modulo Theories

Explore similar work

Accelerating Floating-Point Satisfiability Solving via Gradient Normalization

Accelerated Fourier SAT (AFSAT): Fully Realising a GPU-based Symmetric Pseudo-Boolean SAT Solver

SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification