Paper deep dive
Continuous Optimization for Satisfiability Modulo Theories on Linear Real Arithmetic
Yunuo Cen, Daniel Ebler, Xuanyao Fong
Intelligence
Status: succeeded | Model: google/gemini-3.1-flash-lite-preview | Prompt: intel-v1 | Confidence: 95%
Last extracted: 3/26/2026, 1:41:03 AM
Summary
The paper introduces FourierSMT, a scalable and parallelizable continuous-variable optimization framework for Satisfiability Modulo Theories (SMT) on Linear Real Arithmetic (LRA). It generalizes the Walsh-Fourier expansion (WFE) to a mixed Boolean-real domain (xWFE) and uses extended binary decision diagrams (xBDDs) to compute circuit-output probabilities (COP) efficiently. By applying randomized rounding and Gaussian sampling, the framework transforms discrete SMT constraints into a smooth surrogate objective, which is then optimized using projected gradient descent with an annealing schedule to ensure convergence and soundness.
Entities (5)
Relation Signals (3)
FourierSMT → solves → SMT
confidence 100% · we introduce FourierSMT as a scalable and highly parallelizable continuous-variable optimization framework for SMT.
FourierSMT → utilizes → xWFE
confidence 95% · We generalize the Walsh-Fourier expansion (WFE), called extended WFE (xWFE)... which allows the use of gradient methods for SMT.
xBDD → encodes → xWFE
confidence 90% · To reduce the evaluation complexity of xWFE, we present the extended binary decision diagram (xBDD) and map the constraints from xWFE to xBDDs.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2603.22877v1
- Canonical: https://arxiv.org/abs/2603.22877v1
Trouble viewing inline? Open PDF directly →
Full Text
145,729 characters extracted from source content.
Expand or collapse full text
Continuous Optimization for Satisfiability Modulo Theories on Linear Real Arithmetic Yunuo Cen, 1,∗ Daniel Ebler, 2,† and Xuanyao Fong 1,‡ 1 Department of Electrical and Computer Engineering, National University of Singapore, Singapore 2 School of Computing and Data Science, The University of Hong Kong, Hong Kong, China (Dated: March 25, 2026) 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 introduceFourierSMTas 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 as- signments 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 con- straints 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. INTRODUCTION Satisfiability modulo theories (SMT) is a class of de- cision problems that ask whether a variable assignment exists that satisfies an abstract set of constraints. The constraints are referred to as first-order logic and com- bine Boolean logic with, for example, real-valued inequal- ities [1]. SMTs extend the problem of Boolean satisfiabil- ity (SAT) with greater expressiveness [2], which is essen- tial when addressing complex scientific and engineering challenges, particularly in operations research [3, 4], for- mal verification [5, 6], and artificial intelligence [7, 8], among others. SMT problems, such as SAT, are gen- erally NP-complete [9], making it highly challenging to scale solutions to real-life applications. Practical SMT solvers are mainly based on conflict- driven clause learning (CDCL), which is an exact method that has first achieved engineering success in solving SAT problems [10–13]. CDCL combines Boolean con- straint propagation with non-chronological backtrack- ing, efficiently pruning the search space [14]. To ad- dress the more general structure of the constraints in SMT, the solvers employ an extended framework known as CDCL(T), which integrates CDCL with the- ory solvers [2]. In practice, this means that the solvers explore possible combinations of truth values for proposi- tional constraints while simultaneously checking that the corresponding numerical constraints are mathematically consistent. Prominent solver instances includeZ3[15], CVC5[16],Yices2[17],OpenSMT2[18],SMT- ∗ cenyunuo@u.nus.edu † eblerd@hku.hk ‡ kelvin.xy.fong@nus.edu.sg RAT[19] andMathSAT5[20]. However, CDCL(T)- based solvers often suffer from long runtimes and show poor parallelizability on multi-core architectures. This leads to strongly limited scalability. In addition, the per- formance of the CDCL(T) methods is highly problem- specific, and local search techniques were shown to some- times outperform CDCL(T) on benchmarks such as SMT-LIB with low cutoff times [21], as well as concrete applications [22]. Alternative approaches based on continuous local search (CLS) have been proposed for SAT solving, such asFourierSAT[23],GradSAT[24], andFastFouri- erSAT[25], which transform Boolean constraints into continuous multilinear polynomials [26] and refine solu- tions with gradient descent on the objective function. This allows for strong parallelization on multi-threading architectures such as GPUs and FPGAs, dramatically reducing computation times and allowing for scaling to large and complex problem instances [25]. However, the core theory in CLS, spectrum analysis, is inherently de- fined over Boolean domains and does not extend to real- valued variables. Consequently, CLS has been incompat- ible with SMT. In this work, we propose a scalable and highly par- allelizable CLS-based solver approach for SMT, called FourierSMT, with a focus on linear real arithmetic (LRA) constraints. To enable CLS for SMT, we in- troduce a generalization of the Walsh-Fourier expansion (WFE) [26] from the Boolean to the mixed Boolean-real domain to explicitly incorporate LRA constraints (see Fig. 1b). This allows us to encode the SMT constraints in piecewise multilinear functions, called extended Walsh- Fourier expansion (xWFE) (see Fig. 1c). To identify sat- isfying variable assignments with gradient-based meth- ods, we construct a smooth surrogate function through arXiv:2603.22877v1 [cs.AI] 24 Mar 2026 2 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. randomized roundingof Boolean variables andGaussian samplingof real variables (see Fig. 1d). The number of terms in an xWFE grows exponentially with the num- ber of variables in the corresponding constraint.To avoid this overhead, we extend the data structure of ex- tended binary decision diagram (xBDD) to efficiently en- code Boolean-continuous constraints (see Fig. 1e). We then show equivalence between the expectation value of a xWFE and the circuit-output probability (COP) of the xBDD, which allows one to optimize the COP instead. This leads to a drastic reduction in complexity. The op- timality of the solution is shown to be preserved if we optimize the smooth surrogate objective while gradually reducing the smoothness of the original piecewise mul- tilinear function (see Fig. 1f). This allows for efficient gradient-based optimization under annealing of the opti- mization landscape. We benchmarkFouerierSMTon scheduling and placement problems with up to 10,000 variables and 700,000 constraints and show substantial performance gains of up to 8×shorter runtimes. The results highlight the practical applicability ofFouri- erSMTfor complex real-world computational tasks. RESULTS Satisfiability Modulo Theories SMT defines the class of problems that pose the ques- tion of whether a set of Boolean constraints is satisfiable with respect to a theoryT. They were first introduced in the context of extending purely Boolean constraints in SAT to specific mathematical theories [27–29], such as Reals,BitVectors[30, 31], andArrays[32, 33]. For Reals, this allows us to combine propositional variables with inequalities on real-valued variables, connected by Boolean connectivities such as∧,∨,⊕,→,=. Mathematically, an SMT formulaFis defined as the conjunction of constraintscfrom a finite set of Boolean constraintsC, as F= c∈C c . SolvingFrequires an assignment of all variables that satisfies all constraintsc∈C. For example, a typical SMT formula isF= (x 1 ⊕x 2 )∧(x 1 ∨(y≤0)), where x 1 ,x 2 are Boolean andy∈R. SMT solvers are commonly derived from SAT solvers and follow the approach of CDCL [10–13] and discrete local search (DLS) [34–38]. Here, CDCL is at its core an exhaustive tree-search on variable assignments, such that for practical scenarios with a large number of con- straints compared to the number of decision variables, CDCL-based approaches need an infeasibly long time to converge. More recently, CLS has been explored as a novel complement to CDCL, particularly for the problem class of hybrid SAT solving, where Boolean constraints are combined with other types of constraints such as not- all-equal, XOR, or pseudo-Boolean constraints [23, 24]. CLS has demonstrated orders-of-magnitude speedups over CDCL solvers on selected benchmarks [25]. Ex- isting CLS approaches, however, only support Boolean variables and do not extend to SMT. In the following, we introduceFourierSMTas a novel CLS-based solution framework for SMT, with a focus on 3 the theory of LRA. In this theory, the constraints assume linear inequalities subject to real numbers. SMT(LRA) has a variety of applications, including formal verifica- tion [39], artificial intelligence [40], computational biol- ogy [41]. The framework enables continuous optimization techniques to tackle theory-rich constraints that are cur- rently beyond the capability of existing CLS methods. Walsh-Fourier Expansions The Walsh-Fourier transform was previously stud- ied as a mathematical tool in theoretical computer sci- ence [42, 43], mainly to analyze the spectral properties of Boolean functions and to prove results in circuit com- plexity [44], threshold phenomena in mathematics [45], and social choice theory [46]. Formally, given a functionf:±1 n →Rdefined on a Boolean hypercube, there exists a unique way of expressingfas a multilinear polynomial [26], as f(x) = X S⊆[n] ˆ f(S)· Y i∈S x i ! .(1) Here, ˆ f(S)∈Ris called the Walsh-Fourier coefficient, the variablesx i ,i= 1,2,...,nare Boolean variables that assume values±1, and each term in the sum corresponds to a subset of [n] =1,2,...,n. While the conventional WFE applies to purely Boolean domains, SMT problems involve richer structures that in- clude real variables in LRA. To extend the WFE to SMT, we generalize the map in the following to an xWFE. We begin by constructing an atomα i , which in the theory of LRA is a linear equality or inequality of the form α i : m X j=1 q i,j y j −q i,0 ▷◁0, where▷◁∈ =,<,≤,>,≥, the coefficientsq i,j are num- bers that must have a finite syntactic representation so that formulas can be encoded and reasoned about sym- bolically, and they j are real-valued variables. We asso- ciate with each atomic constraint a Boolean indicator δ i (y) = ( −1,ifα i is True 1,else. Letcbe a constraint consisting ofnpropositional vari- ables andkatoms. In SMT(LRA),ccan be represented as a functionf c :±1 n ×R m → ±1. Then, there is a unique way of expressingf c as a piecewise multilin- ear polynomial, where each term corresponds to a pair of subsets of [n] and [k], as (see Supplementary Note 1) f c (x,y) = X S⊆[n] T⊆[k] ˆ f c (S,T)· Y i∈S x i · Y i∈T δ i (y) ! ,(2) where ˆ f c (S,T)∈Ris the extended Walsh-Fourier coef- ficient. The expression indicates that each constraint in an SMT(LRA) formula admits a unique piecewise multi- linear Walsh-Fourier representation. By aggregating the expansions of all constraints, weighted according to their importance, we obtain the global optimization objective of the original SMT(LRA) problem: F w (x,y) = X c∈C w c ·f c (x,y).(3) Here, weightw c ∈R + corresponds to the constraintc. Rounding and Sampling The objective function defined in Eq. (3) is piecewise multilinear, while the argumentx∈ ±1 n is discrete. To make the objective applicable to CLS, we relax the propositional variablesxto the continuous hypercube [−1,1] n and optimize the resulting multilinear extension. Randomized roundingR: [−1,1] n → ±1 n then maps the variables back onto the Boolean hypercube, as ( P[R(a) i =−1] = 1−a i 2 P[R(a) i = +1] = 1+a i 2 (4) wherei∈ 1,·,nanda∈[−1,1] n . The correspond- ing probability on a Boolean vector is then defined as S a (x) =P[R(a) =x]. This provides a probabilistic representation of the xWFE. Concretely, we express the xWFE as its expectation un- der randomized rounding. Letf c denote the xWFE of a constraintc∈C. Lem. 1 (see Supplementary Note 2) states that, for any real point (a,b)∈[−1,1] n ×R m , the expectation off c with respect to the distributionS a is E x∼S a [f c (x,b)] =f c (a,b),(5) and we have E x∼S a [F w (x,b)] =F w (a,b),(6) where we sampledxfrom the probability distributionS a . The following theorem establishes that the global min- ima of the relaxed problem still encode solutions to the original discrete problem. Theorem 1(Soundness).LetF w be the weighted objec- tive function with weightsw c ∈R + for each constraint c∈C. Then the SMT(LRA) formulaFis satisfiable if and only if Eq.(6)satisfies min a∈[−1,1] n b∈R m F w (a,b) =− X c∈C w c . 4 Figure 2.Optimization trajectories and energy landscapes under different sampling parameters.The number of gradient steps required to reach anε-projected critical point is shown forε= 10 −2 .(a)The colorbar indicates the inverse sampling parameter 1/σ.1.Whenσ→ ∞(i.e., 1/σ= 0), the gradient with respect to the real-valued variablesyvanishes, as the smoothing effect becomes arbitrarily strong.2.Moderately large sampling parameters,i.e., 1/σ∈ 0.1,...,0.5, yield slower convergence to the global minimum.3.In contrast, smaller values ofσ, corresponding to 1/σ∈ 0.6,...,2.0, lead to faster convergence to a local minimum.4.The dashed gradient-colored curve denotes the annealing schedule, in which 1/σ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σ. The horizontal and the vertical axes of each subplot correspond toxandyin the domain [−1,1]. Each subplot shows the smoothed objective (C σ , greyscale background) and the path taken by the gradient descent (colorline, the color refers to the color bar in panel (a) as 1/σ). 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). The proof of Thm. 1 is in the Supplementary Notes 9. The function in Eq. (6) is smooth ina∈[−1,1] n , but non-smooth inb∈R m , so that the gradient with re- spect tobvanishes. To address this, we introduce a sampling-based smoothing technique that provides a con- tinuous approximation of the atoms. Forb∈R m , a sam- pling pointd i (b) drawn from the Gaussian distribution N(b,σ 2 I) can be wrtiten as d i (b) = E y∼N(b,σ 2 I) δ i (y) = erf P m j=1 q i,j b j −q i,0 q 2 P m j=1 q 2 i,j σ (7) where the second equation is the analytical expression derived whenδ i (y) corresponds to a linear constraint of the formq ⊤ i y≤q i,0 , (see the Supplementary Note 2, proof of Lem. 1). Thm. 4 in the Supplementary Note 2 states that, for any point (a,b)∈[−1,1] n ×R m , we have E x∼S a y∼N(b,σ 2 I) [f c (x,y)] = X S⊆[n] T⊆[k] ˆ f c (S,T)· Y i∈S a i · Y i∈T d i (b) ! , (8) which is the expectation of Eq. (2) under relaxation of variablesx i andδ i toa i andd i . The number of terms in Eq. (8) grows exponentially asO(2 n+k ). This is because xWFE enumerates all pos- sible states. In the following, we present an equivalent approach that significantly reduces the complexity. The Cor. 2 in the Supplementary Note 4 establishes that the expectation of an xWFE can be expressed as a COP of a probablistic circuit, COP c = E x∼S a y∼N(b,σ 2 I) [f c (x,y)].(9) Further, letC σ (a,b) = P c∈C w c ·COP c . Then, we have C σ (a,b) = E x∼S a y∼N(b,σ 2 I) [F w (x,y)].(10) We show in the Supplementary Note 5 that running the probability assignment algorithm on an xBDD can produce such a COP (see [24, 47] for an introduction to BDDs, and the Supplementary Note 3 for our ex- tension to xBDD). This allows us to use the COP of xBDDs as an optimization surrogate instead of the ex- pectation of xWFE. In addition, the COP of an xBDD can be efficiently evaluated [48] (see also the Supplemen- tary Note 4), avoiding the problem of state enumeration. In the Supplementary Note 5, Thm. 5 and Thm. 6 estab- lished that the computational complexity of evaluating the COP scales isO(|V c |), while the complexity of com- puting its gradient scales isO(m·|V c |), where|V c |de- notes the number of nodes in the decision diagram repre- senting constraintc. Especially when the literals are sym- metric, the complexity of evaluating the COP reduces to O (n+k) 2 [49]. This offers substantial reductions in computational cost [50–52]. 5 Algorithm 1:FourierSMT Input:A constraint setC, constraint weightsw c , initial point (a,b), sampling parameterσ Output:ResultSATorUnknown 1forc∈Cdo 2Transformcinto xWFEf c and COP c ; // Corollary 1 & Supplementary Notes 1-4 3while||g(a,b)|| 2 > ε 2 do 4fori∈range(n)do 5p i ← 1−a i 2 ;// Rounding, Eq. (4) 6fori∈range(m)do 7p i+n ← 1−d i (b) 2 ;// Sampling, Eq. (7) 8Get the projected gradientg(a,b) by Eq. (13); 9Update the assignment (a,b)←(a,b)−η·g(a,b); 10Rounded assignment (x,y)←(sgn(a),b); 11ifF w (x,y) =− P c w c then 12returnSAT;// Theorem 1 13else 14returnUnknown;// CLS is incomplete FourierSMT - A Gradient-Based Optimizer for SMT The theoretical framework established above sets the foundation forFourierSMT, a CLS-based optimizer for SMT. We refer to Alg. 1 for the following discussion, and to Supplementary Notes 1-5 for a detailed analysis of the algorithm. Alg. 1 starts by transforming the mixed Boolean-real constraints into continuous functions (lines 1 and 2). The corresponding xBDD can be efficiently constructed using existing decision diagram packages such as CUDD [53]. This enables a gradient-based approach to solve the con- tinuous objective in Eq. (10), where the minima encode the solution to the original discrete problem. The vari- ables are transformed to probabilities due to rounding and sampling (lines 4-7). Then,FourierSMTruns pro- jected gradient descent (PGD) until it converges to an ε-projected-critical point (see Methods). At each gra- dient step,FourierSMTcomputes the gradient of the COP of each constraintc(line 8). The gradients can be computed efficiently by top-down and bottom-up mes- sage propagations through xBDDs (see the Supplemen- tary Note 5, Alg. 3 and Alg. 4). The projected gradient mapping is then computed by Eq. (13), through convex quadratic programming (QP) (see Methods, Prop. 1). Line 10 executes the randomized rounding on the propo- sitional variablesx, mapping the assignment back to the original mixed Boolean-real domain. Given the hardness of optimizing non-convex functions [54], it is more practi- cal to converge to local optima and check with Theorem 1 if any optimum is global (line 12). The performance of CLS, measured by the number of steps until convergence, is critically dependent on the smoothness of the objective. We show in the Supple- mentary Note 6, Thm. 7 that the PGD inFourierSMT converges to anε-projected-critical point inO( αL ε 2 ) iter- ations, whereαis the sum of the constraint weights and Lis the gradient Lipschitz constant. In the Supplemen- tary Note 6, Prop. 2, we showed thatLdepends on the number of variables, constraints, theory atoms, and the sampling parameterσ. These parameters jointly deter- mine the convergence rate of each PGD trail. We examine the empirical behavior of the projected gradient method with a concrete example, see Fig. 2. Here, we study the conjunction of the two constraints ¬x⊕(y >0) andx∧(y >0), which has a local minimum onx= 1,δ(y) = 1 and a global minimum onx=−1, δ(y) =−1. A larger varianceσin the Gaussian sampling distributionN(b,σ 2 I) generally produces a smoother and better-conditioned objective landscape. Forσ >2, the Gaussian smoothing covers a wider portion of the en- ergy landscape, enabling the optimizer to capture global structural information and eventually reach the global minimum. However, we observe that trials with largerσ exhibit slower convergence toward theε-projected-critical point, because excessive smoothing reduces the effective update step size. In contrast, whenσ <2, the sam- pling becomes more localized, the energy landscape ap- pears sharper, and the optimization rapidly converges to a nearby local minimum. To mitigate this issue, we adopt anannealing strategy, in which optimization begins with a large varianceσand gradually reduces it according to a schedule. An effective annealing schedule should allow iterations to cross tran- sition regions (see the Supplementary Note 7, Cor. 3) quickly, while subsequently reducingσto recover the ex- act objective. In the limit ofσ→0, we recover the exact multilinear objective as in Eq. (3). This leads to a global exploration of the landscape and identification of the right neighborhood of solutions. Asσreduces, the transition regions become tighter, effectively narrowing the landscape down to the neighborhood of a minimum. This is formalized by the following Theorem 2(Optimality).Whenσ= 0, Eq.(10)has no local optima within the open domain(−1,1) n ×R m , i.e., projected gradient will converge to the boundary of [−1,1] n ×R m . The proof of Thm. 2 is in the Supplementary Note 8. Thm. 2 states that reduction of the sampling parame- terσto zero recovers the soundness property of Thm. 1, as it ensures that the smoothing mechanism introduced for optimization does not alter the semantics of the un- derlying SMT(LRA) formulation. At the same time, the theoretical guarantees atσ= 0 do not fully characterize the behavior of the optimization dynamics at finiteσ. In practice, the overall performance of the solver depends on several factors, including the optimization method, initialization, and, in particular, the annealing schedule used to decreaseσ. As in other annealing-based opti- mization frameworks, the schedule influences how effec- tively the algorithm explores the landscape before local- izing the search to specific regions, and thus plays an im- 6 portant role in determining empirical performance [55– 57]. In Fig. 2b, we illustrate a trial in whichσdecreases at each gradient step. In step 19, the point converges to aε-projected critical point. The above analysis confirms both the convergence and soundness of the proposed annealing-based optimization scheme, ensuring that the obtained solutions are theoreti- cally grounded. We next validate these properties empir- ically through extensive experiments on random hybrid benchmarks and large-scale combinatorial problems. Performance Analysis and Application to Combinatorial Problems To evaluate the performance ofFourierSMT, we first conduct experiments on a benchmark set of random prob- lem instances, each consisting of hybrid constraints fol- lowing the setting in [23],i.e., cardinality (card), not- all-equal (nae), and parity (xor) constraints. Such con- straints are versatile for encoding a wide range of com- binatorial problems. We varyn∈ 100,200,...,1000 to generate 10 benchmark instances for eachn. Each in- stance containsnBoolean variables andnreal variables (this choice is arbitrary, and our solver works for any proportion of Boolean and real variables). We set the number of each type of constraint tom card =m nae = n/5, andm xor =n/50, while their respective constraint lengths arel card =l nae = min(50,n/5) andl xor = 50. The behavior and interactions of such hybrid Boolean constraints have been studied extensively in prior work, and transitions in the hardness of the problems were studied in [58–60]. We extend the setting here to Boolean and real variables. In addition, each instance includesn LRA atoms, enabling the extension of the benchmark to continuous variables. The details of the random bench- mark are given in the Methods. We compareFourierSMTwith representative SMT solvers, includingZ3[15],Z3++[21],CVC5[16], Yices2[17],SMTS[18],MathSAT5[20], andSMT- RAT[19]. All solvers are applied to the corresponding SMT(LRA) encodings, where the Boolean backbone is expressed in conjunctive normal form. For reference, we also report two virtual best solvers:VBS1, defined as the best performance achievable across all solvers, and VBS2, defined as the best performance excludingFouri- erSMT. The gap between VBS1 and VBS2 quantifies the advantage ofFourierSMTcompared to the current state-of-the-art. The solver performance is assessed us- ing the metric called PAR-2 (penalized average runtime 2) score, as in Eq. (15). This is the most common metric used in SMT and SAT solving [61]. For all problems, we set a 1000-second time limit for the benchmark problems. The solvers are executed on AMD EPYC 9654 CPUs, whileFourierSMTis run on NVIDIA L40S GPUs, see Methods for more details. For CDCL(T)-based solvers, the encoding of instances generated withn≤500 in CNF form creates an over- head such that the encoded formulas contain up to 64,000 variables and 127,000 clauses (see Methods sec- tion). ForFourierSMT, only 1000 variables (nBoolean variables andnreal variables) are needed. As a conse- quence, all solvers except FourierSMT fail to solve in- stances for whichn≥500.FourierSMTscales to problems with up ton= 1000. This would involve more than 130,000 variables and 250,000 clauses for CDCL(T)-based solvers, rendering problems of this mag- nitude extremely challenging for current state-of-the-art SMT solvers. Despite this hardness,FourierSMTsuccessfully solves all 100 instances. In contrast, the portfolio of all competing solvers,i.e., VBS2, solves only 50 small- to medium-scale instances. This demonstrates the supe- rior scalability and robustness of FourierSMT on large random hybrid benchmarks. From Fig. 3a we can ob- serve that, althoughFourierSMTis relatively slower on small-scale instances (n= 100), it achieves 100× speedup on medium-scale instances (n= 500) and is ca- pable of solving instances that are at least twice as large as those handled by competing solvers within this bench- mark. Within the maximum runtime ofVBS1across all instances (37.84 seconds),VBS2only solves 20 in- stances, reflecting a five-fold improvement in scalability contributed byFourierSMT(see per-instance results in the Supplementary Note 10, Table IV). To determine the extent of GPU-induced speedup, we conducted an additional experiment that compares the gradient evaluation time of FourierSMT on CPU and on GPU. For each instance, we measure the average gradient computation time on a total of 10,000 random points. As shown in Fig. 3b, for the smallest instance category, the CPU is 2.55×faster than the GPU. This is expected, as the workload is insufficient to saturate the GPU’s mas- sively parallel architecture, and the runtime is dominated by fixed overheads such as kernel-launch latency and de- vice synchronization. As the instance size increases, the GPU amortizes these fixed costs, whereas the runtime re- mains nearly constant until the hardware becomes fully saturated. In contrast, the CPU exhibits approximately linear growth in runtime as the instance size increases. For the largest instance category, the GPU achieves a 6.67×speedup over the CPU, demonstrating the scala- bility advantages of GPU-accelerated gradient computa- tion. The detailed result is provided in the Supplemen- tary Note 11. We next evaluateFourierSMTon two classes of com- binatorial optimization problems, scheduling and place- ment, which are widely used as benchmarks due to their computational hardness and constraint nature [3, 62]. For both problem classes, SMT solvers are considered to be state-of-the-art. To better reflect practical scenarios, we design benchmark instances in which constraints are encoded with Boolean and real-valued variables, thereby extending beyond purely discrete formulations. We com- pareFourierSMTagainst state-of-the-art SMT solvers in two benchmark suites comprising 380 instances. 7 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, includingFourierSMT) is 62.45×faster and solves 50 more instances than its counterpart (VBS2, excluding FourierSMT). The 20 easy instances (small-scale) are solved more efficiently by CDCL(T) solvers, whereas all larger instances are solved most efficiently byFourierSMT. This pattern demonstrates thatFourierSMTis substantially more scalable.(b) The average gradient computation time ofFourierSMTusing 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, includingFourierSMT) is 8.18× faster and solves 20 more instances than the counterpart (VBS2, excludingFourierSMT).(b)Placement problems, which mainly consist of non-overlap, feasibility, and routing-aware constraints. In this category,Z3andZ3++achieve the best performance cross CDCL(T) solvers.VBS1is 4.93×faster and solves 10 more instances thanVBS2. All solvers operate on identical encodings, indicating that the performance gain stems purely from the optimization framework rather than from encoding-free advantages. Scheduling Problems.We consider a continuous-time variant of the scheduling problem, where a numbern j of jobs are assigned ton w workers, and execution can be- gin at any real-valued time stamp rather than at discrete intervals. This formulation remains NP, but generalizes the problem to more practical scenarios involving contin- uous scheduling. The goal is to find the assignment of all jobs within the given time budget. A full description of the problem is given in the Methods. Benchmark instances were generated by varying the number of workersn w and the ratio between jobs and workersr=n j /n w .Specifically, we setn w ∈ 16,32,64,128,256and choser∈ 2,3,4,5. We gen- erate 10 instances for eachn w andr. Precedence con- straints among jobs capture task dependencies. For each configuration, we created ten benchmark instances, with time budgets specified by a greedy heuristic. Fig. 4a summarizes the results, whereFourierSMT achieves the lowest PAR-2 score. The strongest baseline, SMTS, records 259.01 seconds, whereasFourierSMT is 6.34×faster. Relative to widely deployed solvers, speedups are even more pronounced: 14.2×overYices2, 14.5×overZ3++, 16.3×overZ3, 22.4×overCVC5, 23.8×overMathSAT5, and 41.1×overSMT-RAT. 8 Notably,SMTSis fastest on 79 out of 180 instances, followed closely byFourierSMTon 76, while the lat- ter dominates the larger-scale instances.Yices2andZ3 lead on 38 and 8 instances, respectively. In small- to medium-scale instances,FourierSMTexhibits a warm- up phase as a result of exploration of the local objective landscape, leading to slightly slower runtimes. Crucially, on the largest instances, where other solvers fail to scale, FourierSMTsolves all cases within the 1000-second time limit (see per-instance results in the Supplementary Note 10, Table V). To further assess generality, we next consider another NP-complete problem with different structural charac- teristics: the placement problem. Placement Problems.In VLSI physical design, place- ment assigns components to precise positions on chiplets subject to area and non-overlap constraints. Our bench- mark focuses on the 3D variant, where modules may be stacked across multiple layers. The solution of the bench- mark problem encodes the spatial coordinates of all mod- ules subject to the constraints. Instances were generated by varying the number of macrosn m ∈ 2,4,8,16,32,64and the number of lay- ersn l ∈ 2,4,8. We generate 10 instances for eachn m andn l . Routing-aware constraints were applied: mod- ules within the same macro were colocated, modules on the same layer were placed adjacently, and cross-layer modules were connected via through-silicon vias, thereby reducing downstream routing cost (see Methods). We find thatFourierSMTagain delivers the lowest PAR-2 score, see Fig. 4b. Interestingly, hereZ3sur- passesSMTSas the strongest CDCL(T)-based baseline. Its variantZ3++, which augmentsZ3with local search, shows mixed behavior: outperformingZ3in scheduling but falling behind in placement. This behavior arises be- cause, in placement instances where local search offers limited improvement, the additional search overhead re- duces the time available for CDCL(T) reasoning, causing Z3++to underperform relative to pureZ3. In general, FourierSMTis 3.15×faster thanZ3and 3.54×faster thanZ3++. Relative improvement are larger compared to other baselines: 7.4×overSMTS, 8.69×overYices2, 17.95×overCVC5, 21.8×overMathSAT5, and 36.0× overSMT-RAT. It can be seen thatFourierSMTex- cels primarily on the largest 30 instances, which are in- tractable for the other solvers (see per-instance results in the Supplementary Note 10, Table VI). In conclusion, on the problems of scheduling and place- ment,FourierSMTdemonstrates superior scalability while retaining efficiency. In particular,VBS1achieves speedups of 8.18×and 4.93×overVBS2. This advantage arises from the use of continuous relaxations, Gaussian smoothing, and projected gradient methods to efficiently navigate high-dimensional search spaces, allowing effec- tive handling of instances where traditional CDCL(T) heuristics stagnate. Furthermore, the CLS framework al- lows ForierSMT to achieve shorter runtimes due to strong parallelizability on multi-core hardware, which is very challenging for CDCL(T)-based approaches. DISCUSSION We introducedFourierSMT, a continuous optimiza- tion framework to solve SMT problems with linear real arithmetic (LRA) constraints. While most state-of-the- art solvers are based on conflict-driven clause learning, FourierSMTis a CLS-based approach, which allows gradient-dynamics for SMT. Concretely, we encode the SMT clauses in piecewise-linear functions with an ex- tended Walsh-Fourier expansion (xWFE). We then re- duce the number of terms in the xWFE, which grow ex- ponentially in the number of variables and atoms, by introducing an efficient data structure called extended binary decision diagrams (xBDDs). The output proba- bility of such xBDDs has been proven to be equivalent to the expectation value of xWFE. This allows us to find solutions to the SMT with gradient-based search on the output distribution of xBDDs. To boost convergence, we smooth the xBDD output distribution with randomized rounding and Gaussian sampling techniques. We adopt an annealing schedule, which scans the global landscape first and later localizes the search to a suitable region. This approach was shown to efficiently search the land- scape while maintaining the optimality of the solutions. BenchmarkingFourierSMTboth on random SMT in- stances as well as combinatorial optimization problems, such as scheduling and 3D placement, reveals superior scalability, surpassing previous state-of-the-art solvers in particular for large problem instances. A key advantage of the framework is its compatibility with modern parallel hardware: gradient-based proce- dures map naturally to GPUs, enabling substantial ac- celeration at scale. This combination of theoretical nov- elty and computational efficiency suggests thatFouri- erSMTcan serve as a foundation for solving industrial combinatorial problems at scale. For future directions, extending theFourierSMT framework to nonlinear real arithmetic (NRA) would allow one to address nonlinear atomic constraints that induce highly nonconvex feasible regions and generally lack tractable closed-form expectations under Gaussian smoothing. Such an extension would broaden the ap- plicability to domains such as hybrid system verifica- tion [63] and biological network analysis [64], while offer- ing a fresh perspective on scalable algorithms for NRA. Moreover, generalizing Proposition 1 to accommodate nonlinear constraints would provide efficient projection mechanisms for complex feasible sets, thereby further in- tegrating continuous optimization with symbolic reason- ing. In this way, extendingFourierSMTto NRA would help establish a unifying framework that complements complete methods such as cylindrical algebraic decom- position [65] and MCSAT [66]. 9 METHODS Projected Gradient Descent In PGD, each iteration updates the current point by following the negative gradient. If the updated point lies outside the feasible domain, it is mapped back by a projection operator: (a ′ ,b ′ ) = (a,b)−η∇C σ (a,b),(11) (a,b) = proj D (a ′ ,b ′ ).(12) whereDdenotes the feasible set. Next, we formally de- fine the projection operation and analyze its computa- tional properties. Definition 1(Projection).Let(a ′ ,b ′ )∈R n+m denote the point obtained after a gradient step. The projection of(a ′ ,b ′ )onto the feasible setDis defined as proj D (a ′ ,b ′ ) = arg min (a,b) (∥a−a ′ ∥ 2 +∥b−b ′ ∥ 2 +I D (a,b)) whereI D is an indication.I D (a,b)is 0 (resp.∞) if (a,b)∈D(resp./∈). Based on Definition 1, we can establish that the pro- jection problem is a convex QP. Proposition 1.The projection defined in Definition 1 is a convex QP problem. min a,b n X i=1 a 2 i −2a ′ i a i + m X i=1 b 2 i −2b ′ i b i s.t.−1≤a i ≤1,∀i m X k=1 q j,k b k −q j,0 ▷◁0,∀unit atomic constraint where a unit atomic constraint refers to a constraint that only has an atomic constraint without propositional vari- ables. Substituting Eq. (12) into Eq. (11) yields theprojected gradient mappingg: g(a,b) = 1 η ((a,b)−proj D ((a,b)−η∇C σ (a,b))).(13) Annealing with Weight Adaptation FourierSMTintegrates an annealing strategy with an adaptive clause-weighting scheme based on exponen- tial recency-weighted averaging (ERWA), as outlined in Algorithm 2. The optimization proceeds in a smoothed objective landscape, where the sampling parameterσis gradually decreased according to a predefined anneal- ing schedule. At early iterations, a largeσyields a Algorithm 2:CLS with Annealing Input:A constraint setC, initial constraint weights w c ’s, an initial point (a,b), a decay factorβ, a scaling baseγ, a update iterationτ, an annealing scheduleσ 1 ,σ 2 ,...,σ T Output:ResultSATorUnknown 1Initializeh c ←0 for all constraintc∈C; 2forσ t ∈σ 1 ,σ 2 ,...,σ T do 3Local minimum (a,b)←ProjGradDesc(a,b,σ t ,w); 4Rounded assignment (x,y)←(sgn(a),b); 5#Unsat←0; 6forc∈Cdo 7u c ← 1 2 f c (x,y) + 1 2 ; 8h c ←ρ·h c +u c ; 9#Unsat←#Unsat+u c ; 10iftmodτ= 0then 11w c ←w c ·γ h c ;// update weight 12h c ←1;// reset history 13if#Unsat= 0then 14returnSAT; 15returnUnknown; highly smoothed objective, enabling efficient descent to- ward promising regions. Asσdecreases, the optimization progressively sharpens around the original combinatorial objective, allowing the algorithm to refine candidate so- lutions. To guide the search away from local minima, we main- tain dynamic clause weights with ERWA. At each iter- ation, for every constraintc∈C,FourierSMTchecks whether the rounded assignment satisfiesc. The expo- nentially decayed historyh c is then updated as h c [t+ 1] =ρ·h c [t] + [f c (R(a),b) = 1], wheref c (R(a)) = 1 indicates that the rounded assign- ment ofaviolates constraintc, andρ∈(0,1) is a decay rate controlling the memory of past violations. After a fixed number of iterationsT, clause weights are updated multiplicatively as ω c [t]←ω c [t]·γ h c [t] with scaling baseγ >1. This update rule exponen- tially emphasizes recently falsified clauses while atten- uating the influence of earlier ones, adaptively biasing the search toward persistent sources of violation. FourierSMTrepeatedly invokes Alg. 2 with different random seeds until either aSATresult is returned or the time limit is reached. For the benchmark experiments, we setρ= 0.5,γ= 2, andτ= 1. Projected Critical Point Theε-projected critical point is a concept used in the convergence analysis of projected gradient methods — it 10 refers to a point where the projected gradient mapping has small norm,i.e., the optimization has nearly reached a stationary point within the feasible set. Formally, in the FourierSMT framework, the projected gradient mapping is defined in Eq. (13). Then, a point (a ∗ ,b ∗ ) is said to be anε-projected critical point if ||g(a ∗ ,b ∗ )|| 2 ≤ε 2 ,(14) meaning the norm of the projected gradient is smaller than a small thresholdε,i.e., the optimization has nearly converged. Evaluation Metrics The PAR-2 score is a standard metric that balances runtime efficiency and robustness by penalizing timeouts: PAR-2 = 1 N N X i=1 t i ·1[t i ≤T] + 2T·1[t i > T] ,(15) where1(·) is the indicator function andTdenotes the time limit, set to 1000 seconds in our experiments. Benchmark Problem Descriptions Random Hybrid ConstraintsThe random bench- mark consists of cardinality, not-all-equal, and parity constraints, where these constraints are called hybrid constraints. WFE-based CLS approaches,i.e.,Fouri- erSAT[23] andFastFourierSAT[25], achieve perfor- mance competitive with SOTA CDCL-based SAT solvers on random hybrid constraint problems.AsFouri- erSMTis an extended version ofFourierSATthat natively supports real-valued variables, we construct the benchmark instances using the following types of con- straints. cardinality : n X i=1 l i ≤k not-all-equal :¬(l 1 =l 2 =·=l n ) parity : (l 1 ⊕l 2 ⊕·⊕l n ) l i are the literals, which can be propositional variables x j , inequalities with real-valued variables forRealsα k or their’s negation¬x j ,¬α k . ForFourierSMT, the coefficients of the xWFE are computed following [23], as the hybrid constraints are symmetric (For non-symmetric constraints, we can con- struct the xBDD as in [24]). For the SMT solver competi- tors, the hybrid constraints are encoded into disjunctive clauses, where each clause is the disjunction of literals. The cardinality constraints are encoded using the cardi- nality encoding in PySAT [67, 68]. The NAE constraints are encoded using the standard two-clause encoding that eliminates the all-true and all-false assignments. The XOR constraints use the encoding in [69]. Scheduling with Continuous TimeThe scheduling problem is a classical combinatorial optimization prob- lem that involves assigning a set of jobs (or tasks) to a set of workers (or machines, processors, or other resources) subject to various constraints. Constraint programming solvers, such as Google’s OR-Tools CP-SAT [70], are highly effective in handling discrete logical constraints and have achieved state-of-the-art performance on many discrete scheduling benchmarks. There exist numerous variants of the scheduling problem, differing in the char- acteristics of jobs, resources, and temporal dependencies, each leading to distinct formulations and computational challenges. In this study, we focus on continuous-time scheduling problems, where both discrete logical deci- sions and real-valued timing constraints coexist. Such problems can be naturally encoded and solved by SMT solvers, which integrate logical reasoning with LRA. We encode the problem with the following variables: •Worker index: for each jobj, we use a variable X id,j ∈0,...,n w −1to encode which worker it is assigned to.X id,j is Booleanized as follows X id,j = log 2 (n w )−1 X i=0 2 i ·[x i,j =True]. •Job start time: jobjis launched aty j ∈R. We generate instances by the following parameters. •Worker start time: worker will start admitting job afterd id ∈Rtime, which is sampled fromU(0,1). •Job run time: to complete jobjneedt j ∈Rtime, which is sampled fromU(0,1). •Cutoff time: all workers will stop afterd id +Ttime, whereTis a solution from a greedy heuristic to ensure feasibility. The problems include the following constraints •Task dependency: if the input of a jobjdepends on the output of another jobj ′ , thenjhas to be executed afterj ′ . y j ≥y j ′ +t j ′ •Non-overlap: one worker can run only one job at a time. Hence, for every pair of jobs (j,j ′ ), (x 0,j ⊕x 0,j ′ )∨...∨ x log 2 (n w )−1,j ⊕x log 2 (n w )−1,j ′ ∨(y j −y j ′ ≥t j ′ )∨(y j ′ −y j ≥t j ). •Feasibility: the job can only run on a worker if the worker is active. Hence, for each jobj, (¬x 0,j )∨...∨ ¬x log 2 (n w )−1,j ∨(y j ≥d id )∨(y j ≤d id +T−t j ). 11 3D Placement. The placement problem is another canonical combinatorial problem, widely studied in elec- tronic design automation (EDA). It involves assigning a set of components (or modules) to specific spatial lo- cations on a chip, board, or layout region while satisfy- ing geometric and connectivity constraints. In integrated circuit and 3D chiplet design, placement determines the exact coordinates of macros and standard cells to min- imize wirelength, delay, and congestion, while avoiding overlaps among modules. Traditional approaches in the EDA design flow are mostly heuristic approaches [71]. Recent advances in SMT have enabled efficient model- ing of placement problems by combining Boolean logic for non-overlap and connectivity constraints with linear real arithmetic for geometric relationships [72]. In this study, we evaluate a 3D placement problem, where mod- ules are distributed across multiple layers and intercon- nected through through-silicon vias, posing additional spatial and connectivity challenges. The placement of a module is represented by Booleanized indices and real-valued coordinates: •Macro index: for each modulej, a variableM id,j ∈ 0,...,n m −1encodes the macro assignment, Booleanized as M id,j = log 2 (n m )−1 X i=0 2 i ·[m i,j =True]. •Layer index: a variableL id,j ∈ 0,...,n ℓ −1en- codes the assigned layer, Booleanized as L id,j = log 2 (n l )−1 X i=0 2 i ·[l i,j =True]. •Coordinates: each modulejhas continuous posi- tion variables (x j ,y j )∈R 2 . Each instance contains: •n m macros, each occupying 1×1 nm. •n m large process elements (0.4×0.4 nm) andn m ·n ℓ small process elements (0.2×0.2 nm). •n m large memory elements (0.1×0.1 nm) and n m ·n ℓ 2 small memory elements (0.1×0.05 nm). Randomization is applied by alternating the alignment of small memory elements along thex- ory-axis. The di- mensions of each module are denoted byw j (width along x) andd j (height alongy). The problems include the following constraints Three classes of constraints are enforced: •Routing-aware: each large process is paired with a large memory, and each small process with two small memories. For associated modules (j,j ′ ) and ∀i∈[0,log 2 (n m )−1], n (m i,j =m i,j ′ ),(x j −x j ′ ≤w j ′ ),(x j ′ −x j ≤w j ) (y j −y j ′ ≤h j ′ ),(y j ′ −y j ≤h j ) o i.e., they should be placed in the same macro and should be adjacent to each other. Such that the length of the metal wire can be reduced in the pre- ceding routing stage. •Non-overlap: modules sharing the same macro and layer must not overlap. For pairs (j,j ′ ): (m 0,j ⊕m 0,j ′ )∨ m log 2 (n m )−1,j ⊕m log 2 (n m )−1,j ′ (l 0,j ⊕l 0,j ′ )∨ l log 2 (n l )−1,j ⊕l log 2 (n l )−1,j ′ ∨(x j −x j ′ ≥w j ′ )∨(x j ′ −x j ≥w j ) ∨(y j −y j ′ ≥h j ′ )∨(y j ′ −y j ≥h j ) •Feasibility: all modules must remain within the macro boundary, (x j ≥0),(x j ≤1−w j ),(y j ≥0),(y j ≤1−d j ) Experimental Setup All experiments were conducted on a high-performance computing node equipped with 2×AMD EPYC 9654 CPUs, 24×96 GB of DRAM, and 8×NVIDIA L40S GPUs. Baseline solvers were permitted to use up to 64 threads of the CPUs. Because SAT solvers are highly memory-intensive due to clause database management, naive parallelization via multi-threaded racing, without inter-thread clause sharing, typically yields limited per- formance gains. Consequently,MathSAT5, which lacks multithreading support, was executed in single-threaded mode. Our proposed solver,FourierSMT, leverages GPU acceleration. Eight independent replicas were exe- cuted across the eight available GPUs, and we report the median runtimes to provide more robust results. A time- out of 1000 seconds was imposed per benchmark instance for all solvers. DATA AVAILABILITY The benchmark instances that support the results of this study are available from the corresponding author upon request. CODE AVAILABILITY The algorithms are described in the main text and the supplementary notes. The code is available from the cor- responding author upon request. 12 ACKNOWLEDGEMENTS This work was supported in part by the National Re- search Foundation under the Prime Minister’s Office, Sin- gapore, through the Competitive Research Programme (project ID NRF-CRP24-2020-0002 and NRF-CRP24- 2020-0003); in part by the Ministry of Education, Sin- gapore, through the Academic Research Fund Tier 2 (project ID MOE-T2EP50221-0008); and in part by the National University of Singapore, through the Microelec- tronics Seed Fund (FY2024). AUTHOR CONTRIBUTIONS Y.C. conceived the research idea, developed the the- oretical framework, and implemented the methodology. X.F. supervised the project and provided conceptual guidance. Y.C. and D.E. designed the experiments, and X.F. configured the hardware environment for experi- mental evaluations. All authors analyzed the experimen- tal results and wrote the manuscript. COMPETING INTERESTS The authors declare no competing interests. CORRESPONDENCE Correspondence and requests for materials should be addressed to Yunuo Cen and Xuanyao Fong. [1] A. Biere, M. Heule, and H. van Maaren,Handbook of satisfiability, Vol. 185 (IOS press, 2009). [2] C. Barrett and C. Tinelli, Satisfiability modulo theories, inHandbook of model checking(Springer, 2018) p. 305– 343. [3] C. Ans ́otegui, M. Bofill, M. Palahı, J. Suy, and M. Vil- laret, Satisfiability modulo theories: An efficient ap- proach for the resource-constrained project schedul- ing problem, inProceedings of the 9th Symposium on Abstraction, Reformulation and Approximation (SARA 2011)(2011) p. 2–9. [4] M. Bofill, J. Coll, J. Suy, and M. Villaret, Smt encod- ings for resource-constrained project scheduling prob- lems, Computers & Industrial Engineering149, 106777 (2020). [5] S. Lahiri and S. Qadeer, Back to the future: revisiting precise program verification using smt solvers, ACM SIG- PLAN Notices43, 171 (2008). [6] N. S. Bjørner, K. L. McMillan, and A. Rybalchenko, Program verification as satisfiability modulo theories., SMT@ IJCAR20, 3 (2012). [7] X. Ye, Q. Chen, I. Dillig, and G. Durrett, Satlm: Satisfiability-aided language models using declarative prompting, Advances in Neural Information Processing Systems36, 45548 (2023). [8] G. Spallitta, G. Masina, P. Morettin, A. Passerini, and R. Sebastiani, Enhancing smt-based weighted model in- tegration by structure awareness, Artificial Intelligence 328, 104067 (2024). [9] S. A. Cook, The complexity of theorem-proving proce- dures, inProceedings of the third annual ACM symposium on Theory of computing(1971) p. 151–158. [10] N. E ́en and N. S ̈orensson, An extensible sat-solver, inIn- ternational conference on theory and applications of sat- isfiability testing(Springer, 2003) p. 502–518. [11] G. Audemard and L. Simon, Lazy clause exchange pol- icy for parallel sat solvers, inInternational Confer- ence on Theory and Applications of Satisfiability Testing (Springer, 2014) p. 197–205. [12] J. H. Liang,Machine learning for SAT solvers, Ph.D. thesis, University of Waterloo (2018). [13] A. Fleury and M. Heisinger, Cadical, kissat, paracooba, plingeling and treengeling entering the sat competition 2020, Sat Competition2020, 50 (2020). [14] J. P. Marques-Silva and K. A. Sakallah, Grasp: A search algorithm for propositional satisfiability, IEEE Transac- tions on Computers48, 506 (2002). [15] L. De Moura and N. Bjørner, Z3: An efficient smt solver, inInternational conference on Tools and Algorithms for the Construction and Analysis of Systems(Springer, 2008) p. 337–340. [16] H. Barbosa, C. Barrett, M. Brain, G. Kremer, H. Lach- nitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. N ̈otzli,et al., cvc5: A versatile and industrial-strength smt solver, inInternational Conference on Tools and Al- gorithms for the Construction and Analysis of Systems (Springer, 2022) p. 415–442. [17] B. Dutertre, Yices 2.2, inInternational Conference on Computer Aided Verification(Springer, 2014) p. 737– 744. [18] R. Bruttomesso, E. Pek, N. Sharygina, and A. Tsi- tovich, The opensmt solver, inInternational Conference on TOOLS and Algorithms for the Construction and Analysis of Systems(Springer, 2010) p. 150–153. [19] F. Corzilius, U. Loup, S. Junges, and E. ́ Abrah ́am, Smt- rat: An smt-compliant nonlinear real arithmetic toolbox: (tool presentation), inInternational Conference on The- ory and Applications of Satisfiability Testing(Springer, 2012) p. 442–448. [20] A. Cimatti, A. Griggio, B. J. Schaafsma, and R. Sebas- tiani, The mathsat5 smt solver, inInternational Confer- ence on Tools and Algorithms for the Construction and Analysis of Systems(Springer, 2013) p. 93–107. [21] B. Li and S. Cai, Local search for smt on linear and multi-linear real arithmetic, in2023 Formal Methods in Computer-Aided Design (FMCAD)(2023) p. 1–10. [22] B. Li, D. Li, M. Fu, and S. Cai, Smt-layout:A maxsmt-based approach supporting real-time interaction of real-world gui layout, arXiv preprint arXiv:2411.12271 (2024). 13 [23] A. Kyrillidis, A. Shrivastava, M. Vardi, and Z. Zhang, Fouriersat: A fourier expansion-based algebraic frame- work for solving hybrid boolean constraints, inProceed- ings of the AAAI Conference on Artificial Intelligence, Vol. 34 (2020) p. 1552–1560. [24] A. Kyrillidis, M. Vardi, and Z. Zhang, On continuous local bdd-based search for hybrid sat solving, inProceed- ings of the AAAI Conference on Artificial Intelligence, Vol. 35 (2021) p. 3841–3850. [25] Y. Cen, Z. Zhang, and X. Fong, Massively parallel con- tinuous local search for hybrid sat solving on gpus, in Proceedings of the AAAI Conference on Artificial Intel- ligence, Vol. 39 (2025) p. 11140–11149. [26] R. O’Donnell,Analysis of boolean functions(Cambridge University Press, 2014). [27] C. W. Barrett, D. L. Dill, and A. Stump, Checking satis- fiability of first-order formulas by incremental translation to sat, inInternational Conference on Computer Aided Verification(Springer, 2002) p. 236–249. [28] H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Dpll (t): Fast decision procedures, inIn- ternational Conference on Computer Aided Verification (Springer, 2004) p. 175–188. [29] R. Nieuwenhuis and A. Oliveras, On sat modulo theo- ries and optimization problems, inInternational confer- ence on theory and applications of satisfiability testing (Springer, 2006) p. 156–169. [30] S. Jha, R. Limaye, and S. A. Seshia, Beaver: Engineer- ing an efficient smt solver for bit-vector arithmetic, inIn- ternational Conference on Computer Aided Verification (Springer, 2009) p. 668–674. [31] A. C. Wrightet al.,Modular SMT-based verification of rule-based hardware designs, Ph.D. thesis, Massachusetts Institute of Technology (2021). [32] R. Brummayer and A. Biere, Boolector: An efficient smt solver for bit-vectors and arrays, inInternational Confer- ence on Tools and Algorithms for the Construction and Analysis of Systems(Springer, 2009) p. 174–177. [33] S. Ghilardi and S. Ranise, Backward reachability of array-based systems by smt solving: Termination and in- variant synthesis, Logical Methods in Computer Science 6(2010). [34] B. Selman, D. G. Mitchell, and H. J. Levesque, Gener- ating hard satisfiability problems, Artificial intelligence 81, 17 (1996). [35] B. Selman, H. A. Kautz, B. Cohen,et al., Noise strategies for improving local search, inAAAI, Vol. 94 (1994) p. 337–343. [36] S. Cai, K. Su, and C. Luo, Improving walksat for ran- dom k-satisfiability problem with k¿ 3, inProceedings of the AAAI Conference on Artificial Intelligence, Vol. 27 (2013) p. 145–151. [37] A. Balint and U. Sch ̈oning, Choosing probability distri- butions for stochastic local search and the role of make versus break, inInternational Conference on Theory and Applications of Satisfiability Testing(Springer, 2012) p. 16–29. [38] S. Cai, C. Luo, and K. Su, Ccanr: A configuration check- ing based local search solver for non-random satisfiability, inInternational Conference on Theory and Applications of Satisfiability Testing(Springer, 2015) p. 1–8. [39] L. Cordeiro and B. Fischer, Verifying multi-threaded soft- ware using smt-based context-bounded model checking, inProceedings of the 33rd International Conference on Software Engineering(2011) p. 331–340. [40] W. Steiner, An evaluation of smt-based schedule synthe- sis for time-triggered multi-hop networks, in2010 31st IEEE Real-Time Systems Symposium(IEEE, 2010) p. 375–384. [41] B. Yordanov, C. M. Wintersteiger, Y. Hamadi, and H. Kugler, Smt-based analysis of biological computation, inNASA formal methods symposium(Springer, 2013) p. 78–92. [42] A. Bonami, ́etude des coefficients de Fourier des fonctions del p (g), Annales de l’Institut Fourier20, 335 (1970). [43] J. Kahn, G. Kalai, and N. Linial, The influence of vari- ables on boolean functions, in[Proceedings 1988] 29th Annual Symposium on Foundations of Computer Science (IEEE Computer Society, 1988) p. 68–80. [44] A. Tal, Tight bounds on the fourier spectrum of ac0, in32nd Computational Complexity Conference (C 2017)(Schloss Dagstuhl–Leibniz-Zentrum f ̈ur Infor- matik, 2017) p. 15–1. [45] S. Safra, Perspectives from mathematics, computer sci- ence, and economics, Computational complexity and sta- tistical physics , 25 (2006). [46] G. Kalai, A fourier-theoretic perspective on the con- dorcet paradox and arrow’s theorem, Advances in Ap- plied Mathematics29, 412 (2002). [47] M. Thornton and V. Nair, Efficient spectral coefficient calculation using circuit output probabilities, Digital Sig- nal Processing4, 245 (1994). [48] R. E. Bryant, Binary decision diagrams and beyond: En- abling technologies for formal verification, inProceedings of IEEE International Conference on Computer Aided Design (ICCAD)(IEEE, 1995) p. 236–243. [49] T. Sasao, M. Fujita,et al.,Representations of discrete functions, Vol. 1 (Springer, 1996). [50] S. Kolb, M. Mladenov, S. Sanner, V. Belle, and K. Ker- sting, Efficient symbolic integration for probabilistic in- ference, in27th International Joint Conference on Ar- tificial Intelligence: IJCAI 2018(IJCAI Inc, 2018) p. 5031–5037. [51] P. Z. Dos Martires, A. Dries, and L. De Raedt, Exact and approximate weighted model integration with prob- ability density functions using knowledge compilation, in Proceedings of the AAAI Conference on Artificial Intel- ligence, Vol. 33 (2019) p. 7825–7833. [52] S. Kolb, P. Z. Dos Martires, and L. De Raedt, How to exploit structure while solving weighted model integra- tion problems, inUncertainty in Artificial Intelligence (PMLR, 2020) p. 744–754. [53] F. Somenzi, Cudd: Cu decision diagram package, Public Software, University of Colorado (1997). [54] P. Jain, P. Kar,et al., Non-convex optimization for ma- chine learning, Foundations and Trends®in Machine Learning10, 142 (2017). [55] E. Triki, Y. Collette, and P. Siarry, A theoretical study on the behavior of simulated annealing leading to a new cooling schedule, European Journal of Operational Re- search166, 77 (2005). [56] S. Morita and H. Nishimori, Mathematical foundation of quantum annealing, Journal of Mathematical Physics49 (2008). [57] F. B ̈ohm, T. Inagaki, K. Inaba, T. Honjo, K. Enbutsu, T. Umeki, R. Kasahara, and H. Takesue, Understanding dynamics of coherent ising machines through simulation of large-scale 2d ising models, Nature communications9, 14 5020 (2018). [58] J. M. Dudek, K. S. Meel, and M. Y. Vardi, Combining the k-cnf and xor phase-transitions, inProceedings of the Twenty-Fifth International Joint Conference on Artifi- cial Intelligence(2016) p. 727–734. [59] Y. Pote, S. Joshi, and K. S. Meel, Phase transition be- havior of cardinality and xor constraints, inProceedings of the 28th International Joint Conference on Artificial Intelligence(2019) p. 1162–1168. [60] R. Gupta, S. Roy, and K. S. Meel, Phase transition be- havior in knowledge compilation, inInternational Con- ference on Principles and Practice of Constraint Pro- gramming(Springer, 2020) p. 358–374. [61] R. Amadini, M. Gabbrielli, T. Liu, and J. Mauro, On the evaluation of (meta-) solver approaches, Journal of Artificial Intelligence Research76, 705 (2023). [62] S. M. Saif, M. Dessouky, M. W. El-Kharashi, H. Ab- bas, and S. Nassar, Pareto front analog layout place- ment using satisfiability modulo theories, in2016 Design, Automation & Test in Europe Conference & Exhibition (DATE)(IEEE, 2016) p. 1411–1416. [63] A. Cimatti, S. Mover, and S. Tonetta, A quantifier-free smt encoding of non-linear hybrid automata, in2012 Formal Methods in Computer-Aided Design (FMCAD) (IEEE, 2012) p. 187–195. [64] C. McCaig, R. Norman, and C. Shankland, Process al- gebra models of population dynamics, inInternational Conference on Algebraic Biology(Springer, 2008) p. 139–155. [65] B. F. Caviness and J. R. Johnson,Quantifier elimination and cylindrical algebraic decomposition(Springer Science & Business Media, 2012). [66] D. Jovanovic, C. Barrett, and L. De Moura, The design and implementation of the model constructing satisfiabil- ity calculus, in2013 Formal Methods in Computer-Aided Design(IEEE, 2013) p. 173–180. [67] A. Ignatiev, A. Morgado, and J. Marques-Silva, PySAT: A Python toolkit for prototyping with SAT oracles, in SAT(2018) p. 428–437. [68] A. Ignatiev, Z. L. Tan, and C. Karamanos, Towards uni- versally accessible SAT technology, inSAT(2024) p. 4:1–4:11. [69] C. M. Li, Integrating equivalency reasoning into davis- putnam procedure, AAAI/IAAI2000, 291 (2000). [70] L. Perron, F. Didier, and S. Gay, The cp-sat-lp solver, in 29th International Conference on Principles and Prac- tice of Constraint Programming (CP 2023), Leibniz In- ternational Proceedings in Informatics (LIPIcs), Vol. 280, edited by R. H. C. Yap (Schloss Dagstuhl – Leibniz- Zentrum f ̈ur Informatik, Dagstuhl, Germany, 2023) p. 3:1–3:2. [71] Y. Lin, S. Dhar, W. Li, H. Ren, B. Khailany, and D. Z. Pan, Dreamplace: Deep learning toolkit-enabled gpu ac- celeration for modern vlsi placement, inProceedings of the 56th Annual Design Automation Conference 2019 (2019) p. 1–6. [72] D. Lee, D. Park, C.-T. Ho, I. Kang, H. Kim, S. Gao, B. Lin, and C.-K. Cheng, Sp&r: Smt-based simultaneous place-and-route for standard cell synthesis of advanced nodes, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems40, 2142 (2020). [73] S. Sanner, K. V. Delgado, and L. N. de Barros, Symbolic dynamic programming for discrete and continuous state mdps, inProceedings of the Twenty-Seventh Conference on Uncertainty in Artificial Intelligence, UAI’11 (AUAI Press, Arlington, Virginia, USA, 2011) p. 643–652. [74] M. Chavira and A. Darwiche, On probabilistic inference by weighted model counting, Artificial Intelligence172, 772 (2008). [75] Y. Nesterov,Introductory lectures on convex optimiza- tion: A basic course, Vol. 87 (Springer Science & Busi- ness Media, 2013). [76] A. Kyrillidis, A. Shrivastava, M. Y. Vardi, and Z. Zhang, Solving hybrid boolean constraints in continuous space via multilinear fourier expansions, Artificial Intelligence 299, 103559 (2021). 15 Supplementary Note 1: Walsh-Fourier Expansion In this section, we introduce the Walsh-Fourier expansion (WFE, Thm. 3) and further extend it for adapting real variables (xWFE, Cor. 1). The results in this section lead to Eq. (2) in the main text. Theorem 3(Walsh-Fourier Expansion [26]).Given a functionf:±1 n →R, there is a unique way of expressing fas a multilinear polynomial, where each term corresponds to a subset of[n], according to: f(x) = X S⊆[n] ˆ f(S)· Y i∈S x i ! where ˆ f(S)∈Ris called Walsh-Fourier coefficient, givenSand computed as: ˆ f(S) = E x∼±1 n f(x)· Y i∈S x i ! To extend WFE-based CLS methods to SMT(LRA), we generalize Thm. 3 as follows. Corollary 1(Extended Walsh-Fourier Expansion, xWFE).Letcbe a constraint consisting ofnpropositional variables andkatoms. Thenccan be represented as a functionf c :±1 n ×R m → ±1, where−1denotesTrueand+1 denotesFalse. There is a unique way of expressingf c as a piecewise multilinear polynomial, where each term corresponds to a pair of subsets of[n]and[k], according to: f c (x,y) = X S⊆[n] T⊆[k] ˆ f c (S,T)· Y i∈S x i · Y i∈T δ i (y) ! where ˆ f(S,T)∈Ris called Walsh-Fourier coefficient, givenS,T, and computed as: ˆ f c (S,T) = E x∼±1 n δ(y)∼±1 k f c (x,y)· Y i∈S x i · Y i∈T δ i (y) ! Proof of Corollary 1.A constraintcconsists of at mostnpropositional variables andkatomic constraints. Let z= (x,δ(y)) ̃ f c (z) =f c (x,y)(11) be a Boolean function ̃ f c :±1 n+k →±1. By applying Theorem 3 to ̃ f c , we have ̃ f c (z) = X U⊆[n+k] ˆ f c (U)· Y i∈U z i ! with coefficient ˆ f(U) = E z∼±1 n ̃ f(z)· Y i∈S z i ! . By substituting the above equations with Eq. (11), we have f c (x,y) = X U⊆[n+k] ˆ f c (U)· Y i∈U z i ! = X S⊆[n] T⊆[k] ˆ f c (S,T)· Y i∈S x i · Y i∈T δ i (y) ! 16 wherex i =z i andδ i (y) =z i+n , and ˆ f c (S,T) = E x∼±1 n δ(y)∼±1 k f c (x,y)· Y i∈S x i · Y i∈T δ i (y) ! 17 Supplementary Note 2: Expectation In Supplementary Note 1, we extend the WFE to adapt real variables in SMT. The extension is called xWFE and is still discrete in nature. The objective function in the CLS framework is the expectation of xWFEs. The results in this section lead to Eq. (5) and Eq. (6) in the main text. Furthermore, we mathematically derive the analytical expression ofd i (b). Lemma 1.Letf c denote the WFE of a constraintc. For any real point(a,b)∈[−1,1] n ×R m , the expectation off c with respect to the distributionS a is E x∼S a [f c (x,b)] =f c (a,b) = X S⊆[n] T⊆[k] ˆ f c (S,T)· Y i∈S a i · Y i∈T δ i (b) ! . Proof of Lemma 1. E x∼S a [f c (x,y)] = X x∈±1 n f c (x,δ(y))·S a (x) = X x∈±1 n X S⊆[n] T⊆[k] ˆ f(S,T)· Y i∈S x i · Y i∈T δ i (y) ! ·S a (x) = X S⊆[n] T⊆[k] ˆ f(S,T)· X x∈±1 n Y i∈S x i ·S a (x) ! · Y i∈T δ i (y) ! = X S⊆[n] T⊆[k] ˆ f(S,T)· E x∼S a " Y i∈S x i # · Y i∈T δ i (y) ! = X S⊆[n] T⊆[k] ˆ f(S,T)· Y i∈S a i · Y i∈T δ i (y) ! =f c (a,y) d i (b) is the expectation ofδ i (y) giveny∼ N(b,σ 2 I). Whenδ i (y) corresponds to a linear constraint of the form q ⊤ i y≤q i,0 , it can be written as d i (b) =− P y∼N(b,σ 2 I) m X j=1 q i,j y j −q i,0 ≤0 + P y∼N(b,σ 2 I) m X j=1 q i,j y j −q i,0 >0 = 1−2 P y∼N(b,σ 2 I) m X j=1 q i,j y j −q i,0 ≤0 Letz= P m j=1 q i,j b j −q i,0 ands 2 =σ 2 P m j=1 q 2 i,j . d i (z) = 1−2 P z ′ ∼N(z,s 2 ) [z ′ ≤0] = 1−2Φ −z s = 1−2· 1 2 1 + erf −z s √ 2 = erf z s √ 2 18 where Φ is the standard cumulative distribution function, and erf is the error function. By substitutingbandσback to the equation, we have d i (b) = erf P m j=1 q i,j b j −q i,0 q 2 P m j=1 q 2 i,j σ And the differentiation with respect tob j is ∂d i (b) ∂b j = √ 2q i,j q π P m j=1 q 2 i,j σ exp − P m j=1 q i,j b j −q i,0 2 q 2 P m j=1 q 2 i,j σ . Theorem 4 is the consequence of Lemma 1 with Gaussian samplingy∼N(b,σ 2 I). Theorem 4.For any point(a,b)∈[−1,1] n ×R m , the expectation off c (x,y)underx∼S a andy∼N(b,σ 2 I)is E x∼S a y∼N(b,σ 2 I) [f c (x,y)] = X S⊆[n] T⊆[k] ˆ f c (S,T)· Y i∈S a i · Y i∈T d i (b) ! . Moreover, whenσ 2 = 0, the expectation reduces to E x∼S a y∼N(b,σ 2 I) [f c (x,y)] =f c (a,b) Proof of Theorem 4.xis subject a binary ditributionS a andyis subject to Gaussian distributionN(b,σ 2 I). For the expectation on the joint distribution, we have: E x∼S a y∼N(b,σ 2 I) [f c (x,y)] = Z y∈R m X x∈±1 n f c (x,δ(y))·S a (x)·dy = Z y∈R m X S⊆[n] T⊆[k] ˆ f(S,T)· Y i∈S a i · Y i∈T δ i (y) ! ·dy(Due to Lemma 1) = X S⊆[n] T⊆[k] ˆ f(S,T)· Y i∈S a i · Y i∈T Z y∈R m δ i (y)·dy ! = X S⊆[n] T⊆[k] ˆ f(S,T)· Y i∈S a i · Y i∈T E y∼N(b,σ 2 I) [δ i (y)] ! = X S⊆[n] T⊆[k] ˆ f(S,T)· Y i∈S a i · Y i∈T d i (b) ! 19 Supplementary Note 3: Decision Diagrams To explicitly evaluate the WFE of a constraint requires state enumeration. This section introduces decision dia- grams, an efficient data structure for evaluating the constraints (via the equivalence between the COP of the decision diagram and expectation of the xWFE, as in Supplementary Note 4). GradSATavoids state enumeration by maintaining compact representations of Boolean functions using binary decision diagrams (BDDs) [24]. A BDD represents Boolean constraintsB n →Bas an ordered directed acyclic graph, where each node corresponds to a variable and each edge encodes a branching decision. Every decision node tests a Boolean variable and has two outgoing edges, corresponding to the true and false outcomes. To evaluate a BDD, variables are assigned values, and the diagram is traversed according to the corresponding branches until reaching a terminal node. The Boolean value at the terminal node is the output of the function for that assignment. In the extended algebraic decision diagram (xADD) framework [73], linear programming is often used to prune unreachable nodes (e.g., a branch followingy >1 cannot subsequently satisfyy <0), thereby yielding a minimal decision diagram. Motivated by the xADD, we generalize BDDs to handle continuous variables. xBDD provides a unified representation in which Boolean and real-valued variables are captured within a decision diagram through piecewise case statements. However, in our setting, we do not employ such pruning for two reasons. First, the canonicity of linear-programming-pruned diagrams remains an open question. Second, in the presence of probabilistic sampling, deterministically unreachable nodes can still be visited with non-zero probability. For example, ify= 1.1, samples drawn fromy ′ ∼ N(y,σ 2 ) may still yieldy ′ <0. Therefore, we treat an XBDD analogously to a BDD, interpreting atomic constraints as propositional variables, while acknowledging that minimality and canonicity are not guaranteed in the extended setting. Definition 2(Extended Binary Decision Diagram, xBDD).An xBDD is a directed acyclic graphG(V,E)representing a multivariate functionB n ×R m →B. Each decision nodev∈Vcorresponds either to a Boolean variable or to a theory atom over real variables. Each edgee∈Eis labeled(v,true)or(v,false), depending on the outcome of evaluating the decision nodev. A pathpinGis a sequence of edges such that each decision node appears at most once, with the edge labels indicating the branch taken at that node. Formally, a path can be written as a finite subset of all possible decision outcomes: p⊂(v 1 ,true),(v 1 ,false),(v 2 ,true),(v 2 ,false),· 20 Supplementary Note 4: Circuit-Output Probability In Supplementary Note 3 we present the decision diagram data structure. By running the message propagation algorithm (Supplementary Note 5) on the decision diagram, we can efficiently evaluate the COP, which is introduced in this section. The result in this section leads to Eq. (10) in the main text. The COP is defined as a special case of weighted model counting (WMC). To extend COP to adapt the real variable, we further discuss weighted model integration (WMI). Definition 3(Weighted model counting [74]).Letfbe a function over Boolean variablesx. LetW:−1,1 n →R be a weight function. The weighted model counting off c with respect toWis defined as WMC(W) = X x∈−1,1 n f(x,y)·W(x), HereWassigns a weight to each complete assignment, which can be expressed as the product of literal weights associated with Boolean variables: W(x) = Y x i =−1 ω T i · Y x i =1 ω F i whereω T i ,ω F i ∈Rare the literal weights. When the weights satisfyω T i +ω F i = 1, andω T i ,ω F i ≥0, the weighted model counting problem reduces to the circuit-output probability problem. And the weight function becomes an input probability function. The circuit- output probability (COP) offis defined as COP(S a ) = X x∈±1 n f(x)·S a (x), whereS a (x) is the randomized rounding distribution over Boolean variables,i.e., Eq. (3). Definition 4(Weighted model integration).Letfbe a function over Boolean variablesxand real variablesy. Let W:−1,1 n ×R m →Rbe a weight function. The weighted model integration off c with respect toWis defined as WMI(W) = X x∈−1,1 n Z y∈R m f(x,y)·W(x,y)dy, and W(x,y) = Y x i =−1 ω T i · Y x i =1 ω F i · m Y j=1 ω j (y j ). ω j is the weight of the real variable when taking a different valuey j . To generalize circuit-output probability for weighted model integration, the weight of the real variable should satisfy Z y j w j (y j )dy j = 1, and fory j ∈R,w j (y j )≥0. Remark 1(Circuit-output probability).Letf:±1 n ×R m → ±1be a function over propositional variablesx and real variablesy. LetP σ :±1 n+k →[0,1]denote the input probability distribution. Then the circuit-output probability (COP) off ′ is defined as COP(P σ ) = X x∈±1 n X z∈±1 k f(x,y)·P σ (x,z). Here, the input probability distribution factorizes as P σ (x,z) =S a (x)· P y∼N(b,σ 2 I) [δ(y) =z]. where P y∼N(b,σ 2 I) [δ(y) =z]is the probability that the atomic constraintsδ(y)evaluate tozunder Gaussian sampling. 21 Intuitively, the COP measures the probability that a constraint is satisfied under randomized Boolean rounding and Gaussian perturbation of real variables. Corollary 2.For any real point(a,b)∈[−1,1] n ×R m , letP σ denote the joint probability distribution induced byS a andN(b,σ 2 I). For an SMT(LRA) constraintc, the circuit-output probability satisfies COP c (P σ ) = E x∼S a y∼N(b,σ 2 I) [f c (x,y)]. LetC σ (a,b) = P c∈C w c ·COP c (P σ ), we have C σ (a,b) = E x∼S a y∼N(b,σ 2 I) [F w (x,y)] Particularly, whenσ= 0, the above reduced to C σ (a,b) =F w (a,b) Proof of Corollary 2.By the definition of circuit-output probability, we have COP c (P σ ) = X x∈±1 n X z∈±1 k f c (x,y)·P σ (x,z) = X z∈±1 k X x∈±1 n f c (x,y)·S a (x)· P y∼N(b,σ 2 I) [δ(y) =z] = X z∈±1 k E x∼S a [f c (x,y)]· P y∼N(b,σ 2 I) [δ(y) =z] = X z∈±1 k f c (a,y)· P y∼N(b,σ 2 I) [δ(y) =z] Define ̃ f c (x,δ(y)) =f c (x,y), we have COP c (P σ ) = X z∈±1 k ̃ f c (a,z)· P y∼N(b,σ 2 I) [δ(y) =z] = E y∼N(b,σ 2 I) h ̃ f c (a,z) i = E y∼N(b,σ 2 I) [f c (a,y)] = E x∼S a y∼N(b,σ 2 I) [f c (x,y)] For the weighted objective, by linearity of expectation, C σ (a,b) = X c∈C w c ·COP c (P σ ) = X c∈C w c · E x∼S a y∼N(b,σ 2 I) [f c (x,y)] = E x∼S a y∼N(b,σ 2 I) h X c∈C w c ·f c (x,y) i = E x∼S a y∼N(b,σ 2 I) F w (x,y) . 22 Supplementary Note 5: Message Propagation Direct evaluation or differentiation ofE[f c ] is, however, intractable, as it requires enumeratingO(2 n ) Boolean assignments. In contrast, message propagation on the associated xBDD (see Supplementary Notes 3 and 4) provides an efficient surrogate: both forward and backward traversals scale with the size of the decision diagram rather than with the exponential size of the Boolean domain. Thus, message propagation yields a tractable upper bound on computational cost. The procedure consists of two phases: forward propagation (Alg. 3) and backward propagation (Alg. 4). In the forward pass, top-down messages are initialized at the root and recursively distributed along decision edges according to assignment-dependent branching probabilities. The true terminal node accumulates the top-down message, which encodes the probability that constraintcis satisfied under Gaussian sampling. In the backward pass, bottom-up messages are initialized at the true terminal and propagated in reverse topological order. Local sensitivity terms are then computed by contrasting the adjoint contributions of the true and false successors. By leveraging message passing on xBDDs, we can evaluate the expectation of the objective function without explicit state enumeration. The following theorem formalizes the correctness and computational complexity of this procedure. Theorem 5(Evaluation).Alg. 3 returns the expectation of the objective function in Eq.(3). The complexity of running Alg. 3 scales atO( P c |V c |). To prove Thm. 5, we first reproduce Lem. 2 in [24]. Lemma 2.LetG c (V c ,E c )be an xBDD encoded constraintcand run Alg. 3 onG c . For a real assignment(a,b)∈ [−1,1] n ×R m , we have P[x i =−1] = 1−a i 2 , P[δ i (b) =−1] = 1−d i (b) 2 . Then for each nodev∈V c , we have m td [v] =Pr(G c ,v), wherePr(G c ,v)is the probability that the nodevis on the path generated byxandd(·)onG c . Proof of Lemma 2.We prove the statement by structural induction on xBDDG c . We first denote z= P[x 1 =−1]...P[x n =−1]P[d 1 (b) =−1]...P[d k (b) =−1] Basic step: For the root noderofG c , m td [v] = 1, where the statement holds becauseris on the path generated by every discrete assignment onG c . Inductive step: For each non-root nodevofG c , letpar T (v) be the set of parents ofvwith an edge labeled byTrue andpar F (v) be the set of parents ofvwith an edge labeled byFalsein xBDDG c . After Alg. 3 terminates, we have m td [v] = X u∈par T (v) z i ·m td [u] + X u∈par T (v) (1−z i )·m td [u] By inductive hypothesis, m td [v] = X u∈par T (v) z i ·Pr(G c ,u) + X u∈par T (v) (1−z i )·Pr(G c ,u) =Pr(G c ,v) The last inequality holds because the events of reachingvfrom different parents are exclusive. 23 Algorithm 3:Forward Traversal of XBDDs Input:A constraint setC, constraint weightw c ’s, a real assignment (a,b)∈[−1,1] n ×R m , and sampling areaσ Output:Objective function value 1fori∈range(n)do 2p i ← 1−a i 2 ; 3fori∈range(m)do 4p i+n ← 1−d i (b) 2 ; 5fval←0; 6forc∈Cdo 7Get the XBDDG c (V c ,E c ); 8Initializem td [v]←1 ifvis the root node; else 0; 9Sort node indexV←sorted(V c ); 10forv∈Vdo 11m td [v.t]←m td [v.t] +p id(v) ·m td [v]; 12m td [v.f]←m td [v.f] + (1−p id(v) )·m td [v]; 13fval←fval+w c ·(1−2·m td [V c [T]]) 14returnfval; Algorithm 4:Backward Traversal of XBDD Input:A constraint setC, constraint weightw c ’s, a real assignment (a,b)∈[−1,1] n ×R m , and sampling areaσ Output:Gradient of the objective function 1Run Alg. 1 to get forward messagem td ; 2fori∈range(1,n+m+ 1)do 3grad i ←0; 4forc∈Cdo 5Get the XBDDG c (V c ,E c ); 6Initializem bu [v]←1 ifvis the true node; else 0; 7Sort node indexV←sorted(V c ,reverse=true); 8forv∈Vdo 9m bu [v]←m bu [v] +p id(v) ·m bu [v.t]; 10m bu [v]←m bu [v] + (1−p id(v) )·m bu [v.f]; 11∆ =m td [v]·(m bu [v.F]−m bu [v.T]); 12ifid(v)≤nthen 13grad id(v) ←grad id(v) +w c ·∆; 14else 15fori∈range(1,m+ 1)do 16grad i+n ←grad i+n +w c · ∂d id(v) (b) ∂b i+n ·∆; 17returngrad; Proof of Theorem 5.The above Lemma shows that, after running Alg. 3, we have m td [V c [T]] =Pr(G c ,V c [T]) =COP c (P σ )(By definition of circuit-output probability) Complexity: Alg. 3 traverse all xBDDG c for allc∈C. The topological sort takesO(|V c |+|E c |) time by Kahn’s algorithm. The message propagation takesO(|E c |) time. Since|E c |= 2|V c |,i.e., all non-terminal nodes in xBDD only have two outgoing edges. Hence, the overall complexity scales atO(|V c |). By running Alg. 3 on xBDDs, the expectation can be obtained from top-down messages accumulated at the true terminal nodes. Darker colors correspond to larger message values, which in the example increase with successive gradient steps. We now extend this analysis to differentiation. The following theorem establishes the correctness and complexity of computing gradients of the objective function. Theorem 6(Differentiation).Alg. 4 returns the gradient of the expectation of the objective function in Eq.(3). The complexity of running Alg. 4 scales atO(m· P c |V c |). 24 To prove Thm. 6, we first reproduce Lem. 4 in [24]. Lemma 3.LetG c (V c ,E c )be an xBDD encoded constraintcand run Alg. 4 onG c . For a real assignment(a,b)∈ [−1,1] n ×R m , we have P[x i =−1] = 1−a i 2 , P[δ i (b) =−1] = 1−d i (b) 2 . Then, for each nodev∈V c , letf c,v be the subfunction corresponding to the sub-xBDD generated by regardingvas the root. The following holds: m bu [v] =COP c,v (P σ ). Proof of Lemma 3.We prove the statement by structural induction on xBDDG c . We first denote z= P[x 1 =−1]...P[x n =−1]P[d 1 (b) =−1]...P[d k (b) =−1] Basic step: For the terminal nodes, we have m bu [V c [T]] = 1, m bu [V c [F]] = 0. Since the subfunctions given byTrueandFalseare just Boolean constants, the statement holds. Inductive step: For each non-terminal nodevofG c , after Alg. 4 terminates, we have m bu [v] = 1−z i 2 ·m bu [v.T] + 1 +z i 2 ·m bu [v.F] By inductive hypothesis, m bu [v] = 1−z i 2 ·COP c,v.T (P σ ) + 1 +z i 2 ·COP c,v.F (P σ ) =COP c,v (P σ ) Proof of Theorem 6.With Lem. 2 and Lem. 3, we are ready to prove Thm. 6. Given an xBDDG c , we expand all terminal nodes such that each can have only one parent node. The expanded xBDD is calledG c ′ , which has a true terminal setTand a false terminal setF. By repeating the proof of Lem. 2 and Lem. 3 onG c ′ , for any non-terminal nodev /∈(T∪F), we have m ′ td [v] =m td [v] m ′ bu [v] =m bu [v] For any true terminal nodev∈Tand false terminal nodeu∈F, we have m ′ bu [v] = 1 m ′ bu [u] = 0 COP c (P σ ) =P[f c =−1|P σ ] = X v∈u:id(u)=i Pr(G ′ c ,v)·P[f c =−1|v,P σ ] = X v∈u:id(u)=i m ′ td [v]·m ′ bu [v] = X v∈u:id(u)=i m td [v]·m bu [v] = X v∈u:id(u)=i m td [v]·(z i ·m bu [v.T] + (1−z i )·m bu [v.F]) 25 Hence we have ∂COP c (P σ ) ∂z i = X v∈u:id(u)=i m td [v]·(m bu [v.T]−m bu [v.F]) ∂f c (a,b) ∂z i = X v∈u:id(u)=i m td [v]·(m bu [v.F]−m bu [v.T]) Complexity: Alg. 3 traverses all xBDDG c for allc∈C. The topological sort takesO(|V c |+|E c |) time by Kahn’s algorithm. The message propagation takesO(|E c |) time. For gradient computation, the worst case is that every literal is an atomic constraint that consists of allmreal variables. Therefore, the gradient computation takesO(m·|E c |) time. Since|E c |= 2|V c |,i.e., all non-terminal nodes in xBDD only have two outgoing edges. Hence, the overall complexity scales atO(m·|V c |). 26 Supplementary Note 6: Smoothness This section analyzes the Lipschitz continuity and local convexity ofC σ , both of which are critical for establishing convergence guarantees. Proposition 2(Lipschitz).Letα= P c w c andC σ : [−1,1] n ×R m →[−α,α]. Letβdenote the maximum num- ber of occurrences of any single continuous variable within a constraint. Letγ= √ 2β √ πσ . Then, for any two points (a ′ ,b ′ ),(a,b)∈[−1,1] n ×R m , we have |C σ (a ′ ,b ′ )−C σ (a,b)|≤ρ ∥a ′ −a∥ 2 +∥b ′ −b∥ 2 1 2 ∥∇C σ (a ′ ,b ′ )−∇C σ (a,b)∥≤L ∥a ′ −a∥ 2 +∥b ′ −b∥ 2 1 2 whereρ=α √ n+mmax (1,γ)andL= p n+mγ 2 ρ. As a consequence of the Lipschitz continuity [75], we have C σ (a ′ ,b ′ )−C σ (a,b)−⟨∇ a C σ (a,b),a ′ −a⟩−⟨∇ b C σ (a,b),b ′ −b⟩ ≤ L 2 ∥a ′ −a∥ 2 +∥b ′ −b∥ 2 (61) Proof of Proposition 2. ∇ b j d i (b) = √ 2q i,j √ πσ∥q i ∥ exp − P m j=1 q i,j b j −q i,0 2 2σ 2 ∥q i ∥ 2 ∇ b j d i (b) = √ 2|q i,j | √ πσ∥q i ∥ exp − P m j=1 q i,j b j −q i,0 2 2σ 2 ∥q i ∥ 2 ≤ √ 2|q i,j | √ πσ∥q i ∥ ≤ √ 2 √ πσ Therefore, we can have ∇ b j COP c (a,b) =∇ b j X S⊆[n] T⊆[k] ˆ f c (S,T)· Y i∈S a i · Y i∈T d i (b) ! = X S⊆[n] T⊆[k] ˆ f c (S,T)· Y i∈S a i ·∇ b j Y i∈T d i (b) !! = X S⊆[n] T⊆[k] ˆ f c (S,T)· Y i∈S a i · X i∈T ∇ b j d i (b)· Y k∈T,k̸=i d i (b) Suppose a real variableb j appears in the constraint at mostβtimes. Equivalently, letK=i:b i,j ̸= 0, then 27 |K|≤β. Then the above reduces to ∇ b j COP c (a,b) = X j ′ ∈K X S⊆[n] T⊆[k] ˆ f c (S,T)· Y i∈S a i ·∇ b j d j ′ (b)· Y i∈T,i̸=j ′ d i (b) = X j ′ ∈K ∇ b j d j ′ (b)· X S⊆[n] T⊆[k] ˆ f c (S,T)· Y i∈S a i · Y i∈T,i̸=j ′ d i (b) = X j ′ ∈K ∇ b j d j ′ (b)· X S⊆[n] T⊆[k] ˆ f c (S,T)· Y i∈S a i · Y i∈T d i (b) ! ∇ b j COP c (a,b) ≤ X j ′ ∈K ∇ b j d i (b) | z ≤ √ 2 √ πσ · X S⊆[n] T⊆[k] ˆ f c (S,T)· Y i∈S a i · Y k∈T,k̸=i d i (b) | z ≤1 ≤ √ 2β √ πσ =γ. Then we have ∇ b j C σ (a,b) = X c∈C w c ·∇ b j COP c (a,b) ≤ X c∈C w c ·∇ b j COP c (a,b) ≤ X c∈C |w c |· ∇ b j COP c (a,b) ≤αγ. Leta (i) = [a 1 ,·,a i−1 ,a ′ i ,·,a n ] andb (i) = [b 1 ,·,b i−1 ,b ′ i ,·,b ′ m ], then we have: |C σ (a ′ ,b ′ )−C σ (a,b)|≤ n X i=1 C σ (a (i) ,b)−C σ (a (i−1) ,b) + m X i=1 C σ (a ′ ,b (i) )−C σ (a ′ ,b (i−1) ) = n X i=1 (a ′ i −a i )∇ a i C σ (a (i−1) ,b) + m X i=1 (b ′ i −b i )∇ b i C σ (a,b (i−1) ) ≤α n X i=1 |a ′ i −a i |+αγ m X i=1 |b ′ i −b i | ≤αmax (1,γ) n X i=1 |a ′ i −a i |+ m X i=1 |b ′ i −b i | ! ≤αmax (1,γ) √ n+m ∥a ′ −a∥ 2 +∥b ′ −b∥ 2 1 2 |z Due to Cauchy–Schwarz inequality , where we denoteρ=α √ n+mmax (1,γ). Note that we can view∇C σ (a,b) as a vector ofn+mmultilinear-like functions. 28 ∥∇C σ (a ′ ,b ′ )−∇C σ (a,b)∥ 2 = n X i=1 (∇ a i C σ (a ′ ,b ′ )−∇ a i C σ (a,b)) 2 + m X j=1 ∇ b j C σ (a ′ ,b ′ )−∇ b j C σ (a,b) 2 ≤ n X i=1 ρ 2 (a ′ −a) 2 + (b ′ −b) 2 + m X j=1 ρ 2 γ 2 (a ′ −a) 2 + (b ′ −b) 2 = (n+mγ 2 )ρ 2 (a ′ −a) 2 + (b ′ −b) 2 ∥∇C σ (a ′ ,b ′ )−∇C σ (a,b)∥≤ρ p n+mγ 2 ∥a ′ −a∥ 2 +∥b ′ −b∥ 2 1 2 Then we haveL=ρ p n+mγ 2 . We next investigate the local convexity ofC σ and its descent property, which are essential for analyzing gradient- based methods. Proposition 3(Local convexity [75]).SupposeC σ is locally convex on a convex set∆.Let(a ∗ ,b ∗ ) = arg min (a,b)∈∆ C σ (a,b). Then, for all(a,b)∈∆, ⟨∇ a C σ (a ∗ ,b ∗ ),a−a ∗ ⟩+⟨∇ b C σ (a ∗ ,b ∗ ),b−b ∗ ⟩≥0. The following property of the projected gradient mapping provides a key inequality for convergence analysis. Proposition 4(Inequality of gradient mapping [76]).IfC σ is locally convex on a convex set∆, then for every (a,b)∈∆, ⟨∇C σ (a,b),g(a,b)⟩≥∥g(a,b)∥ 2 . Equipped with the above results, we present convergence guarantees for our projected gradient approach in the following lemma and theorem. Lemma 4(Descent Lemma).For the objective functionC σ under linear constraints, letgdenote its projected gradient. If the step size satisfiesη≤ 1 L , then the projected gradient descent sequence obeys C σ a (t+1) ,b (t+1) −C σ a (t) ,b (t) ≤− η 2 ∥g a (t) ∥ 2 Proof of Lemma 4.The proof takes the positive side of Eq. (61) to establish the gradient descent step. C σ (a,b)≤C σ (a ′ ,b ′ ) + ∇C σ (a ′ ,b ′ ), a−a ′ b−b ′ + L 2 ∥a−a ′ ∥ 2 +∥b−b ′ ∥ 2 Let (a,b) = (a ′ ,b ′ )−ηg(a ′ ,b ′ ), the above inequality becomes C σ (a,b)≤C σ (a ′ ,b ′ )−η⟨∇C σ (a ′ ,b ′ ),g(a ′ ,b ′ )⟩+ η 2 L 2 ∥g(a ′ ,b ′ )∥ 2 . Applying Proposition 4 and letη≤ 1 L , we then have C σ (a,b)≤C σ (a ′ ,b ′ )−η∥g(a ′ ,b ′ )∥ 2 + η 2 ∥g(a ′ ,b ′ )∥ 2 =C σ (a ′ ,b ′ )− η 2 ∥g(a ′ ,b ′ )∥ 2 . Lemma 4 implies that, if projected gradient descent is run for sufficient iterations, the sum of gradient norms is always bounded by a constant, which further implies convergence to a stationary point,i.e., Theorem 7. Theorem 7(Convergence Speed).With step sizeη= 1 L , the projected gradient descent converges to anε-projected- critical point(a ∗ ,b ∗ )inO( αL ε 2 )iterations. 29 Proof of Theorem 7.From Lemma 4, we can assumeη= 1 L . Consider a sequence of pointsa (t) ’s andb (t) ’s such that a (t+1) ,b (t+1) = a (t) ,b (t) +ηg a (t) ,b (t) . Due to Lemma 4 we haveC σ a (t+1) ,b (t+1) −C σ a (t+1) ,b (t) ≤ η 2 ∥g(a (t) ,b (t) )∥ 2 . Given any initial pointa (0) ,b (0) , it will converge toa ∗ ,b ∗ . AfterTgradient steps, we have C σ (a ∗ ,b ∗ )−C σ a (0) ,b (0) ≥ 1 2αL T X t=0 ∥g(a (t) ,b (t) )∥ 2 ≥ T+ 1 2αL min t ∥g(a (t) ,b (t) )∥ 2 , which can be rewritten as min t ∥g(a (t) ,b (t) )∥≤ r 2L T+ 1 q C σ (a ∗ ,b ∗ )−C σ a (0) ,b (0) ≤ r 2L T+ 1 √ 2α To achieve a pointa (T) such that∥g(a (t) )∥≤ε, we require q 4αL T+1 ≤ε, which impliesT∼O αL ε 2 . 30 Supplementary Note 7: Local Lipschitz In the Supplementary Note 6, Prop. 2, we established global Lipschitz continuity of the smoothed objective and its gradient over the entire domain. Here, we provide a complementary result showing thatC σ admits tighter local Lips- chitz constants when the real-valued variables are away from the transition regions induced by the atomic constraints. This refinement is useful for analyzing convergence behavior in the regions close to the minima. Corollary 3(Local Lipschitz).For every atomic constraintα i , we define the transition regionr i by y m X j=1 q i,j y j −q i,0 2 < σ 2 ln 2β 2 πσ 2 , andR= S i r i . For any two points points(a ′ ,b ′ ),(a,b)∈[−1,1] n ×(R m ), we have |C(a ′ ,b ′ )−C(a,b)|≤α √ n+m(∥a ′ −a∥+∥b ′ −b∥), ∥∇C σ (a ′ ,b ′ )−∇C σ (a,b)∥≤α(n+m) ∥a ′ −a∥ 2 +∥b ′ −b∥ 2 1 2 Proof of Corollary 3.The transition regionr i is defined such that for any pointb∈R m i , we have ∇ b j d i (b) ≤ 1 β . And hence √ 2|q i,j | √ πσ∥q i ∥ exp − P m j=1 q i,j b j −q i,0 2 2σ 2 ∥q i ∥ 2 ≤ 1 β m X j=1 q i,j b j −q i,0 2 ≥−2σ 2 ∥q i ∥ 2 ln √ πσ∥q i ∥ √ 2β|q i,j | =σ 2 ln 2β 2 πσ 2 For any pointb∈R m i , ∇ b j COP c (a,b) ≤ X j ′ ∈K ∇ b j d i (b) | z ≤ 1 β · X S⊆[n] T⊆[k] ˆ f c (S,T)· Y i∈S a i · Y k∈T,k̸=i d i (b) | z ≤1 ≤β· 1 β = 1 ∇ b j C σ (a,b) ≤ X c∈C |w c |· ∇ b j COP c (a,b) ≤α·1 =α. For the objective function, we have 31 |C(a ′ ,b ′ )−C(a,b)|≤ n X i=1 C(a (i) ,b)−C(a (i−1) ,b) + m X i=1 C(a ′ ,b (i) )−C(a ′ ,b (i−1) ) ≤α n X i=1 |a ′ i −a i |+α m X i=1 |b ′ i −b i | ≤α √ n+m ∥a ′ −a∥ 2 +∥b ′ −b∥ 2 1 2 . For the gradient, we have ∥∇C σ (a ′ ,b ′ )−∇C σ (a,b)∥ 2 = n X i=1 (∇ a i C σ (a ′ ,b ′ )−∇ a i C σ (a,b)) 2 + m X j=1 ∇ b j C σ (a ′ ,b ′ )−∇ b j C σ (a,b) 2 ≤ n X i=1 α 2 (n+m) (a ′ −a) 2 + (b ′ −b) 2 + m X j=1 α 2 (n+m) (a ′ −a) 2 + (b ′ −b) 2 =α 2 (n+m) 2 (a ′ −a) 2 + (b ′ −b) 2 ∥∇C σ (a ′ ,b ′ )−∇C σ (a,b)∥≤α(n+m) ∥a ′ −a∥ 2 +∥b ′ −b∥ 2 1 2 32 Supplementary Note 8: Optimality Thm. 2 is the main text states that, whenσ= 0, the projected gradient will converge to the boundary of the feasible domain. This section proves Thm. 2 by finding a gradient direction of the objective function in the open domain. If the descent direction always exists, then the convergence point will be on the boundary of a closed domain. Lemma 5(Gradient Direction).Letf:R n ×R m →Rbe expressible as a multilinear-like polynomial: f(a,b) = X S⊆[n] T⊆[k] ˆ f(S,T)· Y i∈S a i · Y i∈T δ i (y) ! ,(81) where ˆ f(S,T)’s are the Walsh-Fourier coefficients and at least one coefficient is nonzero. Then for every point(a,b)∈R n ×R m , there exist a region sizeE>0and two directionsv + ,v − ∈R n such that for allε∈(0,E), f(a+εv + ,b)> f(a,b), f(a+εv − ,b)< f(a,b). Proof of Lemma 5.Lemma 3 in [76] has shown that any multilinear functionhand a pointa∈R n , there exist a region sizeε >0 and two directionv + ,v − ∈R n , such that for allε∈(0,ε + ), the following holds h(a+εv + )> h(a) h(a+εv − )< h(a) Given the multilinear-like functionfand any point (a,b)∈R n ×R m , the function can be written as g(a) =f(a,b) = X S⊆[n] T⊆[k] ˆ f(S,T)· Y i∈T δ i (b) ! · Y i∈S a i = X S⊆[n] ˆg b (S)· Y i∈S a i where ˆg b (S) is the coefficient. ˆg b (S) = X S⊆[T] ˆ f(S,T)· Y i∈T δ i (b) If the coefficient ˆ f(S,T) is not 0, then ˆg(S) will not be 0 sinceδ i (b)∈±1. Wheng(a) is a non-constant multilinear function ofa, and we can have f(a+εv + ,b)> f(a,b), f(a+εv − ,b)< f(a,b). Lemma 5 implies that Eq. (81) admits no local optima within the open domain (−1,1) n ×R m . This directly results in Theorem 2. 33 Supplementary Note 9: Technical Proofs Some proofs are provided in the supplementary notes where the corresponding results first appear. This section presents the proofs of the theoretical results stated in the main text. Proof of Theorem 1 The CLS approach relies on Thm. 1 in the main text. This subsection proves Thm. 1. Each atomic constraint partitions the real space into finitely many polyhedral regionsa 1 ,...,a N , the objectiveF w admits the case representation f c (x,y) = f c (x|y∈a 1 ) ify∈a 1 , . . . f c ify∈a N . Letf (i) c (x) =f c (x|y∈a i ), which is a multilinear polynomial inx. The Lem. 1 in [76] states that, ifx∈[−1,1], fori∈1,...,N, we havef (i) c (x)∈[−1,1]. Since the above statement holds in each case, it immediately yields the following Lemma. Lemma 6.If(x,y)∈[−1,1] n ×R m , we havef c (x,y)∈[−1,1]. Now we are ready to prove Thm. 1. Proof of Theorem 1. •“⇒”: SupposeF= V c∈C cis satisfiable and (x,y)∈ ±1 n ×R m is one of its solutions. Then (x,y) is also a solution for every constraintc. Thus, for everyc∈C,f c (x,y) =−1. ThereforeF w (x,y) =− P c∈C w c and min x∈[−1,1] n y∈R m F w (x,y) =− X c∈C w c . •“⇐”: Suppose min x∈[−1,1] n y∈R m F w (x,y) =− X c∈C w c . There must exists (x,y)∈ ±1 n ×R m such thatF w (x,y) =− P c∈C w c . By the above Lemma, (x,y) is a solution off c for everyc∈C. Thus (x,y) is also a solution ofF w . Proof of Proposition 1 Our CLS approach relies on projected gradient descent,i.e., the complexity of the projection heavily affects the performance of CLS. This section proves that the projection in our CLS approach is a convex problem. Proof of Proposition 1.Firstly, the minimization objective function in the matrix form is a b ⊤ I n 0 0I m | z Hessian a b −2 (a ′ ) ⊤ (b ′ ) ⊤ a b , up to an irrelevant constant. The Hessian is diag(I n ,I m ), which is an identity matrix,e.g., positive definite and convex. Therefore, the minimization objective function is a convex function. Secondly, the box constraints−1≤a i ≤1,∀idefine a closed halfspace. The unit theory atoms P m k=1 q j,k b k −q j,0 ▷◁0 are linear inequalities or equalities. The intersection of two convex sets is, therefore, convex. 34 Supplementary Note 10: Per-Instance Benchmark Results The main text summarizes the overall performance across the three benchmark suites. Here, we present the complete per-instance runtime results for all solvers.FourierSMTis executed using 8 GPUs in parallel, and the median runtime per instance is reported in the main text. To complement this, we first report the per-GPU runtime statistics in Table I, Table I, and Table I. We then provide the full per-instance runtimes of all solvers in Table IV, Table V, and Table VI. Eventually, we summarize the results of Table V, and Table VI into Fig. 5. Table I:Per-instance runtime of FourierSMT for the random hybrid-constraint benchmark.Eight GPUs use different seed num- bers. 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. Instances01234567 10009.9818.5309.1228.41710.1398.9668.76610.231 100110.22610.00510.0718.73610.22510.22010.14411.852 100210.49410.31110.07412.36210.25910.95310.81212.552 100 312.85611.40010.10913.10310.33510.98012.99114.721 100413.02112.79010.58814.66410.33912.56313.17114.824 100514.09413.07112.36214.68910.42813.78613.57314.862 100614.40613.91513.81114.82012.98914.28813.78714.866 100714.52113.92714.44315.09913.89214.29714.22415.022 100814.52514.01614.45415.11514.05314.34114.22515.282 100914.66214.39914.59615.23914.55914.41714.27315.350 200014.80414.58814.74415.31714.62214.62714.28015.396 200 115.10914.69214.78015.35714.82014.73014.47315.452 200 215.24314.79514.87615.46014.91614.99114.93615.510 200315.43014.92614.91715.48815.03915.29915.18615.770 200 415.48714.96714.98315.65215.26915.33615.43715.860 200515.52014.99814.99415.67515.35515.40015.50516.091 200615.68415.01915.08615.84415.35915.41815.59616.251 200715.73415.06915.34215.95515.47315.52515.60516.308 200815.75615.10915.37916.01315.55015.55715.83116.331 200915.78315.41715.53316.06315.57715.61415.92616.356 300015.96215.45015.68916.07415.82016.23216.05116.450 300115.98715.46015.70816.13915.95616.28016.09916.537 300216.07315.97015.76516.28615.99716.30516.15416.684 300 316.14316.16815.83116.31316.08516.32016.20816.779 300 416.16316.37316.19616.43616.31916.45616.36416.832 300516.18216.73716.38516.45616.37316.47616.43517.055 300 616.23517.12616.44116.61716.41716.56316.46917.289 300716.23717.46716.57716.79816.49116.57116.96417.297 300816.27417.53316.58916.89816.53316.62116.99317.510 300916.28617.59616.76116.98716.59516.69117.02817.549 400016.35017.67816.77917.37316.85216.70917.04817.559 400116.37317.68716.78417.40316.88316.72817.08217.606 400 216.49117.69116.89317.48417.01717.13817.09517.663 400316.59417.78817.19117.70017.04117.15917.21917.688 400 416.62717.80317.22717.79917.14117.20417.26917.700 400516.64917.81217.31417.81317.22217.38817.42117.899 400616.74417.83017.41617.85017.49317.40417.53617.909 400 716.83717.91217.57217.88217.58317.49217.60517.930 400816.88817.94417.57418.02117.83617.60117.64217.997 400 916.95218.05017.73418.02817.95317.64117.69818.045 500017.18518.20617.91918.04717.97317.74717.70718.121 500117.24718.25918.02918.08517.99717.78817.72818.122 500 217.33718.35518.11218.13418.15317.80717.78418.132 500317.34318.39818.18118.14118.16018.01117.80318.142 500 417.59618.73818.27218.16418.25918.20417.94818.286 500517.63118.75218.36118.35718.43918.27117.95218.301 500617.77618.75818.40418.39318.45018.35817.99218.319 500718.30318.77718.50918.42718.45218.36918.22518.330 500818.60118.84818.60918.44418.49818.39518.33918.363 35 500918.70718.87118.64718.68718.52718.48018.35818.598 600018.84218.89718.71718.80918.62918.50918.36218.692 600 118.93418.89918.75118.86718.92418.52418.38418.702 600219.00318.91918.81919.03019.12918.78118.44918.804 600319.02219.12218.90419.37319.36818.82518.49618.903 600419.19919.26218.92619.38519.48718.85318.57319.056 600519.24219.36019.08219.43219.49219.00418.62419.191 600619.24319.44219.12219.53119.53019.28218.79519.221 600 719.41419.57119.16619.54819.60219.30118.81319.330 600819.45419.93219.36219.58919.68519.32318.83819.351 600919.47920.09919.42519.77919.92719.45118.85019.411 700019.64220.23219.42620.11320.00419.45118.91319.900 700120.00620.27219.43320.77520.01719.52818.97920.529 700220.26920.41720.16320.89820.27419.54019.32720.591 700320.27120.71320.38820.91520.53219.57019.38820.600 700 420.48020.71720.70520.92520.66519.57819.72220.677 700520.49620.73220.77120.93720.67619.90419.83620.830 700620.69220.75420.81521.14220.84820.49019.88620.854 700720.72521.54020.89321.62620.90220.50719.93020.864 700820.73921.78321.02121.64620.93520.50920.04220.992 700920.77022.00421.13121.96921.12220.92520.48021.174 800020.92722.15621.13222.07921.12421.06620.68321.242 800 121.13622.22821.22522.31321.20721.76520.90821.245 800221.35222.29421.62022.94221.88421.95220.96621.357 800321.53622.43821.75123.35222.21821.95320.99621.544 800421.81222.52322.35224.12422.24522.07321.02721.884 800521.84022.78522.37624.86522.38022.08421.03822.181 800622.10322.80722.40925.04222.42522.12821.05722.294 800722.23122.84222.54525.30322.68222.34921.25322.397 800822.44222.88922.58926.09722.82122.35421.26722.414 800922.47822.93322.62526.12123.05022.50821.64522.557 900022.57323.35522.82526.13423.08122.62521.86622.586 900 122.73523.44522.94226.35023.22722.63622.12222.871 900 222.81723.46923.23626.96223.38622.64722.32623.251 900 322.85623.66123.33427.08623.63422.66222.37323.548 900423.28223.77323.52427.33323.64622.74022.53523.551 900523.39924.91424.08828.12823.80823.11022.63623.575 900624.06925.64724.46529.12223.96823.51322.68923.753 900724.13626.51825.39129.17423.99123.88022.68924.101 900825.44327.44625.66229.72825.14824.08522.69424.262 900925.84728.09925.89029.81225.70326.25122.96024.339 1000028.81828.18028.34430.46526.72426.42423.00825.007 1000130.32428.45532.47332.41028.25930.33323.14026.395 1000230.39928.73133.81734.72333.57930.73423.39127.706 1000 330.83231.55139.70935.62342.01833.45125.47028.065 1000 431.48033.16840.42042.75742.16835.79528.17434.467 1000 537.98249.74754.80448.21556.23037.69431.34035.609 1000638.55350.55657.522569.28667.47338.96239.40539.781 1000 746.62352.47261.477588.018564.54945.01056.77356.978 1000853.39556.276615.299623.060635.63759.58159.34574.874 1000 9642.772627.007634.551654.337641.55162.874633.074630.581 Table I: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. Instances01234567 162027.11028.16327.51727.47226.96924.36321.77316.021 162115.05817.11413.98429.76216.87716.96813.73517.574 162212.49213.12012.74012.34512.99713.26613.47712.797 162312.29212.42311.66722.21611.52412.73511.09327.390 36 16249.83611.12011.54010.51011.03211.60712.16611.090 16258.7239.06410.5559.7739.1739.88410.5758.529 16 268.6339.2139.5039.3698.7168.5589.1739.500 162710.2268.5159.37712.2889.60110.1629.7159.783 162812.5379.90311.71410.71610.62510.4189.54810.860 162910.68111.02310.0838.5409.0239.62010.5319.517 163010.04610.34111.03811.4789.87410.3589.95210.441 163110.07510.4029.73010.62010.6039.12311.4709.257 16 3211.32512.93910.82111.89712.66813.03011.35611.276 16339.8229.68810.31211.6429.8409.5769.2279.320 163412.07111.98412.52511.63311.0239.91411.96611.006 163524.00725.66011.68023.65013.76911.73612.50523.719 163611.80111.31811.26413.27712.29411.93511.49011.289 16379.75610.66010.98011.4429.76110.26010.18410.306 163828.98510.87012.55925.01112.01412.06711.57912.454 16 3910.92310.97810.50811.25811.78111.12710.62510.286 164010.75710.01911.99813.10910.94010.27712.58610.270 164126.02627.42527.29324.42439.87712.70211.77339.482 164211.91011.79412.37611.61911.75610.19110.2519.884 164311.06012.11612.36512.06910.68811.16211.78519.462 164410.34410.71410.24110.49511.21911.50411.16413.126 164511.42611.45612.4359.82710.75111.75311.06410.641 16 4624.18417.22712.19825.21123.74425.57711.68911.040 164713.02812.42711.34310.92310.99810.16011.82010.703 164826.68518.30535.62525.83526.79538.45938.36225.770 164911.99112.47113.36712.05812.19211.78110.92612.881 165012.02011.21012.85311.41413.30212.10812.45612.367 165111.73812.11410.47810.77713.34412.78911.68311.025 165212.37211.44912.50010.09910.84913.70112.32223.700 165312.31313.96612.78313.90011.83510.69410.85615.033 165413.14328.03723.91711.76027.07412.38210.42511.153 165562.16757.158130.87865.56347.47766.533195.67449.349 16 5612.18512.20510.65811.90611.18912.95513.26212.049 16 5712.10512.52412.74811.91511.65611.19512.36311.459 16 5824.39612.36013.04424.47626.08622.67912.79325.501 1659301.099531.010689.07371.23653.08480.460295.050307.914 322010.4839.2469.97210.59811.57110.70610.75210.049 322110.23113.32310.85512.16211.51510.39012.96811.171 322210.66011.91512.14812.33611.39313.19213.68811.668 322310.45710.13811.34111.31512.35810.02510.34111.482 322411.13711.7139.55310.80211.08411.51310.1779.497 322512.33010.75111.03712.26312.84511.54811.66512.269 322611.81510.78511.74311.17912.53312.81611.41211.984 322720.49713.49118.80418.97721.10211.00521.29218.941 32 2827.84223.05112.26113.07026.92014.35612.24930.516 32 2914.50518.75318.65712.5249.85114.66118.09012.539 32 3013.52114.61811.62511.82412.68011.84510.24811.183 323111.92012.20311.79212.45412.13010.63410.54511.275 32 3211.78311.97910.85711.34213.20511.88723.47911.551 323313.75031.39232.24332.76519.02568.08329.42333.427 32 3413.79110.81412.98311.23511.35110.00410.91310.289 323511.00010.80211.75711.63013.62311.59211.90711.685 323612.66013.70212.46312.18212.34113.64513.26311.644 32 3715.53911.31212.36813.97311.01311.84311.40111.902 323811.30615.56111.43313.16611.28613.49922.24510.654 32 3912.54913.29112.20412.15213.36719.42912.37312.966 324021.49614.83514.30321.83516.60714.56314.34614.728 32 4118.92412.18527.57719.02333.99730.10028.48014.447 324221.39320.69320.04125.23315.64411.52123.20424.660 324324.18622.93121.93912.60515.30821.85824.56725.342 32 4411.67112.74911.95011.59610.52312.17712.07712.394 324513.03214.90916.06813.29414.50914.64214.18513.640 32 4614.76514.58814.37213.35610.98513.97915.64912.813 324713.32532.49227.17024.67916.94241.12216.04047.731 37 324812.07611.93012.89210.79212.46211.65211.97812.045 324913.52314.58916.66512.59513.33614.49814.66811.851 32 5027.31626.46026.40327.21824.46325.56824.70824.374 325113.05712.86627.97532.20625.17216.35526.77315.960 325227.00031.88328.75416.16013.06629.47913.08028.279 325313.26312.72912.88213.62513.69116.08813.28114.505 325415.48013.98512.65613.63813.77713.51214.60212.753 325525.26217.86918.74225.34124.42814.52524.92426.158 32 5625.04814.83225.24323.47525.96114.38213.76424.829 325737.131153.09326.37725.76916.097173.19026.96823.858 325812.26714.35117.18113.92514.52815.12512.22314.410 325913.21913.43015.11812.53015.29712.81413.46012.927 642013.66412.43712.64712.83712.50212.44612.33412.318 642115.14012.90414.16712.85612.72913.80615.69013.283 642214.48513.61611.74112.53012.03912.78012.63611.734 64 2322.62025.44623.97524.11723.54229.23713.19022.611 642411.90911.80511.70012.70111.22611.73711.66111.464 642513.45411.62813.95912.02112.97812.80112.21811.224 642612.62413.25113.04612.93512.70614.21013.19713.330 642711.72712.56012.72511.82412.11513.46110.91811.483 642811.46912.83012.36511.44811.06111.61011.75412.756 642912.35613.11914.98713.54514.09914.93615.59012.987 64 3013.73316.60513.10414.47914.31113.89713.40013.454 643113.38613.80915.67413.70614.38813.12514.68014.588 643212.79515.67612.63912.72414.02113.61213.35813.911 643313.16816.07915.66723.58612.65815.46315.05416.244 643414.81630.62215.36714.87114.47914.39511.94215.939 643512.50814.21015.19718.01415.12416.27512.71012.567 643614.01912.21611.96812.58912.73813.66412.99513.291 643715.77116.98616.69217.73414.95516.65017.74718.929 643813.91116.00715.85815.81615.40213.87814.73123.682 643916.04216.19215.38018.09615.97015.44216.52515.758 64 4016.29616.35816.04616.38017.34615.67817.74517.582 64 4117.23816.35119.77619.61416.93917.04618.86816.505 64 4215.47815.33916.50917.52816.49718.49614.81015.672 644319.04129.54031.08934.41617.97618.57034.47629.800 644417.91716.95318.79317.19017.87518.11715.94015.401 644517.12433.75919.83731.80119.68032.22918.71416.816 644614.60618.02016.59918.16816.89417.27516.56418.310 644717.44316.80715.97616.72319.82217.60117.33716.263 644816.95316.72616.61219.59816.23718.66216.59815.409 644916.27716.78016.38216.20015.97416.22416.75115.729 645019.78620.32923.13119.89725.67519.09021.95416.985 645138.30420.92035.06125.80436.60921.15536.92120.276 64 5218.04318.89018.55418.27417.41817.90520.25118.659 64 5334.89619.72919.92321.05924.11919.92520.71920.448 64 5442.19038.72450.27739.99640.32744.90621.73220.652 645521.16622.66036.90021.10036.36535.46635.07223.821 64 5638.81549.90568.72759.03455.22851.06463.88457.872 645732.83223.01819.14519.59422.19422.74537.18534.323 64 5822.24434.83422.05520.48020.51917.70223.43821.411 645919.60222.78641.67820.90522.04839.60233.34022.719 1282017.18618.23817.10016.19316.11316.56515.69417.820 128 2118.00915.84015.46015.26319.92916.17016.56417.162 1282216.18717.12215.88716.49815.87718.01617.36515.236 128 2317.64416.81020.14216.78923.22718.80519.53532.824 1282426.80316.97416.44717.59318.34216.25116.94319.176 128 2520.58816.41919.42917.42616.99218.54556.90219.070 1282615.94716.39516.38316.65616.02315.34517.66416.512 1282717.11916.64117.13118.56617.00216.42018.00616.870 128 2816.08816.78418.12219.03218.45316.58916.77517.319 1282916.27720.03517.58918.78417.57517.62215.99817.580 128 3021.81422.90822.69421.04522.25726.84423.21521.967 1283124.54227.29028.97626.64426.40426.57026.87525.465 38 1283226.23324.38727.15426.67327.60425.84326.14027.728 1283323.43324.16524.23924.98523.85925.26326.64421.746 128 3422.65622.50523.45624.60722.88224.25423.50823.515 1283527.08422.43022.06922.45123.92621.36321.38925.000 1283624.40422.06922.52421.73720.98822.77621.86921.904 1283721.94922.76021.93922.41920.80222.89522.07622.004 1283825.27841.06446.07949.89624.95239.09744.15242.200 1283926.32023.34222.78226.44921.88627.21021.89021.438 128 4031.35434.27735.83334.63132.31533.13833.20831.483 1284135.46038.66634.69636.28636.39939.08236.15839.808 1284230.82034.83133.03831.32333.79132.63532.80132.062 1284333.10733.99338.27037.19033.63635.05233.06433.784 1284431.29735.01130.51030.17331.86530.46636.40835.652 1284536.00233.80436.16134.64033.19636.07633.12636.359 1284630.06331.46232.92733.70030.79830.79836.41232.336 128 4733.85033.71035.20433.94533.42433.66934.79534.238 1284832.93038.87434.59637.31333.87632.95932.67332.540 1284940.25448.42038.96642.78566.77162.73361.48360.388 1285046.13242.53941.45242.32942.44649.04841.98943.535 1285144.16244.85043.88044.10144.79144.39044.15446.281 1285243.05645.92643.36543.57445.55647.10143.96844.200 1285342.99343.13845.97143.83444.42443.53744.53141.824 128 54697.360193.551361.557558.898191.024166.769198.631358.692 1285549.26851.98951.39247.39352.99746.76547.77444.647 1285647.84045.97645.57247.87582.27554.70044.37445.443 1285746.18746.68944.22749.37145.05846.76746.29445.219 1285845.40451.69143.83445.57146.11947.09847.10451.651 1285956.45381.09845.87346.74448.80946.91348.79549.198 2562035.90836.67237.32134.98235.63734.89935.74933.948 2562139.40037.32636.82437.64136.58237.47937.11134.659 2562236.01035.61935.99441.82536.14235.81534.48236.828 2562350.90543.85951.60838.89941.88038.64042.05844.878 256 2437.91735.47437.43137.16737.16236.95135.42037.637 256 2536.33837.46439.06037.24841.10235.79237.97136.381 256 2641.92537.21034.79940.69235.70733.98236.00434.329 2562738.07337.47247.74136.66639.49138.31137.42537.082 2562836.43042.10352.09534.87335.79335.19034.21034.592 2562945.92845.20452.71740.02141.33739.56348.81242.727 2563089.47279.31476.43283.416121.65377.03072.37495.447 2563196.00480.15088.21177.21069.21666.36779.16580.615 2563269.88785.54281.06863.32765.14362.78763.73974.472 2563370.51168.12569.73762.73260.71461.74561.55463.700 2563494.28082.15676.839229.78277.66089.560188.93497.280 2563582.41982.48072.429189.68871.44374.19876.24788.979 256 3676.23479.772155.76875.66972.27374.42972.19474.632 256 3782.256129.60274.55371.97574.097179.96599.61082.960 256 3870.14575.37868.27473.69668.18067.87068.55888.778 25639106.83878.90581.00667.23466.45666.47267.33561.509 256 40106.054140.411132.542130.542136.271132.607110.051110.196 25641330.682499.181375.038438.306328.312439.494259.706164.643 256 42141.116132.438127.142126.885120.667118.199141.387125.074 25643117.727117.264110.203109.133136.397124.773152.332108.032 25644134.342134.403133.234140.881147.804156.152139.552157.831 256 45104.982110.648128.998135.608108.966121.395177.990128.933 25646119.874113.904133.330121.894188.890127.232117.959144.403 256 47116.692144.695122.661116.157127.303120.325116.801135.152 25648114.173117.741129.831124.430118.317121.352131.057109.665 256 49114.926114.212115.208115.928128.289122.421110.368128.276 25650156.046167.588173.142153.574186.388160.818170.755152.284 25651166.841164.207167.165161.261164.911156.056176.995157.465 256 52177.216176.742173.549174.933189.339164.802165.471168.873 25653207.576200.987219.719188.459171.248198.044197.958175.104 256 54194.098251.389291.133193.348216.893189.772193.408177.940 25655182.231172.137171.837220.978190.193188.697210.295203.511 39 25656212.837157.267215.598182.321194.911169.995185.429189.570 25657159.824161.129162.742157.909163.794169.472156.279157.547 256 58165.779192.249168.444178.863215.303177.887172.085200.469 25659218.868192.453195.766200.082189.978196.691663.105202.177 Table I:Per-instance runtime of FourierSMT for the 3D place- ment benchmark.Eight GPUs use different seed numbers. All run- times are reported in seconds. The label “to” indicates that the solver exceeded the allotted time limit (1000 seconds) and did not return a solution. Instances01234567 22013.2739.9109.5567.9557.5239.0208.8137.594 2219.25112.52511.6327.6987.6088.7197.8707.994 2228.8308.5558.1968.3707.4479.8998.8808.172 2239.07010.1149.29811.9777.76910.3079.3308.419 22412.0979.7849.14612.2427.90911.54111.1878.727 22511.68413.60211.3298.2269.90210.3008.9768.887 2 2610.2879.2599.8938.3368.0079.8729.5288.433 22710.0978.68110.08411.4268.4629.5008.9618.343 22811.9649.88810.6688.1598.1449.4929.5838.066 22912.7418.66846.09010.3537.5689.1528.9287.931 24010.0507.4579.1568.0698.5459.1967.66610.159 24110.0008.0298.8787.82810.1749.2618.6279.368 24210.7678.0749.0198.8378.3729.5668.11410.530 2439.7788.67610.0368.5529.4089.3318.5069.648 2 449.8628.37210.1878.2668.3808.1158.5489.784 2 459.3538.56910.2308.2479.7889.3078.10810.253 2 4610.4607.8908.5288.2328.0129.3668.61910.124 2479.7308.36010.6548.18610.1159.8488.1278.613 24810.2898.30010.0858.2649.2349.9579.2669.299 24910.6719.1419.5147.8569.35110.2978.0699.190 28011.7948.7638.17310.5427.8539.15010.38910.852 28111.8028.6418.1729.8849.1929.4269.79210.664 2828.3839.6128.01610.0899.0108.5999.60011.457 28310.0119.2308.28410.4149.3349.5048.34811.319 2848.8457.5118.97010.4048.0219.1358.25410.619 28510.6958.3959.04410.6598.1599.2288.27010.790 2 8610.1378.5569.26310.4699.1209.1908.10610.169 2 8710.2189.6119.36010.9989.6769.19211.34612.178 2889.2069.1328.07311.12210.1159.6509.08112.371 2 899.9988.6658.18311.3528.4459.9349.60811.091 4209.75410.7488.92412.2599.89211.01710.53310.853 4218.59011.21011.77611.50114.90612.91610.49111.451 4228.9349.78810.42810.88010.64812.22111.53011.512 4239.0359.72211.05210.96010.68911.24210.60711.279 4 2411.5127.83311.74112.07810.28511.98810.72613.055 4259.95610.13211.03811.6609.82312.47611.46612.298 4269.0879.76910.66910.49411.84210.42310.76510.684 4 279.3567.98110.39813.40111.00310.41811.42113.035 4288.7229.06310.58910.49911.8889.74811.46110.467 42910.5568.80511.32913.56812.02111.79011.00611.971 4 4010.83310.67710.43211.5689.12511.31810.15210.927 44111.0149.59410.15911.48311.12711.10110.43911.870 4 4210.97211.38710.76410.63010.1729.56810.12010.879 44311.69810.27110.1939.8879.8708.76310.90111.238 44410.97610.3639.90112.02810.91810.7449.52511.361 4 4510.05110.23510.19711.08910.3578.1889.84310.537 44611.55110.8799.98911.21210.3688.74910.56011.984 44712.31810.35210.17912.19810.1629.4489.82911.359 44811.7899.80910.41010.97810.55310.86211.25111.218 44911.79610.85810.46911.05410.74711.02910.33611.137 48011.23110.47311.47012.41212.55513.19511.7719.842 40 48111.7569.25912.18512.87413.14612.13112.2919.666 48211.82810.22411.64114.41312.97812.27711.99311.031 4 8311.08911.61012.23513.35012.89712.40412.5678.523 48410.0029.23112.02912.68012.92610.74112.8818.910 48511.4869.89411.73413.20713.37012.23112.3459.533 48611.18910.36711.87214.95812.52012.08311.8289.120 48711.8799.43613.26612.61512.31711.87911.5679.998 48811.33910.27911.46311.79712.71712.70712.97210.831 4 8911.78610.35711.16013.70812.73111.51311.5299.474 82013.47214.25217.17815.59713.31017.75912.18512.494 82114.22617.06816.00114.31415.20013.7599.84216.108 82215.12415.32612.65813.87913.15114.40814.38713.729 82314.99016.10617.21016.02814.48214.36411.91413.831 82414.84217.12313.25614.78713.04314.27015.26411.869 82513.88016.37014.47912.47913.35411.67911.18212.824 8 2616.89717.16414.02016.19413.00812.69913.24013.756 82714.23618.07313.88314.65212.18011.61015.28814.410 82813.13514.43213.19716.38512.34815.98518.43811.411 82915.54214.69911.85113.14613.07617.05115.51511.309 84012.71412.12012.67611.91012.57612.92312.96111.438 84112.58613.36713.33713.25112.94012.71511.20710.657 84213.50513.51014.16713.26912.93512.62511.03512.393 8 4313.91511.22412.84313.87114.00013.34912.71311.964 84412.64313.26911.27412.00813.12713.31212.65812.629 84513.79113.25811.64214.00813.81511.69512.41812.016 84612.97612.15513.47412.56914.19614.16413.91213.145 84712.23112.05813.54915.74513.64413.21712.98812.765 84812.77311.32013.46813.92313.66413.61813.19912.695 84912.86513.03012.87813.28813.01511.70712.49712.635 88018.20612.86515.47214.39714.41013.69915.77913.850 88117.05512.79916.08414.90416.84713.77316.13111.767 88217.43713.09616.33713.49415.25814.37815.98713.570 8 8316.10313.61515.98414.50415.09813.10915.82713.518 8 8418.32313.31816.19714.09615.56514.63916.22214.100 8 8516.87612.61716.10614.74615.41713.65515.11913.889 88617.88413.30716.12414.66815.75613.68615.57812.917 88717.10514.78116.13014.69516.94513.87216.43014.579 88817.46113.51115.02514.17716.66212.80315.41814.215 88917.35113.55616.19213.85214.75313.76915.33414.347 162020.79018.22025.70120.09319.27923.50324.97822.885 162118.32522.19518.35718.11716.79317.26316.96824.416 162221.66319.93825.33222.10018.88920.44418.30519.699 162322.67225.48624.98421.36720.71917.71419.17620.723 162421.36021.91718.52221.76523.22321.65822.20222.354 16 2518.97623.49321.03218.83723.30518.44320.08218.260 16 2626.40921.55119.20322.08916.46622.41424.20019.170 16 2720.46119.20523.68321.62517.02622.26118.47517.196 162825.10521.43425.21119.12217.21119.66319.88017.607 16 2919.38519.87422.48320.14717.21221.82921.69921.956 164017.33516.84317.58316.13315.22815.42916.85814.235 16 4118.07516.04617.10516.32216.26714.40917.97015.761 164216.66416.89716.25816.27615.59315.48916.93616.863 164316.14816.46017.16815.66515.65716.63619.12615.127 16 4416.98216.99917.34316.73316.68816.03317.09316.083 164517.19016.50117.39716.16417.01616.43816.73515.930 16 4618.34516.19117.59417.79516.60215.39916.41816.121 164716.80415.76917.44317.51317.74715.51517.74816.875 16 4817.00916.07814.71317.33816.78015.64116.18616.319 164918.28115.92117.74616.99816.27716.53016.43416.082 168024.86122.21025.32922.58322.86025.30024.48423.472 16 8124.53222.53023.79923.74123.97924.49923.19924.406 168225.13822.60423.97223.67525.38824.56424.16123.670 16 8324.59622.25622.59623.06723.14924.83123.33123.051 168424.53822.56826.84123.57223.11523.83123.14523.528 41 168527.85623.77723.33124.21423.25224.68425.21523.860 168624.27922.22422.44022.72324.20922.63024.13424.090 16 8723.54122.56023.73022.87923.45523.23925.41422.428 168823.99023.17925.41624.27324.63424.82325.79424.819 168925.48922.70524.72725.00124.20124.00024.72325.933 322034.91030.42832.15232.05130.23132.30831.35827.536 322142.83331.73252.32531.17533.01432.98628.89724.072 322255.23231.46631.80226.48235.75831.95635.85532.459 32 2328.23233.61929.76728.49428.24028.53933.19330.332 322429.54333.65734.04432.27029.92632.51327.94729.714 322531.95731.02352.06931.79629.37533.77733.09330.690 322633.79025.00530.29648.98733.64733.74128.87029.078 322753.91228.85129.82333.42527.12133.69932.11227.528 322847.88533.67848.01634.02657.58124.44732.47427.007 322930.82132.18232.57150.68534.82431.39133.60858.438 32 4031.77728.59628.51628.87528.84328.72729.09929.834 324130.33028.06330.18728.71729.21829.86427.42628.624 324227.39530.14030.42528.72931.93330.39729.31731.100 324328.86827.06929.11131.69930.92728.17030.58427.615 324428.13827.54229.93728.91930.74327.60127.56828.672 324530.22128.24629.22530.07530.35829.68829.20428.171 324630.31929.34931.86629.95027.82428.92428.40730.130 32 4732.67528.85131.61328.12129.82528.73928.61928.011 324838.80727.45337.08128.70228.71431.95927.59829.326 324935.69828.98633.72733.75029.31028.01828.23527.811 328086.98361.93594.11775.05264.81267.95066.49565.538 328186.71867.62887.60691.26069.65877.63784.53678.231 328280.11680.35692.24583.72274.26692.56088.45994.920 328372.45497.54281.28491.35875.91094.54090.55093.097 328491.59993.68679.39970.82474.10594.02283.60593.608 328580.49691.30291.82779.64370.64579.90977.75884.928 328678.52681.69483.63573.61082.25884.74276.66989.289 32 8772.26582.55371.33676.01076.65186.81691.09687.175 32 8864.72783.04556.19266.68281.60380.66476.91882.503 32 8964.92380.48969.71766.72676.13867.62679.69875.116 6420266.963127.080168.539866.875128.940120.664121.389137.909 642170.629440.618360.92561.009260.635158.139173.286185.971 6422681.134118.974176.795605.324140.153151.334152.027239.754 6423103.458175.167235.277179.721175.210330.358113.082226.070 6424119.611292.611172.872135.217114.784182.442166.313118.346 6425184.32762.182165.352222.668127.980390.91153.421112.743 6426196.00066.95968.505149.85666.759110.046190.753167.332 642768.046177.111119.817406.39863.028232.73364.398169.949 6428228.988114.589121.839218.387116.397130.568112.37366.926 64 29425.988248.772129.427261.269238.90955.010109.281116.137 64 40106.73295.223105.29998.69183.330102.14285.87894.219 64 41108.505108.623101.53887.96088.047102.63486.77893.657 6442106.27292.516112.12697.97986.683112.25787.55692.539 64 43101.048101.632103.770101.34890.852102.84189.799101.906 644487.64298.95793.46580.69897.71997.97399.211101.439 64 4597.07491.78194.31388.76799.85694.97092.55296.602 644690.86893.793100.89296.94795.182101.527106.562100.122 644788.43094.190101.383101.473109.34194.855112.32795.200 64 4895.50792.62097.261100.27499.202102.549108.26595.527 6449105.889102.44699.68099.72795.710106.408102.54999.878 64 80289.754284.314304.717331.592327.080307.372315.660327.589 6481295.340281.258306.575301.947325.450332.469300.360301.247 64 82252.924285.944228.482290.230301.222269.578287.071318.004 6483292.645332.678281.728287.034313.736329.541328.671301.484 6484278.542273.656301.114303.729334.449280.329283.985328.285 64 85283.962331.013283.824290.712306.059311.748303.534292.165 6486287.729299.289289.911286.438311.286286.862285.105276.748 64 87292.593285.077305.776284.963329.314296.268328.489306.246 6488247.544285.126283.875292.930309.507280.890299.622280.604 42 6489269.551286.376245.185248.663298.424285.382298.903278.127 Table IV: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. InstancesFourierSMT Yices2SMTS MathSAT5Z3Z3PPSMT-RAT CVC5 100010.3200.6672.0561.20651.959127.3701.7742.860 100110.5200.6832.2601.19051.13198.3311.5542.693 100211.7200.6732.4021.20145.10460.2491.6082.737 100 313.6600.6632.3421.15541.76295.6941.6312.874 100414.2900.6982.3861.23258.01499.9421.5962.981 100514.5000.66919.9311.20046.70152.5441.5832.711 100614.8700.67713.0271.20168.633138.8831.5162.896 100714.9100.6423.2811.15142.80556.8221.5912.431 100814.9400.6672.1731.20350.816105.8961.6662.784 100914.9600.6512.5391.16645.264131.6871.6262.800 200 015.33012.04848.99319.439toto24.02248.571 200115.37012.07848.97119.267toto24.38849.811 200215.38012.00854.72719.361toto25.45050.707 200315.46012.00848.86819.301toto25.29347.859 200415.48012.17250.71919.180toto24.14648.347 200515.59012.02147.11719.376toto25.08745.112 200615.66011.99256.30919.141toto24.68048.549 200715.68012.05247.79619.352toto25.51150.345 200 815.89012.10744.31319.269818.373to24.92950.230 200 916.15012.37950.88319.303toto24.73750.114 300 016.16064.666267.43299.981toto149.874259.052 300116.19064.763296.301101.294toto151.812254.098 300216.22064.662306.71999.826toto151.029259.306 300316.24064.989320.685103.340toto149.994258.533 300416.32064.510314.240100.480toto152.409252.257 300516.32065.044305.877101.760toto150.918256.669 300616.48064.674311.96799.943toto149.744257.035 300716.51064.575311.69099.871toto151.735259.863 300816.55064.278308.43199.871toto147.721226.919 300916.85064.698289.83199.544toto151.231255.693 400 016.900218.945to329.279toto367.954820.927 400 117.060214.078996.427328.652toto409.900814.795 400217.310214.551to328.087toto367.802824.332 400 317.500214.109984.854325.206toto364.456822.964 400417.610213.321to327.078toto362.811818.409 400517.630213.839to331.589toto364.403836.187 400617.710212.857to325.873toto362.606819.349 400717.730213.435to326.335toto364.717835.281 400 817.870212.426to325.650toto361.630829.775 400917.950212.935985.271331.455toto384.311817.612 500017.980543.005to838.665toto770.167to 500 117.980541.506to828.176toto757.559to 500218.000553.905to834.533toto737.038to 500318.070543.653to829.635toto706.543to 500 418.120544.267to828.905toto738.708to 500518.230541.190to828.367toto738.962to 500 618.270541.699to829.384toto759.099to 500718.330542.968to840.175toto749.606to 500818.350543.276to835.088toto773.535to 500 918.470541.691to829.888toto745.924to 600018.590tototototototo 600118.620tototototototo 600218.640tototototototo 600318.700tototototototo 600418.700tototototototo 43 600518.770tototototototo 600618.830tototototototo 600 718.840tototototototo 600819.030tototototototo 600919.240tototototototo 700019.290tototototototo 700119.430tototototototo 700219.540tototototototo 700 319.570tototototototo 700419.640tototototototo 700519.670tototototototo 700619.810tototototototo 700719.830tototototototo 700819.980tototototototo 700920.190tototototototo 800 020.230tototototototo 800120.410tototototototo 800220.750tototototototo 800320.850tototototototo 800421.280tototototototo 800521.380tototototototo 800621.560tototototototo 800 721.580tototototototo 800821.680tototototototo 800921.700tototototototo 900021.740tototototototo 900121.820tototototototo 900221.970tototototototo 900322.230tototototototo 900422.350tototototototo 900522.750tototototototo 900622.910tototototototo 900 723.040tototototototo 900 823.240tototototototo 900 923.670tototototototo 1000023.860tototototototo 1000123.860tototototototo 1000223.870tototototototo 1000324.200tototototototo 1000424.640tototototototo 1000525.000tototototototo 1000625.780tototototototo 1000726.300tototototototo 1000828.680tototototototo 1000 937.840tototototototo Table V:Per-instance runtime for the continuous time schedul- ing 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. InstancesFourierSMT Yices2SMTS MathSAT5Z3Z3PPSMT-RAT CVC5 162027.0400.2301.1720.2990.8620.3319.9561.179 162116.9220.0620.1950.1630.0830.1639.9520.332 16 2212.8970.0300.3580.2520.0920.1547.2620.288 162312.3570.0440.2120.3240.0960.1595.5620.267 162411.1050.0320.1990.2610.0860.1456.6320.252 16 259.4730.0330.1940.3230.0860.1577.9030.266 16269.1930.0350.1900.2530.0790.1503.6070.288 16279.7490.0280.1820.1990.0780.1502.0400.209 162810.6710.0370.1800.3090.0830.1606.2660.340 16299.8510.0340.1870.2610.0930.1555.7750.258 163010.3490.1180.3241.2920.1560.36140.3091.089 44 163110.2380.1230.2760.8220.1730.32949.5130.775 163211.6270.1280.3380.8340.1800.325162.9220.922 16 339.7550.1150.1990.5970.1800.34522.8850.893 163411.7990.1140.2100.8070.1610.31760.2490.940 163518.7090.1570.3160.6760.1570.30334.0231.171 163611.6460.1140.2740.6140.1530.34685.4150.785 163710.2830.1250.2210.8020.1630.30953.7710.903 163812.2610.1630.4060.7970.2160.342184.3331.081 16 3910.9500.1400.2990.6780.2500.301107.4490.986 164010.8480.2080.2971.8110.3190.708236.6471.982 164126.6600.2470.5063.5220.5380.797636.7072.836 164211.6880.2890.5332.0130.3180.913to2.088 164311.9270.3490.5414.6110.3270.729to2.203 164410.9390.1700.3832.2900.3190.646324.8211.977 164511.2450.2890.5111.7220.2930.617351.5242.472 16 4620.4860.3870.5092.7310.4590.758to3.105 164711.1710.2210.5491.7820.4120.557470.7672.462 164826.7400.4830.6242.1920.3160.443506.9572.463 164912.1250.3590.5331.4760.3370.416518.5912.418 165012.2380.4780.7516.3280.5870.761to4.577 165111.7100.7890.6624.0120.7971.002to6.415 165212.3470.6100.7014.3980.5540.862to5.733 16 5312.5481.4780.6707.9160.7020.745to7.342 165412.7621.0360.7208.0670.6660.819to5.275 165563.8655.5060.97510.2562.2681.263to7.366 165612.1170.5400.7679.0260.6221.454to6.014 165712.0100.5430.6555.6710.7870.779to8.433 165823.5381.2890.7084.6410.7201.024to8.297 1659298.07545.3380.90917.7436.8932.204to6.887 322010.5410.2250.2972.1980.3810.536226.1521.968 322111.3430.3560.4271.4950.3340.691446.4552.844 322212.0310.2960.4581.8690.3590.699527.7952.861 32 2310.8860.3140.4663.8020.4000.578287.0402.722 32 2410.9430.3590.3492.3840.3650.556164.0713.310 32 2511.9640.2080.4802.1130.3580.579to3.180 322611.7790.2970.5063.1490.5710.660393.3263.882 322718.9590.3020.4832.7100.3860.703366.1212.951 322818.7030.2810.4562.2260.3660.621840.6973.385 322914.5830.3100.4451.9190.3190.407337.7982.887 323011.8351.7340.85523.4551.1001.629to16.291 323111.8561.2520.6878.1221.0111.506to16.124 323211.8352.4330.91810.5111.4732.357to13.910 323331.8181.3470.8608.0881.1081.807to14.332 323411.0741.0210.76411.3130.9511.578to8.211 32 3511.6580.7840.75412.6220.8701.883to13.741 32 3612.5611.2130.7638.4031.1151.305to12.722 32 3711.8721.1840.86710.7241.5892.144to16.586 323812.3001.1420.90910.0321.0061.758to9.707 32 3912.7581.0300.85013.5711.2113.401to15.931 324014.7822.8081.45232.4404.0877.874to36.276 32 4123.3003.5081.94828.9593.3535.354to55.646 324221.0433.6721.31518.7814.3086.253to39.611 324322.4354.0251.51124.5043.5014.608to58.803 32 4412.0145.4311.67827.8232.8119.385to77.434 324514.3472.8921.53531.3652.0473.177to49.941 32 4614.1754.1721.86533.3983.5484.469to53.574 324725.9255.7672.01748.4484.8285.118to51.069 32 4812.0114.1201.45935.9931.4425.693to42.363 324914.0114.1611.57535.2824.3106.212to45.499 325025.98613.9473.334110.1446.10413.729to117.503 32 5120.7649.3362.60863.7704.2448.820to158.131 325227.63924.3794.380321.9936.39119.946to167.740 32 5313.45325.7723.725104.5789.7087.789to129.521 325413.70719.5423.177308.9649.90915.601to127.565 45 325524.6768.3432.86281.4175.2199.815to114.127 325624.15219.7563.251272.3029.20810.591to104.664 32 5726.67227.0242.43474.30710.6709.452to109.409 325814.38177.4723.663350.93211.50315.308to169.241 325913.3257.0813.40777.9777.39817.317to148.968 642012.4743.1281.44627.5122.8884.589to43.508 642113.5442.6481.58729.8592.0944.722to49.726 642212.5833.6001.46931.3992.1964.997to39.326 64 2323.7593.0751.57428.2123.0304.471to36.486 642411.7183.1181.48440.3002.2102.873to86.908 642512.5092.5291.44349.3452.2453.074to39.101 642613.1212.8451.57633.5603.4132.975to44.290 642711.9703.0471.71431.6213.8886.653to51.427 642811.6823.4781.50544.8501.9013.457to45.369 642913.8223.3351.74929.4502.9193.084to41.745 64 3013.81516.1084.063146.74729.85614.692to224.028 643114.09820.5344.505293.3196.2977.573to212.775 643213.48515.5763.856183.1605.58717.535to306.306 643315.56521.6054.250217.0937.88216.597to181.239 643414.84423.4484.405225.2806.5299.740to249.158 643514.66729.0914.684207.8818.32712.844to364.327 643612.86617.8744.013267.5549.64710.302to314.181 64 3716.83919.0995.471246.81410.50912.319to392.739 643815.60922.7305.623183.8276.42522.011to327.328 643916.00620.8855.062154.65510.7519.073to366.237 644016.36988.45011.824839.809162.14842.087to826.405 644117.14262.74513.014to96.19434.222to763.588 644216.08478.79411.181525.42528.05135.795to618.071 644329.67055.3819.464to111.91430.951toto 644417.53274.8799.381531.11823.77130.858to922.959 644519.758587.88314.536to128.22940.888to821.720 644617.084134.38414.546to169.075101.591to643.976 64 4717.07262.43211.054to107.36452.151to834.580 64 4816.669129.38314.496to140.32430.992toto 64 4916.25163.54812.345to117.02032.773to737.374 645020.113to34.423to525.77948.919toto 645130.432158.51323.438to279.40954.905toto 645218.414343.73933.762to415.86651.988toto 645320.584148.07227.740to200.551395.898toto 645440.162153.32131.825to241.26471.977toto 645529.447332.85225.877to408.406329.576toto 645656.550to42.611to694.874509.194toto 645722.882140.64528.956to180.277371.783toto 645821.733to32.239to993.27941.324toto 64 5922.753to32.126to62.01145.145toto 128 2016.83365.63912.042854.79788.73124.302to724.482 128 2116.36774.27810.026591.88198.18525.512to538.788 1282216.34364.39310.604to103.85327.445to469.126 128 2319.17053.56710.177to37.00331.513to813.266 1282417.28490.82210.389to38.65432.262to662.087 128 2518.80886.97012.953609.96625.15031.401to578.507 1282616.38978.20011.339to88.00232.617to441.320 1282717.06069.7539.852813.15397.43430.212to592.031 128 2817.05180.9778.802to25.54587.076toto 1282917.58472.30510.466568.93185.57523.183to718.122 128 3022.476367.83533.598to357.972163.510toto 1283126.607358.55158.302toto467.951toto 128 3226.453381.84038.941to893.475445.183toto 1283324.202340.65243.340toto329.264toto 1283423.482257.36236.143to117.034324.488toto 128 3522.441272.18647.435to907.247122.779toto 1283621.986291.67633.592to761.162319.208toto 128 3722.040488.27037.073to890.721844.235toto 1283841.632927.92658.770to537.663146.421toto 46 1283923.062264.38139.865to106.86958.927toto 1284033.173to148.878tototototo 128 4136.343to135.016tototototo 1284232.718716.402124.973tototototo 1284333.889836.317125.073tototototo 1284431.581749.251122.616tototototo 1284535.321to123.238tototototo 1284631.899to109.968tototototo 128 4733.898to143.873tototototo 1284833.418968.79088.984tototototo 1284954.404883.718148.272tototototo 1285042.492to300.366tototototo 1285144.276to334.595tototototo 1285244.084to335.216tototototo 1285343.686to462.148tototototo 128 54278.661to390.678tototototo 1285548.521to278.542tototototo 1285646.908to586.455tototototo 1285746.240to444.569tototototo 1285846.608to342.575tototototo 1285948.802to341.136tototototo 2562035.693540.753111.198toto305.297toto 256 2137.218569.220100.476toto488.482toto 2562236.002616.599100.626to308.660989.786toto 2562342.959660.138100.475tototototo 2562437.165606.099112.441tototototo 2562537.356605.49097.369toto470.725toto 2562635.855595.612129.581toto911.357toto 2562737.773661.744122.221tototototo 2562835.492532.737109.400tototototo 2562943.965663.289108.188toto712.464toto 2563081.365to362.189tototototo 256 3179.657to466.286tototototo 256 3267.515to507.674tototototo 256 3363.216to395.136tototototo 2563491.920to502.177tototototo 2563579.333to467.360tototototo 2563675.150to522.162tototototo 2563782.608to442.585tototototo 2563869.352to426.302tototototo 2563967.284to422.094tototototo 25640131.542tototototototo 25641352.860tototototototo 25642127.013tototototototo 256 43117.495tototototototo 256 44140.216tototototototo 256 45125.164tototototototo 25646124.563tototototototo 256 47121.493tototototototo 25648119.834tototototototo 256 49115.568tototototototo 25650164.203tototototototo 25651164.559tototototototo 256 52174.241tototototototo 25653198.001tototototototo 256 54193.753tototototototo 25655189.445tototototototo 256 56187.500tototototototo 25657160.476tototototototo 25658178.375tototototototo 256 59198.387tototototototo 47 Table VI:Per-instance runtime for the 3D placement bench- mark.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. InstancesFourierSMT Yices2SMTS MathSAT5Z3Z3PPSMT-RAT CVC5 2208.3570.0050.1200.0200.0340.0500.2130.023 2218.4620.0050.1220.0210.0360.0510.2140.024 2228.4640.0060.1320.0210.0360.0520.2280.024 2238.5730.0060.1360.0210.0360.0520.3730.025 2 248.8510.0060.1360.0210.0360.0520.3730.025 2258.9080.0060.1380.0210.0360.0530.3790.025 2268.9160.0060.1380.0210.0370.0580.3820.026 2278.9280.0060.1400.0230.0380.0580.3870.029 2289.0400.0060.1460.0240.0380.0600.3880.030 2 299.0690.0080.1460.0350.0390.0610.4520.049 2409.1360.0090.1470.0470.0420.0625.2950.070 2419.1710.0090.1500.0470.0420.0626.0520.070 2429.2260.0100.1500.0490.0420.0637.0910.071 2439.2300.0100.1550.0500.0430.0637.5160.079 2449.2710.0100.1550.0500.0430.0649.5850.089 2459.2820.0100.1570.0510.0440.0669.6490.091 2 469.3050.0100.1570.0510.0440.0669.8540.094 2479.3140.0110.1600.0510.0440.06811.0320.104 2489.3300.0120.1600.0510.0450.06911.5490.105 2499.3690.0130.1610.0540.0460.07032.8210.110 2809.3930.0130.1630.0710.0460.072497.3210.229 2819.4190.0140.1660.0740.0470.078498.0620.267 2829.4280.0150.1670.0810.0470.080857.4660.269 2 839.5380.0160.1680.0840.0470.081to0.272 2 849.6090.0160.1690.0850.0480.082to0.274 2859.7700.0160.1690.0850.0480.086to0.278 2 869.7710.0160.1700.0850.0480.090to0.291 2879.9470.0160.1730.0900.0480.095to0.333 28810.1010.0170.1730.0900.0490.098to0.338 28910.2160.0170.1850.0930.0500.110to0.347 42010.2320.0380.1850.1750.0630.111to0.543 42110.2650.0390.1880.1860.0640.111to0.634 42210.4830.0410.1900.1860.0650.112to0.673 42310.4860.0450.1910.1920.0670.112to0.679 42410.5820.0460.1940.2040.0680.114to0.685 42510.6400.0490.2000.2060.0680.123to0.698 4 2610.6970.0490.2000.2400.0680.124to0.788 4 2710.7100.0500.2000.2490.0700.126to0.964 4 2810.7200.0570.2020.2520.0700.129to0.973 42910.7550.0580.2020.2650.0700.131to0.974 44010.7640.0580.2030.2800.0780.134to1.080 44110.8250.0590.2050.2880.0790.136to1.092 4 4210.8310.0600.2070.2950.0800.142to1.136 44310.9200.0640.2110.3060.0810.145to1.142 4 4410.9440.0710.2200.3110.0820.145to1.246 44511.0580.0800.2210.3170.0820.146to1.260 44611.2520.0900.2240.3410.0830.150to1.320 4 4711.3850.0930.2280.3430.0860.152to1.329 44811.4760.0940.2400.3440.0870.156to1.386 4 4911.5210.1100.2580.3660.1030.234to1.729 48011.5590.1210.2720.7120.1170.246to2.357 48111.6200.1300.2940.7220.1170.247to2.378 4 8211.6270.1330.3040.8600.1180.255to2.437 48311.6300.1380.3060.8600.1180.265to2.647 48411.8500.1380.3101.0400.1200.266to2.755 48511.8790.1450.3141.1360.1200.267to3.186 48611.9100.1530.3151.3170.1200.271to3.422 48711.9820.1540.3481.3670.1210.280to3.475 48 48812.1580.1600.3511.4590.1230.322to3.651 48912.3190.1710.3761.7090.1230.373to3.864 8 2012.6260.4830.6781.7750.1860.384to8.973 82112.6510.5010.6992.4510.1860.418to9.414 82212.8280.5450.7122.6370.1860.470to9.457 82312.8380.5640.7163.4330.1890.496to10.148 82412.8720.5920.7373.7260.1900.521to10.855 82513.0890.6080.7384.0900.1900.534to11.372 8 2613.0960.6120.7394.2970.1900.534to13.034 82713.1020.6170.7454.3780.1910.542to14.031 82813.1020.6720.7624.7230.1970.548to14.282 82913.3090.7080.7754.9460.1970.550to14.888 84013.3340.7220.7825.7440.2290.552to19.526 84113.8140.7310.8076.1600.2320.555to20.242 84213.8620.7530.8196.7180.2350.559to21.701 8 4313.8880.7750.8266.8250.2380.574to21.923 84413.9220.8300.8347.1610.2380.627to22.077 84514.1330.8660.8659.0540.2390.657to26.833 84614.3230.9030.89611.1500.2400.666to27.298 84714.4040.9150.93311.1730.2410.667to27.538 84814.5291.1040.97213.5240.2430.678to30.722 84914.5501.1160.98314.8450.2570.686to31.907 8 8014.6201.1340.99222.6880.3720.701to63.512 88114.7361.2461.03028.3550.3750.719to64.636 88214.7571.3541.10942.3440.3760.753to70.565 88314.8011.4301.20244.8100.3760.759to71.132 88414.8181.4371.22553.2470.3810.844to73.549 88514.9331.6211.31259.8970.3920.845to77.774 88615.1021.6521.33563.4280.4000.851to81.516 88715.1231.8691.34390.1240.4070.876to87.172 88815.4561.9251.387156.8480.4150.888to92.884 88915.4942.5181.420163.3630.4151.063to96.264 16 2016.2525.0024.874738.1480.8501.849to280.715 16 2116.2945.4105.394to0.8531.865to285.539 16 2216.3045.4356.297to0.8571.869to297.034 162316.4705.7226.349to0.8621.878to316.067 162416.4825.8417.448to0.8661.936to341.960 162516.4886.7357.851to0.8681.942to349.459 162616.5107.8987.893to0.8701.979to368.993 162716.6188.3197.976to0.8922.087to382.363 162816.8588.5688.031to0.9212.381to415.233 162917.15910.7698.272to0.9492.384to424.091 164018.22112.2448.435to1.4822.610to492.489 164119.52913.5108.515to1.4902.674to601.084 16 4219.77114.0988.542to1.5352.676to640.257 16 4319.83314.4108.965to1.5612.872to640.758 16 4420.19114.85610.740to1.5622.942to651.161 164520.92316.04010.916to1.6982.986to707.244 16 4621.04518.78011.552to1.7383.023to745.994 164721.82019.34011.669to1.7523.446to870.632 16 4821.83720.89612.465to1.8243.548to933.501 164921.84123.46413.683to1.9503.767toto 168023.10824.45517.134to2.9923.913toto 16 8123.34734.67017.767to3.0744.641toto 168223.40736.19218.943to3.1274.822toto 16 8323.55039.24319.255to3.2185.144toto 168423.88943.80120.517to3.3535.539toto 16 8523.97844.63322.418to4.1265.560toto 168624.03744.94122.475to4.3925.569toto 168724.06752.93525.362to5.3396.267toto 16 8824.72556.19726.090to10.18410.949toto 168924.72765.36626.307to11.15913.933toto 32 2028.405109.77189.343to12.78718.546toto 322128.795154.79496.938to12.90218.692toto 49 322228.859165.528101.115to13.06019.956toto 322328.968179.768116.255to13.59520.941toto 32 2428.989188.215118.699to13.62621.012toto 322529.020188.843119.695to14.30221.073toto 322629.148247.890120.004to14.41921.115toto 322729.153249.458120.484to14.57021.511toto 322829.456259.489121.021to14.86623.490toto 322929.649299.561133.291to14.93123.788toto 32 4030.268301.993138.032to15.13225.547toto 324130.968302.071139.322to16.71726.024toto 324231.098310.454146.172to16.75826.949toto 324331.705327.171157.097to17.74627.057toto 324431.877336.877157.264to17.78629.046toto 324531.971369.498166.412to18.60830.326toto 324632.208390.207178.427to19.64232.118toto 32 4732.359430.133182.445to19.65035.197toto 324833.090435.579224.071to22.81836.683toto 324933.852439.721226.689to23.94037.391toto 328067.222444.490292.867to24.49338.167toto 328172.416447.244316.561to24.78840.871toto 328278.791488.759356.595to25.45242.984toto 328379.602495.382381.526to27.17045.100toto 32 8480.203586.220425.064to30.82545.218toto 328581.383597.532433.010to31.02046.395toto 328681.976679.850443.741to34.38650.004toto 328786.090930.571489.981to37.31251.141toto 328887.602970.144492.600to37.75753.715toto 328990.954to524.383to38.02066.488toto 642094.642to757.721to162.246258.806toto 642195.259to877.139to165.145273.614toto 642296.957to984.668to167.819290.407toto 642397.597to988.336to169.436292.482toto 64 2497.846tototo170.077293.424toto 64 2598.231tototo170.333297.116toto 64 2698.291tototo172.951315.039toto 642798.535tototo172.968322.046toto 6428101.162tototo172.973323.287toto 6429101.490tototo184.401324.042toto 6440119.118tototo360.426551.277toto 6441129.951tototo375.781575.071toto 6442133.424tototo381.141576.374toto 6443144.883tototo390.029591.010toto 6444146.666tototo413.503592.750toto 6445150.765tototo445.167609.174toto 64 46164.411tototo475.534614.263toto 64 47177.466tototo483.366618.999toto 64 48179.629tototo518.660635.730toto 6449184.168tototo524.320653.587toto 64 80281.755tototototototo 6481284.500tototototototo 64 82286.508tototototototo 6483287.296tototototototo 6484292.549tototototototo 64 85297.850tototototototo 6486301.022tototototototo 64 87301.597tototototototo 6488307.610tototototototo 64 89311.516tototototototo 50 Figure 5.Detailed solver performance on benchmark categories. (a)Results on the scheduling problems.Z3++, CVC5,MathSAT5,SMT-RATwins non of the instances in this category.Yices2performs best on the small-scale instances (n w = 16), whileSMTSattains the best results on the medium-scale cases (n w ∈ 32,64). As the instance size increases further,FourierSMTcan handle cases that cause timeouts among competing solvers.(b)Results on the placement problems. SMTS,CVC5,MathSAT5,SMT-RATwins non of the instances in this category.Yices2still performs best on the small- scale instances (n m = 2), whileZ3andZ3++attains the best results on the medium-scale cases (n w ∈ 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.FourierSMTbenefits 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,FourierSMTremains scalable and continues to solve instances that all other solvers time out on. 51 Supplementary Note 11: Gradient Computation Time To quantify the acceleration attributable to GPU execution, we measure the gradient computation time ofFouri- erSMTwhen executed on either CPU or GPU. Our high-performance cluster node has dual AMD EPYC 9654 (with at most 384 threads), but configure the following flags:XLAFLAGS=--xlacpumultithreadeigen=false intraopparallelismthreads=64,OMPNUMTHREADS=64, andMKLNUMTHREADS=64to enforce thatFourierSMT uses at most 64 CPU threads. Similarly, the node contains 8 NVIDIA L40S GPUs, but we constrainFourierSMT to a single GPU by settingCUDAVISIBLEDEVICES=0. We measure the gradient computation time using the instances in the random hybrid constraint benchmark. For each instance, we evaluate the gradient at 10,000 distinct initial points. These points are partitioned into 100 groups, where each group of 100 points uses the same annealing parameter. We test 100 annealing parameters corresponding to 1/σ∈ 0.00,0.01,0.99. The results of this experiment are reported in Fig. 3b of the main text. In this section, we report the per-instance gradient computation time in Table VII. Table VII:Per-instance average gradient runtime of Fouri- erSMT for the random hybrid-constraint benchmark.All run- times are reported in milliseconds. The label “to” indicates that the solver exceeded the allotted time limit (1000 seconds) and did not re- turn a solution. InstancesCPUGPU 10004.84112.890 10014.99312.848 10024.97512.126 100 35.30012.370 10044.93012.902 100 54.88612.942 100 65.25112.888 10074.86112.973 10084.91112.756 10094.88412.323 200023.86913.734 200121.14713.594 200221.68713.708 200322.09213.645 200420.11913.596 200 520.23313.531 200622.75613.481 200 719.92513.689 200 824.23013.694 200921.73513.693 300035.27012.828 300134.59212.738 300233.98612.485 300334.08612.560 300 434.51712.774 300532.87712.885 300634.47212.621 300 733.74112.883 300833.28212.712 300 934.67613.236 400041.61112.906 400 141.82812.971 400242.04112.790 400343.20612.829 400 444.23112.649 400542.22812.518 400642.13112.778 400746.59212.903 400 842.83112.731 400944.68112.893 500 048.97212.831 500150.52812.483 52 500248.61912.816 500348.68212.483 500 447.27512.462 500547.32712.348 500647.23812.817 500747.02912.674 500851.21412.514 500947.07712.605 600 059.57012.863 600155.35012.784 600252.88212.745 600353.69112.688 600458.43212.558 600555.39112.882 600654.91712.973 600 755.20513.011 600858.44512.659 600958.83212.750 700059.73612.797 700165.50612.836 700266.11813.046 700360.35912.455 700 463.34912.727 700560.29112.665 700660.05012.934 700760.20312.671 700868.39112.668 700960.00012.822 800071.69112.832 800177.56912.737 800266.06412.634 800365.72812.997 800 465.24712.726 800 570.43612.787 800 671.17512.987 800767.00912.992 800867.24712.815 800968.65612.895 900077.77512.671 900180.03212.928 900275.77112.982 900382.11513.027 900477.76012.705 900576.14412.758 900 676.44512.863 900 775.27112.708 900 876.23213.017 900976.16413.072 1000 090.08112.284 1000183.09312.864 1000 284.63712.743 1000383.68012.876 1000482.62612.527 1000 582.26912.627 1000682.54912.778 1000 786.00812.697 1000882.36012.418 1000 986.24612.711