Paper deep dive
A general optimization solver based on OP-to-MaxSAT reduction
Yuxin Zhao, Han Huang, Zhifeng Hao
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 97%
Last extracted: 4/27/2026, 1:34:27 AM
Summary
The paper proposes GORED (General Optimization Solver based on OP-to-MaxSAT Reduction), an automated framework that enhances the generality of optimization solvers. It introduces an 'OP-to-MaxSAT' reduction method that converts diverse optimization problems (including integer, mixed-integer, linear, and nonlinear programming) into MaxSAT instances in polynomial time. The method uses a unified LaTeX-based modeling language, a signed binary fixed-point representation for numerical variables, and specific reduction rules for relational, arithmetic, and domain operations. Experimental validation on 136 instances across 11 problem types shows that GORED achieves solution quality comparable to specialized methods while providing significantly higher generality.
Entities (7)
Relation Signals (4)
OP-to-MaxSAT reduction → reduces → Optimization Problem
confidence 100% · reducing the problems from optimization problems to MaxSAT instances
OP-to-MaxSAT reduction → targets → MaxSAT
confidence 100% · reducing the problems from optimization problems to MaxSAT instances
GORED → uses → OP-to-MaxSAT reduction
confidence 100% · a general optimization solver based on OP-to-MaxSAT reduction (GORED).
Signed Binary Fixed-Point Representation → encodes → Optimization Problem Variables
confidence 90% · we use the signed binary fixed-point representation for encoding variables.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Optimization problems are fundamental in diverse fields, such as engineering, economics, and scientific computing. However, current algorithms are mostly designed for specific problem types and exhibit limited generality in solving multiple types of optimization problems. To enhance generality, we propose an automated reduction method named OP-to-MaxSAT reduction and a general optimization solver based on OP-to-MaxSAT reduction (GORED). GORED unifies the solving of multiple types of optimization problems by reducing the problems from optimization problems to MaxSAT instances in polynomial time and solving them using the state-of-the-art MaxSAT solver. The generality and solution quality of GORED are validated through experiments on 136 instances across 11 types of optimization problems. Experimental results demonstrate that GORED not only successfully solves a wide range of optimization problems but also yields solutions comparable in quality to those from existing methods, with no statistically significant differences observed. By introducing automated reduction, this work shifts the paradigm of optimization solvers from designing specialized algorithms for each problem type to employing a single algorithm for diverse problems. As a result, advances in this single algorithm can now drive progress in a wide range of optimization problems across various domains.
Tags
Links
- Source: https://arxiv.org/abs/2604.21961v1
- Canonical: https://arxiv.org/abs/2604.21961v1
Trouble viewing inline? Open PDF directly →
Full Text
136,607 characters extracted from source content.
Expand or collapse full text
[2] [1] of Software Engineering, China University of Technology, , 510006, 2] of Software Engineering, Yat-sen University, , 519082, 3] of Mathematics, College of Science, University, , 515063, A general optimization solver based on OP-to-MaxSAT reduction yuxinzhaozyx@163.com huangh985@mail.sysu.edu.cn haozhifeng@stu.edu.cn * [ [ Abstract Optimization problems are fundamental in diverse fields, such as engineering, economics, and scientific computing. However, current algorithms are mostly designed for specific problem types and exhibit limited generality in solving multiple types of optimization problems. To enhance generality, we propose an automated reduction method named OP-to-MaxSAT reduction and a general optimization solver based on OP-to-MaxSAT reduction (GORED). GORED unifies the solving of multiple types of optimization problems by reducing the problems from optimization problems to MaxSAT instances in polynomial time and solving them using the state-of-the-art MaxSAT solver. The generality and solution quality of GORED are validated through experiments on 136 instances across 11 types of optimization problems. Experimental results demonstrate that GORED not only successfully solves a wide range of optimization problems but also yields solutions comparable in quality to those from existing methods, with no statistically significant differences observed. By introducing automated reduction, this work shifts the paradigm of optimization solvers from designing specialized algorithms for each problem type to employing a single algorithm for diverse problems. As a result, advances in this single algorithm can now drive progress in a wide range of optimization problems across various domains. keywords: Optimization Problem, MaxSAT, Solver, Reduction, Generality 1 Introduction Optimization problems (OP) are prevalent in various fields, such as engineering design, resource allocation, machine learning, and transportation. The primary goal of optimization problems is to maximize or minimize a specific objective function under given constraints. As real-world problems become more and more diverse across various fields, the optimization problem needs to introduce various complex constraints for specific application scenarios. For example, in transportation, to meet the requirements of multi-level distribution, crowdshipping, and electric vehicle charging, vehicle routing problems (VRP) must consider not only traditional path optimization but also factors like multi-level vehicles[1, 2], multiple depots[3, 4], heterogeneous capacities[5, 6] and charging station locations[3, 7, 8]. In industrial production, job-shop scheduling problem (JSP) has evolved into multiple variants to handle requirements such as maintenance[9, 10], outsourcing[10], energy savings[11, 12], and dynamic jobs[9, 13, 14]. The increasing diversity of requirements significantly raises the complexity of optimization problems. If all types of optimization problems could be solved using a general method, it could not only reduce manual intervention on algorithm development but also promote knowledge integration across disciplines, accelerating the development and application of optimization technologies in various fields. Despite significant progress in solving optimization problems, existing research still shows clear limitations in terms of generality. The mainstream methods can be broadly categorized into two categories: mathematical programming methods and heuristic methods. Mathematical programming methods, such as linear programming[15, 16], integer programming[17, 18, 19], and quadratic programming[20, 21], offer notable advantages in theoretical rigor and solution quality. However, they rely heavily on strict mathematical structures, such as convex optimization or linear constraints. These methods struggle with non-standard constraints like nonlinear constraints. Non-standard optimization problems require manual transformation into equivalent standard forms before mathematical programming methods can solve them. Heuristic methods, such as genetic algorithms[22, 23, 24, 25, 26, 27], evolutionary algorithms[28, 29, 30, 31, 32], and particle swarm optimization[33, 34, 35, 36, 37], provide some flexibility. They allow designing operators for specific problems to adapt to the problem characteristics. However, this customization leads to high costs for algorithm transplantation and makes it challenging to create a general solver. Moreover, heuristic methods lack theoretical guarantees of optimality and are prone to getting stuck in local optima. Designing local search strategies for avoiding local optima further reduces their general applicability. Both methods depend heavily on manual intervention, such as problem transformation and algorithm design. This reliance makes it hard to achieve the universal solving of optimization problems and handle increasingly complex optimization problems. Therefore, developing a general optimization method that can adapt to various types of optimization problems while reducing manual intervention is an important research direction. To address the limitations of existing optimization methods in terms of generality, in this paper, we propose a general optimization solver based on OP-to-MaxSAT reduction (GORED). The core idea is to achieve universal optimization by automatically reducing any type of optimization problem to a MaxSAT instance and solving it using a MaxSAT solver. This optimization solver analyzes the constraint structure of problems and applies the proposed reduction rules to automate the reduction process, eliminating the need for manual intervention. We also demonstrate that the time complexity of this reduction process is polynomial, ensuring both efficiency and generality of the reduction. By introducing automated reduction, this work marks a shift from developing problem-specific algorithms to using a single algorithm for diverse optimization problems, enabling progress in one algorithm to generalize across many problem types. In summary, this paper provides the following contributions: 1) We propose an algorithm called OP-to-MaxSAT reduction, which automatically reduces multiple types of optimization problems to MaxSAT instances in polynomial time. Through rigorous theoretical analysis, we prove its time complexity. This reduction ensures the reliability and efficiency of the general optimization solver when handling various optimization problems. 2) We develop a general optimization solver based on the proposed OP-to-MaxSAT reduction. This solver achieves generality by automating the reduction and solving processes, enabling a single algorithm to solve multiple types of optimization problems, such as integer/mixed-integer programming, linear/nonlinear programming, combinatorial/numerical optimization, etc. This solver serves as a general tool for solving optimization problems across various fields. 3) To validate the cross-field applicability and practical effectiveness of the proposed general optimization solver, we conducted experiments on 11 types of optimization problems from various fields. These experiments cover several real-world applications, such as transportation and industrial production. The results show that the solver can effectively address optimization challenges across fields, highlighting its potential and value in practical applications. 2 OP-to-MaxSAT Reduction The Maximum Satisfiability problem (MaxSAT) is an extension of the Boolean Satisfiability problem (SAT). A MaxSAT instance is defined as maxcnf=(S,H)maxcnf=(S,H) over a set of Boolean variables X=x1,x2,⋯,xnX=\x_1,x_2,·s,x_n\, where S=(C1,w1),(C2,w2),⋯,(Cp,wp)S=\(C_1,w_1),(C_2,w_2),·s,(C_p,w_p)\ is a set of weighted soft clauses with wi≥0w_i≥ 0, and H=Cp+1,Cp+2,⋯,Cp+qH=\C_p+1,C_p+2,·s,C_p+q\ is a set of hard clauses. Each clause CiC_i is a disjunction of literals, where a literal is a Boolean variable xix_i or its negative ¬xi x_i. For example, C1=x1∨¬x2∨x5C_1=x_1 x_2 x_5. A clause is satisfied if at least one of its literals is true under a given variable assignment V:X→0,1V:X→\0,1\. A hard clause is a clause that must be satisfied. MaxSAT aims to find a solution (variable assignment) V that maximizes the total weight of satisfied soft clauses in S, while satisfying all hard clauses in H. This structure is highly similar to optimization problems, making MaxSAT an ideal target problem for reduction from optimization problems. Although many studies have attempted to manually reduce specific types of optimization problems to MaxSAT instances, these methods are limited to specific types of problems and lack generality[38, 39, 40]. Such manual reductions are not only time-consuming and labor-intensive, but also difficult to adapt to new types of optimization problems. To perform a manual reduction, one must first understand the characteristics of the specific problem before designing the corresponding reduction rules, which greatly limits the applicability and practicality of these methods. Therefore, developing an automated and general reduction method is the key to overcoming these limitations. To overcome the above limitations, we propose an automated reduction method called OP-to-MaxSAT reduction. This method consists of four steps: (1) unified modeling of optimization problems; (2) reducing variables in optimization problems to Boolean variables in MaxSAT; (3) reducing constraints to hard clauses; and (4) reducing the objective to soft clauses. This method not only improves the automation of reduction but also enhances its applicability across various optimization problems. In the following section, we will discuss the details of these steps. 2.1 Unified Modeling of Optimization Problems To reduce various types of optimization problems to MaxSAT problems, a unified modeling language is needed to describe these optimization problems. Since LaTeX is widely used in academic communication, we have designed the modeling language for optimization problems in LaTeX’s mathematical format. This format makes it easier to represent and visualize the mathematical models of optimization problems. Detailed grammar of this modeling language can be found in Appendix A. The proposed modeling language formulates the optimization problem in the form of Formulas 1-5. min/max / O O (1) s.t. s.t. C1B1 C_1 B_1 (2) C2B2 C_2 B_2 (3) ⋮ (4) CnBn C_n B_n (5) where the objective of the problem consists of the optimization direction min/max / and the objective function O. The objective function O is represented as a numerical expression. The i-th constraint of the problem consists of a constraint formula CiC_i and a universal quantifier BiB_i. The constraint formula CiC_i is a relational expression. The universal quantifier BiB_i is optional, which defines the scope of bound variables in the constraint formula CiC_i. In the following, we will use the Capacitated Vehicle Routing Problem (CVRP) as an example to illustrate the structure of optimization problems that the proposed modeling language can express in detail, as shown in Formulas 6-17. min ∑k=1m∑i=1n∑j=1ndi,jxi,j,k _k=1^m _i=1^n _j=1^nd_i,jx_i,j,k (6) s.t. s.t. xi,j,k∈0,1 x_i,j,k∈\0,1\ ∀k∈V,i,j∈P ∀ k∈ V,i,j∈ P (7) xi,i,k=0 x_i,i,k=0 ∀k∈V,i∈P ∀ k∈ V,i∈ P (8) ∑i=1nxi,j,k=∑i=1nxj,i,k _i=1^nx_i,j,k= _i=1^nx_j,i,k ∀j∈P,k∈V ∀ j∈ P,k∈ V (9) ∑k=1m∑i=1nxi,j,k=1 _k=1^m _i=1^nx_i,j,k=1 ∀j∈C ∀ j∈ C (10) ∑j=2nx1,j,k=1 _j=2^nx_1,j,k=1 ∀k∈V ∀ k∈ V (11) ∑i=1n∑j=2nqjxi,j,k≤Q _i=1^n _j=2^nq_jx_i,j,k≤ Q ∀k∈V ∀ k∈ V (12) uj−ui−qj+Q≥Qmaxk=1mxi,j,k u_j-u_i-q_j+Q≥ Q _k=1^m\x_i,j,k\ ∀i,j∈C,i≠j ∀ i,j∈ C,i≠ j (13) ui∈qi,…,Q u_i∈\q_i,…,Q\ ∀i∈C ∀ i∈ C (14) V=1,…,m V=\1,…,m\ (15) C=2,…,n C=\2,…,n\ (16) P=1∪C P=\1\∪ C (17) Formulas 6-17 present a mathematical model of CVRP using the proposed modeling language. m, n, di,jd_i,j, qjq_j and Q are the parameters of this problem. m is the number of vehicles, n is the number of positions, di,jd_i,j is the distance between position i and position j, qjq_j is the demand of customer j, and Q is the capacity of each vehicle. In a problem instance, these parameters are defined after Formulas 6-17 in the form of an assignment expression, such as m=5m=5, n=20n=20, d1,2=3d_1,2=3, etc. Formula 6 defines the objective of the problem, including the optimization direction (max or min) and the expression of the objective function. Formulas 7-17 are constraints of the problem. Each constraint consists of a constraint formula and a universal quantifier. A universal quantifier, such as i,j∈C,i≠ji,j∈ C,i≠ j in Formula 13, defines the scope of bound variables (such as i,ji,j) in the constraint formula. A constraint formula is a relational expression. It can be classified into equality constraints (e.g., Formulas 8-11), inequality constraints (e.g., Formulas 7, 12, 13), and domain constraints (e.g., Formulas 7, 14-17). A domain constraint specifies the type and domain of a variable. For example, ui∈qi,…,Qu_i∈\q_i,…,Q\ indicates that uiu_i is an integer variable ranging from qiq_i to Q, and x∈ℝx indicates that x is a real variable. The ability to specify integer and real variables means that the modeling language is able to express mixed integer programming problems. In this modeling language, each expression supports not only basic arithmetic operations but also nonlinear operations such as power, absolute values, minimum, and maximum (e.g., Formula 13). Therefore, this modeling language allows nonlinear constraints and objective, making it suitable for nonlinear optimization problems. The modeling language also supports set variables and set operations, as shown in Formulas 15-17. However, the purpose of supporting set variables is to simplify the problem description. Therefore, set variables cannot serve as decision variables in optimization problems. Instead, set variables can only be used as constant sets to represent finite integer or enumerated domains. OP-to-MaxSAT reduction includes an iterative simplification process for this modeling language, shown in Algorithm 1. This process aims to gradually eliminate all universal quantifiers and set variables, in order to simplify constraints and identify the set of decision variables. For example, from the constraint m=5m=5, we can derive V=1,…,5V=\1,…,5\, which allows Formula 11 to be split into five constraints without universal quantifiers. At the same time, abstract variables like x1,j,kx_1,j,k can be instantiated into specific variables with concrete indices, such as x1,2,1x_1,2,1. Constraints such as m=5m=5 and V=1,…,5V=\1,…,5\ are treated as assignment expressions. All the assignment expressions are removed from the mathematical model during simplification. When no more constraints can be simplified, the variables remaining in the mathematical model form the set of decision variables of the optimization problem. This simplification process not only checks the validity of the input mathematical model, but also provides a simpler representation of the problem for reduction to a MaxSAT instance. 2.2 Reduction of Variables To reduce optimization problems to MaxSAT instances, the numerical variables of optimization problems must be encoded into Boolean variables used in MaxSAT. In optimization problems, variables can be classified into integer and real variables, corresponding to integer programming and mixed-integer programming problems, respectively. To ensure the general applicability of variable encoding, we use the signed binary fixed-point representation for encoding variables. =am+n⏟sign bitam+n−1⋯am⏟integer bitsam−1⋯a0⏟fractional bits a= a_m+n_sign bit a_m+n-1·s a_m_integer bits a_m-1·s a_0_fractional bits (18) As shown in Formula 18, the variable a can be encoded to m+n+1m+n+1 Boolean variables, including 1 sign bit, n integer bits, and m fractional bits. The value it represents is v()=(−1)am+n∑−mn−12iai+mv( a)=(-1)^a_m+n _-m^n-12^ia_i+m. For integer variables, all fractional bits can be set to 0 to exactly represent integer values without loss of precision. For real number variables, although this encoding can only approximate real values, the precision can be flexibly controlled by adjusting the number of fractional bits m, to meet the requirements of specific problems. This encoding method not only accurately represents numerical variables but also facilitates the reduction of constraints and objective in later steps. 2.3 Reduction of Constraints Given a solution to an optimization problem, checking whether it satisfies all constraints is an NP problem. According to the theory of NP-completeness, any NP problem can be reduced to a SAT problem in polynomial time. Therefore, the constraints of an optimization problem can be reduced to a SAT instance, i.e., a conjunctive normal form (CNF). This CNF can be treated as hard clauses in the MaxSAT problem, ensuring that any feasible solution to the MaxSAT problem strictly satisfies all constraints of the original problem. If no MaxSAT solution satisfies these hard clauses, then the original optimization problem has no feasible solution. Figure 1: Operation tree of constraint ∑i=15xi=1 _i=1^5x_i=1 Table 1: Reduction Rules of Operations Category Operator Reduction Rule Relational == Equal(,)Equal( a, b) Operations ≠ NotEqual(,)NotEqual( a, b) ≤,≥≤,≥ LessEqual(,)LessEqual( a, b) <,><,> LessThan(,)LessThan( a, b) Arithmetic +,Σ+, Sum(1,2,⋯,k,)Sum(\ a_1, a_2,·s, a_k\, c) Operations ×,⋅,Π×,·, Product(1,2,⋯,k,)Product(\ a_1, a_2,·s, a_k\, c) kk a Scale(,k,)Scale( a,k, c) k,/ a^k,/ Power(,k,)Power( a,k, c) ‖\| a\| Absolute(,)Absolute( a, c) ⌊⌋ a Floor(,)Floor( a, c) ⌈⌉ a Ceil(,)Ceil( a, c) max Max(1,2,⋯,k,)Max(\ a_1, a_2,·s, a_k\, c) min Min(1,2,⋯,k,)Min(\ a_1, a_2,·s, a_k\, c) Domain ∈ IntegerDomain(,L,R)IntegerDomain( a,L,R) Definitions ∈ EnumerationDomain(,1,2,⋯,k)EnumerationDomain( a,\ b_1, b_2,·s, b_k\) L<≤RL< a≤ R RealDomain(,L1,R1,L2,R2)RealDomain( a,L_1,R_1,L_2,R_2) After the simplification process of the modeling language, each constraint in the mathematical model of the optimization problem is a relational expression. Each constraint can be represented as an operation tree, as shown in Figure 1. In the operation tree, each intermediate node represents an operation, and each leaf node represents a variable or a constant. Based on the properties of operations, these operations can be divided into three categories: relational operations, arithmetic operations, and domain definitions. For each category of operation, we have designed a corresponding reduction rule to reduce it to CNF. Table 1 summarizes the correspondence between operations and reduction rules. Detailed reduction rules are provided in Appendix C. By reducing all nodes in the operation tree to CNF according to their corresponding reduction rules, all constraints can be converted to CNF. The reduction rule for the relational operation opr aop_r b can be uniformly expressed as OPr(,)OP_r( a, b), where oprop_r is a relational operator, a and b are two operands of this operation. In the proposed modeling language, each relational operation corresponds to the relational expression in a constraint. Since all such expressions must be true, these reduction rules do not need to encode the result of relational operations. Instead, they only need to describe how these two operands make the relational operation true. For example, the CNF generated by Equal(,)Equal( a, b) is as Formulas 19-26. ¬am+n∨¬bm+n∨e a_m+n b_m+n e (19) am+n∨bm+n∨e a_m+n b_m+n e (20) am+n∨¬bm+n∨¬e a_m+n b_m+n e (21) ¬am+n∨bm+n∨¬e a_m+n b_m+n e (22) ¬e∨¬ai∨bi e a_i b_i i=0,…,m+n−1 i=0,…,m+n-1 (23) ¬e∨ai∨¬bi e a_i b_i i=0,…,m+n−1 i=0,…,m+n-1 (24) e∨¬ai e a_i i=0,…,m+n−1 i=0,…,m+n-1 (25) e∨¬bi e b_i i=0,…,m+n−1 i=0,…,m+n-1 (26) where aia_i and bib_i are the binary bits of the operands a and b under signed binary fixed-point encoding; these bits serve as the propositional variables of SAT problems. e is an additional intermediate variable introduced for representing this operation. The reduction rule for the arithmetic operation =opa(1,…,k) c=op_a( a_1,…, a_k) can be uniformly represented as OPa(1,⋯,k,)OP_a(\ a_1,·s, a_k\, c). Here, opaop_a denotes the function performing the arithmetic operation, 1 a_1 to k a_k are its k operands, and c is the output of the operation. The operands 1 a_1 to k a_k can be obtained from the children of the operation node, while the output c is an intermediate variable created specifically for this operation node. The purpose of such reduction rules is to describe the relationship between operands and output. The reduction rule for the domain definition ∈D a∈ D can be uniformly represented as OPd(,D)OP_d( a,D), where D is the domain of the operand a. We define IntegerDomainIntegerDomain and RealDomainRealDomain to describe continuous integer and real number domains, respectively. In addition, we define EnumerationDomainEnumerationDomain to describe sparse and non-continuous domains. 2.4 Reduction of the Objective In the proposed modeling language, the objective function is an arithmetic expression composed of arithmetic operations. Therefore, we first construct the operation tree of the objective function. Then, we encode all arithmetic operations in the objective function into hard clauses using the constraint reduction method described earlier. The output of the root node is taken as the variable representing the objective value, denoted by u. After these steps, the only remaining task is to encode the objective value u into soft clauses of MaxSAT. The goal of the optimization problem is to maximize or minimize the objective value, while the MaxSAT problem only supports maximization. To handle optimization problems that aim to minimize the objective value, we convert the minimization of the objective value into the maximization of its negation. For a signed binary fixed-point encoded objective value u, we only need to flip the sign bit to obtain the unified maximization objective value μ, as shown in Formula 27. =um+num+n−1⋯u0,maximize (¬um+n)um+n−1⋯u0,minimize μ= casesu_m+nu_m+n-1·s u_0,&maximize u\\ ( u_m+n)u_m+n-1·s u_0,&minimize u\\ cases (27) For a signed objective value μ, if treated as a signed integer, its range is [−2m+n+1,2m+n−1][-2^m+n+1,2^m+n-1]. If we can shift it to the range [1,2m+n−1][1,2^m+n-1], denoted by an unsigned integer μ, μ^0 μ_0 to μ^m+n μ_m+n can be used as soft clauses in the MaxSAT problem. The weight of each soft clause μ^i μ_i can be set to 2i2^i, so that the objective function of the MaxSAT problem becomes ∑i=0m+n2iμ^i _i=0^m+n2^i μ_i. This transformation realizes the reduction of the objective from the optimization problem to the MaxSAT problem. To convert the objective value μ into μ, a simple way is ^=+2m+n μ= μ+2^m+n. However, the value 2m+n2^m+n exceeds the range of an (m+n+1)(m+n+1)-bit signed number. To avoid overflow, we define the following reduction rule Normalization(,^)Normalization( μ, μ): Complement(,(¬μ^m+n)μ^m+n−1⋯μ^0) Complement( μ,( μ_m+n) μ_m+n-1·s μ_0) (28) where Complement(,)Complement( a, c) indicates that c is the two’s complement of a. See Appendix C for details. This reduction rule converts μ into μ by taking the two’s complement of μ and then flipping its sign bit. 2.5 Reduction Algorithm In summary, the reduction algorithm proposed in this paper includes the simplification process of the modeling language and the reduction processes of variables, constraints, and the objective, shown in Algorithms 1-2. Algorithm 1 OP-to-MaxSAT Reduction 1:M: optimization problem instance, 2:n: number of integer bits, 3:m: number of fractional bits 4:maxcnfmaxcnf: generated MaxSAT instance, 5:P: set of known quantities and their values, 6:Q: set of unknown quantities and their encodings 7:P=∅,Q=∅P= ,Q= 8:// simplify the mathematical model 9:while M exists assignment expression do // equations such as c=1c=1 10: extract an assignment expression “variable=valuevariable=value” from M 11: replace all “variablevariable” of M with “valuevalue” 12: perform algebraic simplification on M 13: add (variable,value)(variable,value) into P 14:end while 15:// reduction of constraints 16:for each constraint C in M do 17: represent the expression of C as an operation tree T 18: H=H= EncodeExpression(T, Q) 19: add H into maxcnfmaxcnf as hard clauses 20:end for 21:// reduction of the objective function 22:represent the expression of objective function in M as an operation tree T 23:H=H= EncodeExpression(T, Q) 24:add H into maxcnfmaxcnf as hard clauses 25:= u= the encoding of T’s root 26:if the optimization direction of M is minimizeminimize then 27: =(¬um+n)um+n−1⋯u0 μ=( u_m+n)u_m+n-1·s u_0 28:else 29: = μ= u 30:end if 31:create a new intermediate variable μ 32:add Normalization(,^)Normalization( μ, μ) into maxcnfmaxcnf as hard clauses 33:for i=0i=0 to m+nm+n do 34: add μ^i μ_i as soft clause and 2i2^i as its weight into maxcnfmaxcnf 35:end for 36:return maxcnfmaxcnf, P, Q Algorithm 2 Encoding of Expression 1: 2:T: the operation tree of expression, 3:Q: set of variables and their encodings 4:H: generated hard clauses 5:function EncodeExpression(T, Q) 6: H=∅H= 7: for each node e of T in post order do 8: if e is a variable then 9: if e is in Q then 10: the encoding of e = the encoding of e in Q 11: else 12: // reduction of variable 13: encode variable e as a signed binary fixed-point number c 14: the encoding of e = c 15: add (e, c) into Q 16: end if 17: else if e is a numeric constraint then 18: encode the output of e as a signed binary fixed-point number c 19: the encoding of e = c 20: else if e is a relational operation then 21: ,= a, b= the encodings of e’s two children 22: add OPr(,)OP_r( a, b) into H 23: else if e is an arithmetic operation then 24: encode the output of e as a signed binary fixed-point number c 25: the encoding of e = c 26: 1,⋯,k a_1,·s, a_k = the encodings of e’s children 27: add OPa(1,⋯,k,)OP_a(\ a_1,·s, a_k\, c) into H 28: else if e is a domain definition then 29: D=D= the domain specified in e 30: = a= the variable defined in e 31: add OPd(,D)OP_d( a,D) into H 32: end if 33: end for 34: return H 35:end function 3 Results The scientific viewpoint of this paper is that automated reduction is the key to enabling multiple types of optimization problems to be solved by a single algorithm. To validate this viewpoint, this paper proposes GORED, a general optimization solver enabled by the OP-to-MaxSAT reduction. Its architecture is shown in Figure 2. GORED reduces input optimization problems into MaxSAT instances, employs standard MaxSAT solvers to solve these MaxSAT instances, and finally maps the MaxSAT solutions back to the original problem space to obtain high-quality solutions for the original optimization problems. Without incorporating problem-specific solving logic, GORED enables unified modeling and solving of multiple types of optimization problems, shifting the paradigm of optimization solvers from designing specialized algorithms for each problem type to employing a single algorithm for a wide range of optimization problems. Figure 2: The Architecture of General Optimization Solver based on OP-to-MaxSAT Reduction 3.1 Generality To verify the generality of GORED, we conducted experiments on 11 optimization problems. The mathematical models of these problems, as represented by the proposed modeling language, are shown in Appendix B. These problems cover typical types of optimization problems, including integer programming, mixed-integer programming, linear programming, nonlinear programming, numerical optimization, combinatorial optimization, quadratic programming, convex optimization, and non-convex optimization. The application scenarios span multiple fields, such as transportation and industrial production. In Table 3, we compare the manual intervention required by GORED and mainstream optimization methods to adapt to these problems. The compared mainstream optimization methods include mathematical programming solvers like CPLEX, Gurobi, and SCIP, as well as heuristic methods like genetic algorithm(GA), evolutionary algorithm(EA), and particle swarm optimization(PSO). The experimental results show that mainstream optimization methods require manual intervention to adapt to specific optimization problems, while GORED can solve various types of problems without manual intervention. In Table 3, we compare the solving algorithms used by GORED and mainstream optimization methods for each problem. The table shows that mainstream methods employ different solving algorithms for different problems, whereas GORED can uniformly solve these problems using just a single algorithm. The results indicate that GORED has stronger generality in terms of manual intervention and solving algorithms. Table 2: Comparison in Generality: Manual Intervention00footnotetext: Legend: LP = linear programming, NLP = nonlinear programming, IP = integer programming, MIP = mixed-integer programming, NOP = numerical optimization problem, COP = combinatorial optimization problem, QP = quadratic programming, convex = convex optimization problem, non-convex = non-convex optimization problem, O = no manual intervention need, X = unable to adapt to this problem, R = reformulating problem, E = encoding decision variables, S = selecting proper operators, D = designing problem-specific operators. Optimization Problem Problem Characteristics Manual Intervention LP/NLP IP/MIP NOP/COP others GORED CPLEX Gurobi SCIP GA EA PSO Graph Coloring Problem[41] NLP IP COP - O O R R R+S E+R E+R Traveling Salesman Problem[42] LP IP COP - O O O O E+R+S E+R E+R Capacitated Vehicle Routing Problem[43] LP MIP COP - O O O R E+R+S E+R E+R Two-Echelon Vehicle Routing Problem[41] LP MIP COP - O O O O E+R+D E+R E+R Multidimensional Knapsack Problem[41] LP IP COP - O O O O S E E Job-Shop Scheduling Problem[44] LP MIP COP - O O O O E+R+D E+R E+R Open-Shop Scheduling Problem[44] LP MIP COP - O O O O E+R+D E+R E+R Quadratic Assignment Problem[45] NLP IP COP QP O O O O E+S E E Shifted Sphere Function[46] NLP MIP NOP QP + convex O O O O S O O Shifted Schwefel’s Problem[46] NLP MIP NOP QP + convex O O O O S O O Shifted Rosenbrock’s Function[46] NLP MIP NOP non-convex O X R R S O O Table 3: Comparison in Generality: Solving Algorithms00footnotetext: Legend: B&C = branch-and-cut, Ipopt = interior point optimizer, Simplex = simplex method, Barrier = barrier method, TPX = two-point crossover, OX = order crossover, SBX = simulated binary crossover, BM = bitflip mutation, IM = inversion mutation, PM = polynomial mutation, CX = custom problem-specific crossover, CM = custom problem-specific mutation, DE = differential evolution algorithm, Discretization = decoding continuous decision variables to discrete variables. Optimization Problem Solving Algorithms GORED CPLEX Gurobi SCIP GA EA PSO Graph Coloring Problem[41] MaxSAT Solver B&C B&C B&C GA+TPX+PM DE+Discretization PSO+Discretization Traveling Salesman Problem[42] MaxSAT Solver B&C B&C B&C GA+OX+IM DE+Discretization PSO+Discretization Capacitated Vehicle Routing Problem[43] MaxSAT Solver B&C B&C B&C GA+OX+IM DE+Discretization PSO+Discretization Two-Echelon Vehicle Routing Problem[41] MaxSAT Solver B&C B&C B&C GA+CX+CM DE+Discretization PSO+Discretization Multidimensional Knapsack Problem[41] MaxSAT Solver B&C B&C B&C GA+TPX+BM DE+Discretization PSO+Discretization Job-Shop Scheduling Problem[44] MaxSAT Solver B&C Simplex+B&C B&C GA+CX+CM DE+Discretization PSO+Discretization Open-Shop Scheduling Problem[44] MaxSAT Solver B&C B&C B&C GA+CX+CM DE+Discretization PSO+Discretization Quadratic Assignment Problem[45] MaxSAT Solver B&C B&C B&C GA+OX+IM DE+Discretization PSO+Discretization Shifted Sphere Function[46] MaxSAT Solver Barrier Barrier B&C GA+SBX+PM DE PSO Shifted Schwefel’s Problem[46] MaxSAT Solver Barrier Barrier B&C GA+SBX+PM DE PSO Shifted Rosenbrock’s Function[46] MaxSAT Solver - B&C B&C + Ipopt GA+SBX+PM DE PSO 3.2 Solution Quality To evaluate the performance of GORED in terms of solution quality, we conducted experiments on 136 test instances across 11 types of optimization problems described above. The results are summarized in Table 4, see Appendix D for details. The results indicate that GORED satisfies all constraints and achieves the optimal objective value in all problem instances, achieving solution quality comparable to current optimization methods. Its superiority mainly comes from the automated OP-to-MaxSAT reduction, i.e., automatically converting the original optimization problem into a MaxSAT instance and then solving it using a MaxSAT solver. This reduction makes the completeness of GORED depend on the completeness of the MaxSAT solver. When a complete MaxSAT solver is used, GORED is also complete, and the solution found is guaranteed to be the global optimum of the original optimization problem under finite precision. Table 4: Comparison in Solution Quality00footnotetext: Legend: The notation ”+/=/−+/=/-” indicates the number of instances in which GORED performs better than / equally to / worse than the existing methods in terms of the objective value of solution. Optimization Problem # Instances Comparison of GORED with Existing Methods (+/=/−+/=/-) CPLEX Gurobi SCIP GA EA PSO Graph Coloring Problem[41] 13 0/13/0 0/13/0 0/13/0 12/1/0 12/1/0 13/0/0 Traveling Salesman Problem[42] 11 0/11/0 0/11/0 0/11/0 11/0/0 11/0/0 11/0/0 Capacitated Vehicle Routing Problem[43] 8 0/8/0 0/8/0 0/8/0 2/6/0 7/1/0 8/0/0 Two-Echelon Vehicle Routing Problem[41] 20 0/20/0 0/20/0 0/20/0 19/1/0 0/20/0 16/4/0 Multidimensional Knapsack Problem[41] 20 0/20/0 0/20/0 0/20/0 2/18/0 1/19/0 18/2/0 Job-Shop Scheduling Problem[44] 10 0/10/0 0/10/0 0/10/0 10/0/0 10/0/0 10/0/0 Open-Shop Scheduling Problem[44] 20 0/20/0 0/20/0 0/20/0 10/10/0 10/10/0 20/0/0 Quadratic Assignment Problem[45] 8 0/8/0 0/8/0 0/8/0 1/7/0 0/8/0 1/7/0 Shifted Sphere Function[46] 10 0/10/0 0/10/0 0/10/0 0/10/0 0/10/0 1/9/0 Shifted Schwefel’s Problem[46] 6 0/6/0 0/6/0 0/6/0 5/1/0 4/2/0 2/4/0 Shifted Rosenbrock’s Function[46] 10 - 0/10/0 0/10/0 10/0/0 9/1/0 10/0/0 Total 136 0/126/0 0/136/0 0/136/0 82/54/0 64/72/0 110/26/0 3.3 Polynomial Time Complexity of Reduction To demonstrate the computational efficiency of the OP-to-MaxSAT reduction proposed in this paper, we analyze the time complexity of the entire reduction process. The total reduction time T(P)T(P) for an optimization problem P, with n integer bits and m fractional bits, can be expressed as: T(P)=Tm(P)+Tc(P)+Tt(P) T(P)=T_m(P)+T_c(P)+T_t(P) (29) where Tm(P)T_m(P) denotes the time spent on the mathematical model simplification, Tc(P)T_c(P) denotes the time for reducing constraints in problem P, and Tt(P)T_t(P) denotes the time for reducing the objective in problem P. To analyze how the size of problem P affects the reduction time, we use p, the number of operations, and q, the maximum number of operands among all operations, to represent the size of problem P. During the simplification of the mathematical model, the OP-to-MaxSAT reduction selects one assignment expression at a time for simplification, until no assignment expressions remain. To find an assignment expression, each constraint must be checked. Since the number of constraints is less than the number of operations, the time to find one assignment expression is O(p)O(p). There are O(p)O(p) assignment expressions in total. Each time an assignment expression is found, OP-to-MaxSAT reduction replaces variables and performs algebraic simplification of operations. These involve traversing O(pq)O(pq) operands and O(p)O(p) operations. Therefore, the total time spent on mathematical model simplification Tl(P)T_l(P) is in O(p3q)O(p^3q). In the proposed OP-to-MaxSAT reduction, reducing constraints means converting each operation into a conjunctive normal form (CNF) according to the corresponding reduction rule. Therefore, the reduction time for constraints can be expressed as the sum of the time required by each operation’s reduction rule. The time needed for each reduction rule depends on the size of the generated CNF, i.e., the number of literals and clauses, as shown in Table 5. The table shows that the maximum time complexity of a single reduction rule is O(qm2+qn2+qmn)O(qm^2+qn^2+qmn). Thus, the total reduction time for constraints Tc(P)T_c(P) is in O(pqm2+pqn2+pqmn)O(pqm^2+pqn^2+pqmn). Table 5: Generated CNF Size and Time Complexity of Reduction Rules Reduction Rule Size of The Generated CNF Time Complexity Upper Bound of #Literals Upper Bound of #Clauses Equal(,)Equal( a, b) O(1)O(1) O(m+n)O(m+n) O(m+n)O(m+n) NotEqual(,)NotEqual( a, b) O(m+n)O(m+n) O(m+n)O(m+n) O(m+n)O(m+n) LessEqual(,)LessEqual( a, b) O(m+n)O(m+n) O(m+n)O(m+n) O(m+n)O(m+n) LessThan(,)LessThan( a, b) O(m+n)O(m+n) O(m+n)O(m+n) O(m+n)O(m+n) Sum(1,2,⋯,k,)Sum(\ a_1, a_2,·s, a_k\, c) O(qm+qn)O(qm+qn) O(qm+qn)O(qm+qn) O(qm+qn)O(qm+qn) Product(1,2,⋯,k,)Product(\ a_1, a_2,·s, a_k\, c) O(qm2+qn2+qmn)O(qm^2+qn^2+qmn) O(qm2+qn2+qmn)O(qm^2+qn^2+qmn) O(qm2+qn2+qmn)O(qm^2+qn^2+qmn) Scale(,k,)Scale( a,k, c) O(m2+n2+mn)O(m^2+n^2+mn) O(m2+n2+mn)O(m^2+n^2+mn) O(m2+n2+mn)O(m^2+n^2+mn) Power(,k,)Power( a,k, c) O(m2+n2+mn)O(m^2+n^2+mn) O(m2+n2+mn)O(m^2+n^2+mn) O(m2+n2+mn)O(m^2+n^2+mn) Absolute(,)Absolute( a, c) O(1)O(1) O(m+n)O(m+n) O(m+n)O(m+n) Floor(,)Floor( a, c) O(n)O(n) O(m+n)O(m+n) O(m+n)O(m+n) Ceil(,)Ceil( a, c) O(n)O(n) O(m+n)O(m+n) O(m+n)O(m+n) Max(1,2,⋯,k,)Max(\ a_1, a_2,·s, a_k\, c) O(qm+qn)O(qm+qn) O(qm+qn)O(qm+qn) O(qm+qn)O(qm+qn) Min(1,2,⋯,k,)Min(\ a_1, a_2,·s, a_k\, c) O(qm+qn)O(qm+qn) O(qm+qn)O(qm+qn) O(qm+qn)O(qm+qn) IntegerDomin(,L,R)IntegerDomin( a,L,R) O(m+n)O(m+n) O(m+n)O(m+n) O(m+n)O(m+n) EnumerationDomain(,1,2,⋯,k)EnumerationDomain( a,\ b_1, b_2,·s, b_k\) O(qm+qn)O(qm+qn) O(qm+qn)O(qm+qn) O(qm+qn)O(qm+qn) RealDomin(,L1,R1,L2,R2)RealDomin( a,L_1,R_1,L_2,R_2) O(m+n)O(m+n) O(m+n)O(m+n) O(m+n)O(m+n) Normalization(,^)Normalization( μ, μ) O(m+n)O(m+n) O(m+n)O(m+n) O(m+n)O(m+n) The reduction of the objective mainly consists of two parts: encoding the arithmetic operations in the objective function and encoding the objective value. The encoding of the arithmetic operation is done in the same way as in the reduction of constraints, so the time spent in operation encoding is O(pqm2+pqn2+pqmn)O(pqm^2+pqn^2+pqmn). For encoding the objective value, we first apply the normalization rule Normalization(,^)Normalization( μ, μ), and then reduce it to m+n+1m+n+1 soft clauses. As shown in Table 5, the time complexity of normalization is O(m+n)O(m+n). Hence, the time complexity for encoding the objective value is also O(m+n)O(m+n). The total reduction time for objective Tt(P)T_t(P) is in O(pqm2+pqn2+pqmn)O(pqm^2+pqn^2+pqmn). In summary, the total time of OP-to-MaxSAT reduction T(P)T(P) is in O(p3q+pqm2+pqn2+pqmn)O(p^3q+pqm^2+pqn^2+pqmn). This indicates that OP-to-MaxSAT runs in polynomial time. Since most optimization problems are NP-hard, and no polynomial-time algorithms are currently known for NP-hard problems, the time cost of OP-to-MaxSAT reduction only accounts for a small portion of the overall solving time for the optimization problem. 4 Discussion The proposed GORED successfully addresses the challenge faced by traditional optimization methods in handling diverse and complex optimization problems with a single algorithm. By introducing an automated reduction method, GORED enables universal solving across various types of optimization problems, significantly reducing manual intervention. This breakthrough opens up new possibilities for cross-domain integration and application of optimization techniques. OP-to-MaxSAT reduction and GORED establish a new paradigm that solves multiple types of problems with a single algorithm, rather than designing specialized algorithms for each problem type, enabling advances in one algorithm to drive progress across a wide range of problems. To better understand the value and limitations of GORED, we will thoroughly discuss the shortcomings of existing optimization methods, analyze the advantages of GORED over them, and further discuss the limitations of GORED and potential directions for future improvement. 4.1 Comparison with Related Methods In contrast to existing methods, GORED introduces an automated reduction mechanism, allowing a single algorithm to solve diverse optimization problems while guaranteeing completeness. Mathematical programming methods, such as branch-and-cut[47, 48, 49], interior-point method[50, 51, 52], barrier method[53, 54, 55], and simplex method[56, 57], are classic techniques in the field of optimization. They are known for their theoretical rigor and high solution quality. These methods classify optimization problems into many types. For example, linear programming (LP) is widely used in planning and scheduling[15, 16]. Integer programming (IP) is used for combinatorial optimization[17, 18, 19]. Quadratic programming (QP) is suitable for problems with a quadratic objective function[20, 21]. Each mathematical programming method is designed for a specific type of problem, which makes these methods rely on certain mathematical structures like convexity or linearity. They exhibit limitations when dealing with complex nonlinear constraints or objectives. In such cases, manual intervention is needed to relax constraints, linearize, or reformulate models. The manual intervention limits their generality and automation. With the increasing demand for solving optimization problems in industry, many optimization solvers have been developed by integrating multiple mathematical programming methods. Examples include CPLEX[58], Gurobi[59], and SCIP[60]. These solvers offer unified modeling languages and support modeling and solving various optimization problems. Compared to a single mathematical programming method, they greatly extend the range of applicable problems. However, their ability to handle different problem types mainly depends on automatically selecting suitable mathematical programming methods according to the problem characteristics before solving the problems. In other words, their generality comes from integrating and packaging multiple algorithms, not from using a single algorithm to automatically solve multiple types of problems. Compared with these solvers, GORED does not rely on the mathematical structure of problems or the integration of mathematical programming methods. Instead, it solves multiple types of problems using a single algorithm through OP-to-MaxSAT reduction. Therefore, GORED offers higher generality. Heuristic methods are widely used in complex optimization problems due to their flexibility and adaptability. Typical approaches such as Genetic Algorithms (GA)[22, 23, 24, 25, 26, 27], Evolutionary Algorithms (EA)[28, 29, 30, 31, 32], Particle Swarm Optimization (PSO)[33, 34, 35, 36, 37], and Simulated Annealing (SA)[61, 62, 63] have demonstrated effectiveness in diverse applications, including job-shop scheduling and vehicle routing. Recently, reinforcement learning[64, 65, 66, 67, 68, 69], graph neural network[70, 71], and large language model[72] have also been introduced into optimization, showing potential for generalization across various problem types. However, these methods generally lack theoretical guarantees of optimality. They are prone to getting stuck in local optima. Moreover, the design of heuristic algorithms is highly dependent on the specific problem. This problem-specific algorithmic design makes it difficult to use the same algorithm for different problems without modification, limiting their generality. In addition, parameter tuning and operator design of heuristic methods require substantial expert knowledge, which further limits their generality. Compared with heuristic methods, GORED does not rely on problem-specific operators. It can be applied to various types of optimization problems without algorithmic adjustments, offering higher generality. Besides, the completeness of GORED comes from the MaxSAT solver used after reduction. When a complete MaxSAT solver is used to solve the reduced MaxSAT instance, GORED can guarantee the optimality of solutions. Reduction is not a new technique. Some studies have already attempted to reduce optimization problems to MaxSAT instances. These problems include the set cover problem[38], the dominating set problem[38], the group testing problem[39], and more recently, the quantum bit mapping and routing problems[40]. Reduction has shown good performance in solving these problems. However, these reduction methods are designed for specific problems. They lack an automated reduction mechanism and are therefore not general. Furthermore, the existing reduction methods mainly focus on combinatorial optimization problems. This makes the reduction process easier, as MaxSAT itself is also a combinatorial optimization problem. In contrast, reducing numerical optimization problems is more challenging. Research in this area is still limited. Compared to existing reduction methods, the proposed OP-to-MaxSAT reduction automates the reduction processes for various optimization problems. It requires no manual intervention for adapting to specific problems and works for both combinatorial and numerical optimization problems. 4.2 Error Analysis The proposed OP-to-MaxSAT reduction encodes variables as signed binary fixed-point numbers. This encoding requires that all values involved in the computation can be represented as signed binary fixed-point numbers with n integer bits and m fractional bits m. This requirement implies that OP-to-MaxSAT reduction can only guarantee the equivalence between the original and reduced problems under finite precision. Numerical errors occur when the values in the problem exceed the representable range. These errors are primarily caused by finite fractional bits. Any integer can be exactly represented by choosing a sufficiently large n. However, some decimal fractions, such as 0.1, cannot be exactly represented with finite binary bits. Since they have infinite binary expansions, they will always result in errors, no matter how large m is. Figure 3: Relationship between precision and error. To evaluate how precision affects numerical errors, we conducted experiments on 15 problem instances across three numerical optimization problems. The precision was defined as the number of fractional bits m. The error was measured as the Euclidean distance between the solution found by GORED and the theoretical optimal solution. As shown in Figure 3, the error decreases exponentially as the precision increases. All observed errors stayed within acceptable bounds. These findings demonstrate that despite precision limits, the proposed OP-to-MaxSAT reduction can maintain approximate equivalence between the original problem and the reduced problem under finite precision. 4.3 Limitations and Future Directions Our method demonstrates improved generality and automation compared to existing methods. However, this generality still has limitations. For example, GORED cannot be directly applied to multi-objective optimization problems or black-box optimization problems. In the case of multi-objective optimization, GORED can only produce a single solution, whereas such problems require a Pareto solution set. A simple method to address this issue is to run GORED multiple times, each time assigning a different set of weights to the objectives to convert the problem into a single-objective formulation. One Pareto-optimal solution can be obtained from each run, and these solutions can be collected to approximate a Pareto solution set. As for black-box optimization, since OP-to-MaxSAT reduction relies on white-box constraints and objectives, GORED is not applicable unless the optimization problem is converted into a white-box formulation. OP-to-MaxSAT reduction is the key to enabling the generality of GORED. However, the reduction may generate large MaxSAT instances, which may lead to a long solving time. Specifically, when handling complex constraints, the reduction introduces a large number of intermediate variables and hard clauses, which increases the workload of the MaxSAT solver. As a result, solving time grows significantly. This issue becomes especially serious for high-dimensional optimization problems. Consequently, GORED may not be suitable for applications with strict real-time requirements. Future research can address the above issue from two perspectives: the reduction and the MaxSAT solver. From the perspective of reduction, more compact reduction rules can be explored to reduce the number of intermediate variables and clauses. This improvement would decrease the size of generated MaxSAT instances and improve solving efficiency. In addition, during reduction, prior knowledge about the problem structure can be passed to the MaxSAT solver for preprocessing and pruning, which may enhance performance without sacrificing generality. From the perspective of the MaxSAT solver, as technology advances, MaxSAT solvers are becoming capable of handling larger instances. Future MaxSAT solvers are expected to handle even larger problems and provide faster MaxSAT solvers for GORED, enabling both generality and efficiency. This research direction holds both theoretical and practical significance, and deserves further exploration and attention. 5 Materials and Methods 5.1 Benchmark The problem instances used in this paper are from public benchmarks. Instances for the graph coloring problem, multi-dimensional knapsack problem, and two-echelon vehicle routing problem are obtained from OR-LIBRARY[41]. Traveling salesman problem instances were taken from TSPLIB[42]. Vehicle routing problem instances are from CVRPLIB[43]. Job-shop and open-shop scheduling problem instances are from Taillard[44]. Quadratic assignment problem instances are obtained from QAPLIB[45]. The Shifted Sphere Function, Shifted Schwefel’s Problem, and Shifted Rosenbrock’s Function are part of the benchmarks from the IEEE CEC 2005[46]. 5.2 Selection of MaxSAT Solver We tested all MaxSAT solvers from the weighted complete track of MaxSAT Evaluation 2024[73] on small instances of the test problems. Based on the results, the fastest solver, Pacose24[74], is selected as the MaxSAT solver used in GORED for all experiments in this paper. All experiments were conducted on a machine with an Intel(R) Core(TM) i9-10980XE CPU and 128GB of memory. 5.3 Parameter Settings For the experiments on solution quality, the parameter settings of GORED for each test problem are shown in Table 6. Note that the setting of these parameters only affects the size of the generated MaxSAT instances and the solving time of GORED, but has no impact on generality. We can also set the parameters to sufficiently large values (e.g., n=20n=20, m=20m=20) so that all problems are solved using the same parameter settings. Table 6: Parameter Settings of GORED on Test Problems Optimization Problem # integer bits n # fractional bits m Graph Coloring Problem 10 1 Traveling Salesman Problem 15 1 Capacitated Vehicle Routing Problem 15 1 Two-Echelon Vehicle Routing Problem 20 1 Multidimensional Knapsack Problem 15 5 Job-Shop Scheduling Problem 20 1 Open-Shop Scheduling Problem 20 1 Quadratic Assignment Problem 10 1 Shifted Sphere Function 20 20 Shifted Schwefel’s Problem 20 20 Shifted Rosenbrock’s Function 20 20 5.4 Data Availability All benchmark instances is available at https://github.com/YuxinZhaozyx/GORED. All other data are included in the manuscript and its appendices. 5.5 Code Availability The code of GORED is available at https://github.com/YuxinZhaozyx/GORED. 6 Acknowledgments This work is supported by National Natural Science Foundation of China (92570116, 62276103), Innovation Team Project of General Colleges and Universities in Guangdong Province (2023KCXTD002), the Research and Development Project on Key Technologies for Intelligent Sensing and Analysis of Urban Events Based on Low-Altitude Drones (2024BQ010011), Guangdong Basic and Applied Basic Research Foundation (2023B1515120020) and National Key R&D Program of China (2025YFC3410000). 7 Author Contributions Y.Z, H.H and Z.H designed research; Y.Z and H.H performed research; Y.Z wrote the paper with contributions from all co-authors. 8 Competing Interests The authors declare no competing interest. References [1] Huang, H., Yang, S., Li, X. & Hao, Z. An embedded hamiltonian graph-guided heuristic algorithm for two-echelon vehicle routing problem. IEEE Transactions on Cybernetics 52, 5695–5707 (2022). [2] Wang, H. et al. A hybrid fuzzy C-means heuristic approach for two-echelon vehicle routing with simultaneous pickup and delivery of multicommodity. IEEE Transactions on Fuzzy Systems 33, 218–230 (2025). [3] Zou, Y., Hao, J.-K. & Wu, Q. A two-individual evolutionary algorithm for cumulative capacitated vehicle routing with single and multiple depots. IEEE Transactions on Evolutionary Computation 29, 505–518 (2025). [4] Mehlawat, M. K., Gupta, P., Khaitan, A. & Pedrycz, W. A hybrid intelligent approach to integrated fuzzy multiple depot capacitated green vehicle routing problem with split delivery and vehicle selection. IEEE Transactions on Fuzzy Systems 28, 1155–1166 (2020). [5] Feng, L. et al. Solving generalized vehicle routing problem with occasional drivers via evolutionary multitasking. IEEE Transactions on Cybernetics 51, 3171–3184 (2021). [6] Bertsimas, D., Delarue, A. & Martin, S. Optimizing schools’ start time and bus routes. Proceedings of the National Academy of Sciences 116, 5943–5948 (2019). [7] Xing, Q., Xu, Y. & Chen, Z. A bilevel graph reinforcement learning method for electric vehicle fleet charging guidance. IEEE Transactions on Smart Grid 14, 3309–3312 (2023). [8] Yin, F. & Zhao, Y. Wasserstein distributionally robust equilibrium optimization under random fuzzy environment for the electric vehicle routing problem. IEEE Transactions on Fuzzy Systems 33, 1120–1132 (2025). [9] An, Y., Chen, X., Gao, K., Li, Y. & Zhang, L. Multiobjective flexible job-shop rescheduling with new job insertion and machine preventive maintenance. IEEE Transactions on Cybernetics 53, 3101–3113 (2023). [10] Su, J., Huang, H., Li, G., Li, X. & Hao, Z. Self-organizing neural scheduler for the flexible job shop problem with periodic maintenance and mandatory outsourcing constraints. IEEE Transactions on Cybernetics 53, 5533–5544 (2023). [11] Li, R., Gong, W., Wang, L., Lu, C. & Dong, C. Co-evolution with deep reinforcement learning for energy-aware distributed heterogeneous flexible job shop scheduling. IEEE Transactions on Systems, Man, and Cybernetics: Systems 54, 201–211 (2024). [12] Pan, Z., Lei, D. & Wang, L. A Bi-population evolutionary algorithm with feedback for energy-efficient fuzzy flexible job shop scheduling. IEEE Transactions on Systems, Man, and Cybernetics: Systems 52, 5295–5307 (2022). [13] Liu, C.-L., Tseng, C.-J. & Weng, P.-H. Dynamic job-shop scheduling via graph attention networks and deep reinforcement learning. IEEE Transactions on Industrial Informatics 20, 8662–8672 (2024). [14] Lei, K. et al. Large-Scale Dynamic Scheduling for Flexible Job-Shop With Random Arrivals of New Jobs by Hierarchical Reinforcement Learning. IEEE Transactions on Industrial Informatics 20, 1007–1018 (2024). [15] Kuang, Y. et al. Accelerate presolve in large-scale linear programming via reinforcement learning. IEEE Transactions on Pattern Analysis and Machine Intelligence 47, 6660–6672 (2025). [16] Mo, P. et al. Energy-efficient train scheduling and rolling stock circulation planning in a metro line: A linear programming approach. IEEE Transactions on Intelligent Transportation Systems 21, 3621–3633 (2020). [17] Wang, R., Zhang, C., Pu, S., Gao, J. & Wen, Z. A customized augmented lagrangian method for block-structured integer programming. IEEE Transactions on Pattern Analysis and Machine Intelligence 46, 9439–9455 (2024). [18] Dash, S., Sodhi, R. & Sodhi, B. An appliance load disaggregation scheme using automatic state detection enabled enhanced integer programming. IEEE Transactions on Industrial Informatics 17, 1176–1185 (2021). [19] Shen, Z.-S. et al. Free-energy machine for combinatorial optimization. Nature Computational Science 5, 322–332 (2025). [20] Lam, B. S. Y. & Liew, A. W.-C. A fast binary quadratic programming solver based on stochastic neighborhood search. IEEE Transactions on Pattern Analysis and Machine Intelligence 44, 32–49 (2022). [21] Shir, O. M. & Emmerich, M. Multiobjective mixed-integer quadratic models: A study on mathematical programming and evolutionary computation. IEEE Transactions on Evolutionary Computation 29, 661–675 (2025). [22] Duan, J., He, Z. & Yen, G. G. Robust multiobjective optimization for vehicle routing problem with time windows. IEEE Transactions on Cybernetics 52, 8300–8314 (2022). [23] Awad, A., Hawash, A. & Abdalhaq, B. A genetic algorithm (GA) and swarm-based binary decision diagram (BDD) reordering optimizer reinforced with recent operators. IEEE Transactions on Evolutionary Computation 27, 535–549 (2023). [24] Li, J., Liu, R. & Wang, R. Elastic strategy-based adaptive genetic algorithm for solving dynamic vehicle routing problem with time windows. IEEE Transactions on Intelligent Transportation Systems 24, 13930–13947 (2023). [25] Krol, A. & Sierpinski, G. Application of a genetic algorithm with a fuzzy objective function for optimized siting of electric vehicle charging devices in urban road networks. IEEE Transactions on Intelligent Transportation Systems 23, 8680–8691 (2022). [26] Liu, S.-C. et al. Many-objective job-shop scheduling: A multiple populations for multiple objectives-based genetic algorithm approach. IEEE Transactions on Cybernetics 53, 1460–1474 (2023). [27] He, L. et al. Multiobjective optimization of energy-efficient JOB-shop scheduling with dynamic reference point-based fuzzy relative entropy. IEEE Transactions on Industrial Informatics 18, 600–610 (2022). [28] Li, B., Zhang, Y., Yang, P., Yao, X. & Zhou, A. A two-population algorithm for large-scale multiobjective optimization based on fitness-aware operator and adaptive environmental selection. IEEE Transactions on Evolutionary Computation 29, 631–645 (2025). [29] Huang, H., Xu, Y., Xiang, Y. & Hao, Z. Correlation-based dynamic allocation scheme of fitness evaluations for constrained evolutionary optimization. IEEE Transactions on Evolutionary Computation 28, 1250–1264 (2024). [30] Yang, S., Huang, H., Luo, F., Xu, Y. & Hao, Z. Local-diversity evaluation assignment strategy for decomposition-based multiobjective evolutionary algorithm. IEEE Transactions on Systems, Man, and Cybernetics: Systems 53, 1697–1709 (2023). [31] Han, K., Christie, L. A., Zăvoianu, A.-C. & McCall, J. A. W. Exploring representations for optimizing connected autonomous vehicle routes in multi-modal transport networks using evolutionary algorithms. IEEE Transactions on Intelligent Transportation Systems 25, 10790–10801 (2024). [32] Gao, D., Wang, G.-G. & Pedrycz, W. Solving fuzzy job-shop scheduling problem using DE algorithm improved by a selection mechanism. IEEE Transactions on Fuzzy Systems 28, 3265–3275 (2020). [33] Dziwinski, P. & Bartczuk, L. A new hybrid particle swarm optimization and genetic algorithm method controlled by fuzzy logic. IEEE Transactions on Fuzzy Systems 28, 1140–1154 (2020). [34] Dai, S.-H., Jia, Y.-H., Chen, W.-N., Mei, Y. & Yang, Q. Multistage particle swarm optimization for heterogeneous multipoint dynamic aggregation. IEEE Transactions on Systems, Man, and Cybernetics: Systems 55, 4614–4628 (2025). [35] Han, H.-G., Xu, Z.-A. & Wang, J.-J. A novel set-based discrete particle swarm optimization for wastewater treatment process effluent scheduling. IEEE Transactions on Cybernetics 54, 5394–5406 (2024). [36] Zouari, M. et al. PSO-based adaptive hierarchical interval type-2 fuzzy knowledge representation system (PSO-AHIT2FKRS) for travel route guidance. IEEE Transactions on Intelligent Transportation Systems 23, 804–818 (2022). [37] Zhang, L., Oh, S.-K., Pedrycz, W., Yang, B. & Wang, L. A promotive particle swarm optimizer with double hierarchical structures. IEEE Transactions on Cybernetics 52, 13308–13322 (2022). [38] Lei, Z. & Cai, S. Solving set cover and dominating set via maximum satisfiability. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 34, 1569–1576 (2020). [39] Ciampiconi, L., Ghosh, B., Scarlett, J. & Meel, K. S. A MaxSAT-based framework for group testing. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 34, 10144–10152 (2020). [40] Molavi, A. et al. Qubit mapping and routing via MaxSAT. In 2022 55th IEEE/ACM International Symposium on Microarchitecture (MICRO), 1078–1091 (2022). [41] Beasley, J. E. Or-library: Distributing test problems by electronic mail. Journal of the Operational Research Society 41, 1069–1072 (1990). [42] Reinelt, G. Tsplib—a traveling salesman problem library. ORSA Journal on Computing 3, 376–384 (1991). [43] Uchoa, E. et al. New benchmark instances for the capacitated vehicle routing problem. European Journal of Operational Research 257, 845–858 (2017). [44] Taillard, E. Benchmarks for basic scheduling problems. European Journal of Operational Research 64, 278–285 (1993). [45] Burkard, R., Karisch, S. & Rendl, F. Qaplib-a quadratic assignment problem library. European Journal of Operational Research 55, 115–119 (1991). [46] Suganthan, P. et al. Problem definitions and evaluation criteria for the cec 2005 special session on real-parameter optimization. Natural Computing 341-357 (2005). [47] Kazachkov, A. M., Le Bodic, P. & Sankaranarayanan, S. An abstract model for branch and cut. Mathematical Programming 206, 175–202 (2024). [48] Galias, Z. Deterministic branch and cut algorithm for multiobjective optimization of protective device allocation in radial distribution systems. IEEE Transactions on Industrial Informatics 21, 2344–2353 (2025). [49] Castellucci, P. B., Coelho, L. C. & Darvish, M. A new branch-and-benders-cut algorithm for the time-dependent vehicle routing problem. Expert Systems with Applications 265, 125996 (2025). [50] Zhang, Z., Zhao, Q. & Dai, F.-A. A warm-start strategy in interior point methods for shrinking horizon model predictive control with variable discretization step. IEEE Transactions on Automatic Control 68, 3830–3837 (2023). [51] Lu, W., Liu, M., Lin, S. & Li, L. Fully decentralized optimal power flow of multi-area interconnected power systems based on distributed interior point method. IEEE Transactions on Power Systems 33, 901–910 (2018). [52] Huang, M. & Chen, J. Proactive mobility load balancing through interior-point policy optimization for open radio access networks. IEEE Transactions on Mobile Computing 24, 500–506 (2025). [53] Dvurechensky, P. & Staudigl, M. Hessian barrier algorithms for non-convex conic optimization. Mathematical Programming 209, 171–229 (2025). [54] Dzahini, K. J., Kokkolaras, M. & Le Digabel, S. Constrained stochastic blackbox optimization using a progressive barrier and probabilistic estimates. Mathematical Programming 198, 675–732 (2023). [55] Zhao, R. & Freund, R. M. Analysis of the frank–wolfe method for convex composite optimization involving a logarithmically-homogeneous barrier. Mathematical Programming 199, 123–163 (2023). [56] Blank, J., Deb, K., Dhebar, Y., Bandaru, S. & Seada, H. Generating well-spaced points on a unit simplex for evolutionary many-objective optimization. IEEE Transactions on Evolutionary Computation 25, 48–60 (2021). [57] Xu, J. et al. Scaled simplex representation for subspace clustering. IEEE Transactions on Cybernetics 51, 1493–1505 (2021). [58] IBM. IBM ILOG CPLEX Optimization Studio 22 (2024). https://w.ibm.com/products/ilog-cplex-optimization-studio. Accessed 15 July 2025. [59] Gurobi Optimization. Gurobi 12.0 (2025). https://docs.gurobi.com/12.0/. Accessed 15 July 2025. [60] Suresh Bolusani et al. The SCIP optimization suite 9.0 (2024). https://optimization-online.org/?p=25734. Accessed 15 July 2025. [61] Davari, S. A., Nekoukar, V., Garcia, C. & Rodriguez, J. Online weighting factor optimization by simplified simulated annealing for finite set predictive control. IEEE Transactions on Industrial Informatics 17, 31–40 (2021). [62] Onizawa, N., Katsuki, K., Shin, D., Gross, W. J. & Hanyu, T. Fast-converging simulated annealing for ising models based on integral stochastic computing. IEEE Transactions on Neural Networks and Learning Systems 34, 10999–11005 (2023). [63] Han, C., Gu, Y., Wu, G. & Wang, X. Simulated annealing-based heuristic for multiple agile satellites scheduling under cloud coverage uncertainty. IEEE Transactions on Systems, Man, and Cybernetics: Systems 53, 2863–2874 (2023). [64] Ming, F., Gong, W., Wang, L. & Jin, Y. Constrained multi-objective optimization with deep reinforcement learning assisted operator selection. IEEE/CAA Journal of Automatica Sinica 11, 919–931 (2024). [65] Peng, C. et al. Learning-based temporal sequence of constrained handling selection for constrained multi-objective evolutionary optimization. IEEE Transactions on Evolutionary Computation (2025). DOI:10.1109/tevc.2025.3584207. [66] Yuan, Z., Li, G., Wang, Z., Sun, J. & Cheng, R. RL-CSL: A combinatorial optimization method using reinforcement learning and contrastive self-supervised learning. IEEE Transactions on Emerging Topics in Computational Intelligence 7, 1010–1024 (2023). [67] Zhang, Z., Wu, Z., Zhang, H. & Wang, J. Meta-learning-based deep reinforcement learning for multiobjective optimization problems. IEEE Transactions on Neural Networks and Learning Systems 34, 7978–7991 (2023). [68] Ghafarollahi, A. & Buehler, M. J. Modeling protein motions through reinforcement learning. Proceedings of the National Academy of Sciences 121, e2422180121 (2024). [69] Barreto, A., Hou, S., Borsa, D., Silver, D. & Precup, D. Fast reinforcement learning with generalized policy updates. Proceedings of the National Academy of Sciences 117, 30079–30087 (2020). [70] Heydaribeni, N., Zhan, X., Zhang, R., Eliassi-Rad, T. & Koushanfar, F. Distributed constrained combinatorial optimization leveraging hypergraph neural networks. Nature Machine Intelligence 6, 664–672 (2024). [71] Schuetz, M. J. A., Brubaker, J. K. & Katzgraber, H. G. Combinatorial optimization with physics-inspired graph neural networks. Nature Machine Intelligence 4, 367 (2022). [72] Akiba, T., Shing, M., Tang, Y., Sun, Q. & Ha, D. Evolutionary optimization of model merging recipes. Nature Machine Intelligence 7, 195–204 (2025). [73] MaxSAT evaluation 2024 : Solver and benchmark descriptions (2024). http://hdl.handle.net/10138/584878. Accessed 15 July 2025. [74] Berg, J. et al. Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024), Vol. 307, 4:1–4:28 (2024). [75] Zhou, N.-F. & Kjellerstrand, H. Optimizing SAT encodings for arithmetic constraints. In Principles and Practice of Constraint Programming, Vol. 10416, 671–686 (2017). Appendix A Grammar of Unified Modeling Language The grammar of the proposed modeling language is described below using Extended Backus-Naur Form (ISO/IEC 14977). ⬇ 1model = ’ align’, (objective|constraint), ’\\’, (objective|constraint), [’\\’], ’ align’; 2 3objective = (’ ’ | ’ ’), [’&&’], numeric_expression, [’&&’ | ’&&’, conditions]; 4constraint = [’s.t.’], [’&&’], relation_expression, [’&&’ | ’&&’, conditions]; 5 6conditions = condition, ’,’, condition; 7condition = variable, ’,’, variable, ’=’, numeric_expression, ’,’, (’...’ | ’…’ | ’·s’), ’,’, numeric_expression 8 | [’∀’], variable, ’,’, variable, ’∈’, set_expression 9 | [’∀’], variable, ’,’, variable, (’⊂’|’ ’|’ ’), set_expression 10 | numeric_expression, (’≤’ | ’<’), variable, (’≤’ | ’<’), variable, (’≤’ | ’<’), numeric_expression 11 | relation_expression; 12 13relation_expression = variable, ’=’, variable, ’=’, variable 14 | variable, ’≠’, variable 15 | numeric_expression, ’=’, numeric_expression, ’=’, numeric_expression 16 | numeric_expression, ’≠’, numeric_expression 17 | numeric_expression,(’≤’|’<’),numeric_expression,(’≤’|’<’),numeric_expression 18 | numeric_expression,(’≥’|’>’),numeric_expression,(’≥’|’>’),numeric_expression 19 | set_expression, ’=’, set_expression, ’=’, set_expression 20 | set_expression, ’≠’, set_expression 21 | set_expression, (’⊂’ | ’ ’ | ’ ’), set_expression 22 | numeric_expression, (’∈’ | ’∉’ | ’ ∈’), set_expression; 23 24numeric_expression = [’-’], numeric_1st_term, (’+’ | ’-’), numeric_1st_term; 25 26numeric_1st_term = numeric_2nd_term [’·’ | ’×’ | ’/’], numeric_2nd_term; 27 28numeric_2nd_term = numeric_3rd_term 29 | ’ ’, ’, numeric_expression, ’, (’, numeric_expression, ’ | one_token) 30 | numeric_3rd_term, ’^’, (’, numeric_expression, ’ | one_token) 31 | (’Σ’ | ’Π’), ’_’, ’, variable, ’=’, numeric_expression, [’,’, conditions], ’, ’^’, (’, numeric_expression, ’ | one_token) numeric_1st_term 32 | (’Σ’ | ’Π’), ’_’, ’, conditions, ’, numeric_1st_term 33 | (’ ’ | ’ ’), set_expression 34 | (’ ’ | ’ ’), ’_’, ’, variable, ’=’, numeric_expression, [’,’, conditions], ’, ’^’, (’, numeric_expression, ’ | one_token), (’\’, numeric_expression, ’\’ | ’ ’, ’, numeric_expression, ’) 35 | (’ ’ | ’ ’), ’_’, ’, conditions, ’, (’\’, numeric_expression, ’\’ | ’ ’, ’, numeric_expression, ’); 36 37numeric_3rd_term = variable 38 | numeric 39 | ’(’, numeric_expression, ’)’ 40 | (’|’ | ’ ’), (variable | numeric_expression | set_expression), (’|’ | ’ ’) 41 | ’I’, ’(’, relation_expression, ’)’ 42 | ’ ’, numeric_expression, ’ ’ 43 | ’ ’, numeric_expression, ’ ’; 44 45set_expression = set_term 46 | set_expression, (’∪’ | ’∩’ | ’ ’ | ’ ’), set_expression; 47 48set_term = variable 49 | set 50 | ’(’, set_expression, ’)’ 51 | (’ ’ | ’ ’), ’_’, ’, variable, ’=’, numeric_expression, [’,’, conditions], ’, ’^’, (’, numeric_expression, ’ | one_token) set_term 52 | (’ ’ | ’ ’), ’_’, ’, conditions, ’, set_term; 53 54numeric = MULTI_TOKEN_NUMERIC 55 | DIGIT; 56 57set = predefined_set 58 | ’ ’, ’, numeric_expression, ’,’, numeric_expression, ’ 59 | ’\’, numeric_expression, ’,’, numeric_expression, ’\’ 60 | ’ ’, ’, numeric_expression, ’,’, (’…’ | ’...’ | ’·s’), ’,’, numeric_expression, ’ 61 | ’\’, numeric_expression, ’,’, (’…’ | ’...’ | ’cdots’), ’,’, numeric_expression, ’\’; 62 63predefined_set = ’R’ | ’R^+’ | ’R^-’ | ’Z’ | ’Z^+’ 64 | ’Z^-’ | ’N’ | ’ ’; 65 66variable = VARIABLE_TERM 67 | VARIABLE_TERM, ’_’, (’, numeric_expression, ’,’, numeric_expression, ’ | one_token); 68 69one_token = DIGIT | VARIABLE_TERM; ⬇ 70MULTI_TOKEN_NUMERIC = (’0’ | DIGIT_EXCEPT_ZERO, DIGIT), [’.’, DIGIT]; 71 72DIGIT = ’0’ | DIGIT_EXCEPT_ZERO; 73 74DIGIT_EXCEPT_ZERO = ’1’ | ’2’ | ’3’ | ’4’ | ’5’ | ’6’ | ’7’ | ’8’ | ’9’; 75 76VARIABLE_TERM = LETTER 77 | GREEK_LETTER 78 | ’ ’, ’, LETTER, ’ 79 | ’ ’, ’ , LETTER, ’ 80 | ’ ’, ’, (LETTER | GREEK_LETTER), ’; 81 82LETTER = ’a’ | ’b’ | ’c’ | ’d’ | ’e’ | ’f’ | ’g’ | ’h’ | ’i’ | ’j’ | ’k’ | ’l’ | ’m’ | ’n’ | ’o’ | ’p’ 83 | ’q’ | ’r’ | ’s’ | ’t’ | ’u’ | ’v’ | ’w’ | ’x’ | ’y’ | ’z’ | ’A’ | ’B’ | ’C’ | ’D’ | ’E’ | ’F’ 84 | ’G’ | ’H’ | ’I’ | ’J’ | ’K’ | ’L’ | ’M’ | ’N’ | ’O’ | ’P’ | ’Q’ | ’R’ | ’S’ | ’T’ | ’U’ | ’V’ 85 | ’W’ | ’X’ | ’Y’ | ’Z’; 86 87GREEK_LETTER = ’ ’ | ’ ’ | ’ ’ | ’ ’ | ’ ’ | ’ ’ | ’ ’ | ’ ’ 88 | ’ ’ | ’ ’ | ’ ’ | ’ ’ | ’ ’ | ’ ’ | ’ ’ | ’ ’ | ’ ’ 89 | ’ ’ | ’ ’ | ’ ’ | ’ ’ | ’ ’ | ’ ’ | ’ ’ | ’α’ | ’β’ 90 | ’γ’ | ’δ’ | ’ε’ | ’ζ’ | ’η’ | ’θ’ | ’ ’ | ’κ’ 91 | ’λ’ | ’μ’ | ’ν’ | ’ξ’ | ’ ’ | ’π’ | ’ρ’ | ’σ’ | ’τ’ 92 | ’ ’ | ’φ’ | ’χ’ | ’ψ’ | ’ω’ | ’ ’ | ’ ’ 93 | ’ ’ | ’ ’ | ’ ’ | ’ ’ | ’ ’; Appendix B Mathematical Models of the Test Problems The mathematical models of the test problems used in the experiments are represented in the proposed modeling language as follows: B.1 Graph Coloring Problem The Graph Coloring Problem[41] involves assigning colors to the vertices of a given undirected connected graph such that each vertex receives exactly one color, and no two adjacent vertices share the same color. The objective is to determine a valid coloring scheme that minimizes the total number of distinct colors used. The mathematical model of this problem represented in the proposed modeling language is shown in Formulas 30-32. min maxi=1nxi _i=1^n\x_i\ (30) xi≠xj x_i≠ x_j i,j=1,…,n,i<j,ci,j=1 i,j=1,…,n,i<j,c_i,j=1 (31) xi∈1,…,n x_i∈\1,…,n\ i=1,…,n i=1,…,n (32) where xix_i denotes the color assigned to vertex i, ci,jc_i,j indicates whether vertices i and j are adjacent. B.2 Traveling Salesman Problem The Traveling Salesman Problem[42] is defined as follows: Given a set of n cities, a salesman must start from an initial city, visit each of the remaining cities exactly once, and return to the starting city. The objective is to find the shortest path that satisfies these constraints. The mathematical model of this problem represented in the proposed modeling language is shown in Formulas 33-38. min ∑i=1n∑j=1,j≠inci,jxi,j _i=1^n _j=1,j≠ i^nc_i,jx_i,j (33) s.t. s.t. xi,j∈0,1 x_i,j∈\0,1\ i,j=1,…,n i,j=1,…,n (34) ∑i=1,i≠jnxi,j=1 _i=1,i≠ j^nx_i,j=1 j=1,…,n j=1,…,n (35) ∑j=1,j≠inxi,j=1 _j=1,j≠ i^nx_i,j=1 i=1,…,n i=1,…,n (36) ui−uj+nxi,j≤n−1 u_i-u_j+nx_i,j≤ n-1 2≤i≤n,2≤j≤n,i≠j 2≤ i≤ n,2≤ j≤ n,i≠ j (37) ui∈2,…,n u_i∈\2,…,n\ i=2,…,n i=2,…,n (38) where n is the number of cites, xi,jx_i,j indicates whether the salesman travels from city i to city j, ci,jc_i,j denotes the distances between city i, and city j, and uiu_i represents the order in which city i is visited by the salesman. B.3 Quadratic Assignment Problem The Quadratic Assignment Problem[45] is defined as follows: Given n facilities and n distinct locations, the objective is to assign each facility to a unique location such that the total cost is minimized. The total cost is determined by the sum of the products of the flow between each pair of facilities and the distance between their assigned locations, weighted by the associated transportation cost. The mathematical model of this problem represented in the proposed modeling language is shown in Formulas 39-42. min ∑i=1n∑j=1n∑k=1n∑l=1nfi,jdk,lxi,kxj,l _i=1^n _j=1^n _k=1^n _l=1^nf_i,jd_k,lx_i,kx_j,l (39) s.t. s.t. xi,j∈0,1 x_i,j∈\0,1\ i,j=1,…,n i,j=1,…,n (40) ∑i=1nxi,j=1 _i=1^nx_i,j=1 j=1,…,n j=1,…,n (41) ∑j=1nxi,j=1 _j=1^nx_i,j=1 i=1,…,n i=1,…,n (42) where xi,jx_i,j indicates whether facility i is assigned to location j, fi,jf_i,j denotes the transportation cost from facility i to facility j, and di,jd_i,j denotes the distance from facility i to facility j. B.4 Capacitated Vehicle Routing Problem The Capacitated Vehicle Routing Problem[43] is defined as follows: Given a depot, n−1n-1 customer locations, and a fleet of n vehicles, each with a capacity of Q, the objective is to determine a set of routes for the vehicles such that: (1) Each route starts and ends at the depot; (2) Each customer is visited exactly once by exactly one vehicle; (3) The total demand of the customers served on any single route does not exceed the vehicle capacity Q; (4) The required quantity of goods is delivered to each customer upon visit. The goal is to minimize the total travel distance across all vehicles. The mathematical model of this problem represented in the proposed modeling language is shown in Formulas 43-51. min ∑k=1m∑i=1n∑j=1ndi,jxi,j,k _k=1^m _i=1^n _j=1^nd_i,jx_i,j,k (43) s.t. s.t. xi,j,k∈0,1 x_i,j,k∈\0,1\ ∀k∈1,…,m,i,j∈1,…,n ∀ k∈\1,…,m\,i,j∈\1,…,n\ (44) xi,i,k=0 x_i,i,k=0 ∀k∈1,…,m,i∈1,…,n ∀ k∈\1,…,m\,i∈\1,…,n\ (45) ∑i=1nxi,j,k=∑i=1nxj,i,k _i=1^nx_i,j,k= _i=1^nx_j,i,k ∀j∈1,…,n,k∈1,…,m ∀ j∈\1,…,n\,k∈\1,…,m\ (46) ∑k=1m∑i=1nxi,j,k=1 _k=1^m _i=1^nx_i,j,k=1 ∀j∈2,…,n ∀ j∈\2,…,n\ (47) ∑j=2nx1,j,k=1 _j=2^nx_1,j,k=1 ∀k∈1,…,m ∀ k∈\1,…,m\ (48) ∑i=1n∑j=2nqjxi,j,k≤Q _i=1^n _j=2^nq_jx_i,j,k≤ Q ∀k∈1,…,m ∀ k∈\1,…,m\ (49) uj−ui−qj+Q≥Qmaxk=1mxi,j,k u_j-u_i-q_j+Q≥ Q _k=1^m\x_i,j,k\ ∀i,j∈2,…,n,i≠j ∀ i,j∈\2,…,n\,i≠ j (50) ui∈qi,…,Q u_i∈\q_i,…,Q\ ∀i∈2,…,n ∀ i∈\2,…,n\ (51) where n is the number of locations, the first location is the depot, the rest are locations of customers, m is the number of vehicles, xi,j,kx_i,j,k indicates whether vehicle k travels from location i to location j, di,jd_i,j denotes the distance from location i to location j, qiq_i denotes the demand of customer i, Q is the capacity of each vehicle, and uiu_i denotes the cumulative amount of goods delivered by a vehicle upon completing service at location i. B.5 Two-Echelon Vehicle Routing Problem The Two-Echelon Vehicle Routing Problem[41] is defined on a two-level distribution system comprising one central depot, m satellites, n customers, N1N_1 first-level vehicles, and N2N_2 second-level vehicles. All customer demands are known and must be satisfied. Goods are initially located at the depot and must be transferred to customers via the satellites: first-level vehicles move goods from the depot to the satellites, and second-level vehicles then distribute them from the satellites to the customers. Each customer is visited exactly once by a single second-level vehicle. The objective is to determine the number of vehicles used at each level and to design routes for first-level and second-level vehicles such that all customer demands are met and the total travel distance across all vehicles is minimized. The mathematical model of this problem represented in the proposed modeling language is shown in Formulas 52-72. min ∑i,j∈0∪S,i≠jci,jyi,j+∑i∈S∑j∈C(ci,jzi,j,i+cj,izj,i,i)+∑k∈S∑i,j∈C,i≠jci,jzi,j,k _i,j∈\0\∪ S,i≠ jc_i,jy_i,j+ _i∈ S _j∈ C(c_i,jz_i,j,i+c_j,iz_j,i,i)+ _k∈ S _i,j∈ C,i≠ jc_i,jz_i,j,k (52) s.t. s.t. ∑i∈Sy0,i≤N1 _i∈ Sy_0,i≤ N_1 (53) ∑i∈0∪S,i≠jyi,j=∑i∈0∪S,i≠jyj,i _i∈\0\∪ S,i≠ jy_i,j= _i∈\0\∪ S,i≠ jy_j,i ∀j∈S ∀ j∈ S (54) ∑i∈S∑j∈Czi,j,i≤N2 _i∈ S _j∈ Cz_i,j,i≤ N_2 (55) ∑i∈S∪C,i≠jzi,j,k=∑i∈S∪C,i≠jzj,i,k _i∈ S∪ C,i≠ jz_i,j,k= _i∈ S∪ C,i≠ jz_j,i,k ∀k∈S,j∈C ∀ k∈ S,j∈ C (56) zi,j,k=0 z_i,j,k=0 ∀k∈S,i,j∈S,i≠j ∀ k∈ S,i,j∈ S,i≠ j (57) zi,j,k=0 z_i,j,k=0 ∀k∈S,i∈S,j∈C,i≠k ∀ k∈ S,i∈ S,j∈ C,i≠ k (58) zj,i,k=0 z_j,i,k=0 ∀k∈S,i∈S,j∈C,i≠k ∀ k∈ S,i∈ S,j∈ C,i≠ k (59) Q1,i,j≤yi,jT1 Q_1,i,j≤ y_i,jT_1 ∀i,j∈0∪S,i≠j ∀ i,j∈\0\∪ S,i≠ j (60) Q2,i,j≤∑k∈Szi,j,kT2 Q_2,i,j≤ _k∈ Sz_i,j,kT_2 ∀i,j∈S∪C,i≠j ∀ i,j∈ S∪ C,i≠ j (61) Q1,i,0=0 Q_1,i,0=0 ∀i∈S ∀ i∈ S (62) Q2,i,j=0 Q_2,i,j=0 ∀i∈S∪C,j∈S,i≠j ∀ i∈ S∪ C,j∈ S,i≠ j (63) ∑i∈0∪S,i≠jQ1,i,j=∑k∈0∪S,k≠jQ1,j,k+∑l∈CQ2,j,l _i∈\0\∪ S,i≠ jQ_1,i,j= _k∈\0\∪ S,k≠ jQ_1,j,k+ _l∈ CQ_2,j,l ∀j∈S ∀ j∈ S (64) ∑i∈S∪C,i≠jQ2,i,j=∑k∈S∪C,k≠jQ2,j,k+ρj _i∈ S∪ C,i≠ jQ_2,i,j= _k∈ S∪ C,k≠ jQ_2,j,k+ _j ∀j∈C ∀ j∈ C (65) ∑k∈S∑i∈S∪C,i≠jzi,j,k=1 _k∈ S _i∈ S∪ C,i≠ jz_i,j,k=1 ∀j∈C ∀ j∈ C (66) zi,j,k∈0,1 z_i,j,k∈\0,1\ ∀k∈S,i,j∈S∪C,i≠j ∀ k∈ S,i,j∈ S∪ C,i≠ j (67) yi,j∈0,…,N1 y_i,j∈\0,...,N_1\ ∀i,j∈0∪S,i≠j ∀ i,j∈\0\∪ S,i≠ j (68) S=1,…,m S=\1,…,m\ (69) C=m+1,…,m+n C=\m+1,…,m+n\ (70) Q1,i,j∈0,…,N1T1 Q_1,i,j∈\0,…,N_1T_1\ ∀i,j∈0∪S,i≠j ∀ i,j∈\0\∪ S,i≠ j (71) Q2,i,j∈0,…,T2 Q_2,i,j∈\0,…,T_2\ ∀i,j∈S∪C,i≠j ∀ i,j∈ S∪ C,i≠ j (72) where there are m+n+1m+n+1 positions, position 0 is the depot, positions 11 to m are satellites, denoted by set S, positions m+1m+1 to m+nm+n are customers, denoted by set C. N1N_1 and N2N_2 are the number of candidate first-level and second-level vehicles, respectively. ci,jc_i,j denotes the distance from position i to position j. yi,jy_i,j denotes the number of first-level vehicles that travel from position i to position j. zi,j,kz_i,j,k indicates whether second-vehicle k travels from position i to position j. ρj _j is the demand of customer j. Qk,i,jQ_k,i,j denotes the amount of goods carried by a vehicle at level k on the route segment from location i to location j. TkT_k represents the capacity of vehicles at level k. B.6 Multidimensional Knapsack Problem The Multidimensional Knapsack Problem[41] is defined as follows: Given a set of n items and a single knapsack, each item has an associated value and m distinct weight attributes. The knapsack has a capacity constraint on each of the m weight dimensions. The objective is to select a subset of items to place into the knapsack such that the total value of the selected items is maximized, while ensuring that the sum of weights in each dimension does not exceed the corresponding capacity constraint of the knapsack. The mathematical model of this problem represented in the proposed modeling language is shown in Formulas 73-75. max ∑i=1nvixi _i=1^nv_ix_i (73) s.t. s.t. ∑i=1nwi,jxi≤Wj _i=1^nw_i,jx_i≤ W_j j=1,…,m j=1,…,m (74) xi∈0,1 x_i∈\0,1\ i=1,…,n i=1,…,n (75) where n is the number of items, m is the number of weight dimensions, viv_i is the value of item i, wi,jw_i,j is the weight of item i on dimension j, WjW_j is the capacity of the j-th weight dimension, and xix_i indicates whether item i is selected to place into the knapsack. B.7 Job-Shop Scheduling Problem The Job-Shop Scheduling Problem[44] is defined as follows: Given n jobs and m machines, each job must be processed on each machine exactly once. The processing order and time across machines are predetermined and may differ for each job. The constraints are that (1) each machine can process at most one job at a time, and (2) each job can be processed on only one machine at a time. The objective is to determine a feasible schedule that minimizes the makespan, i.e., the total time required to complete all jobs. The mathematical model of this problem represented in the proposed modeling language is shown in Formulas 76-86. min C C (76) s.t. s.t. 0≤xi,j≤V 0≤ x_i,j≤ V ∀j∈J,i∈M ∀ j∈ J,i∈ M (77) xσj,h,j≥xσj,h−1,j+pσj,h−1,j x_ _j,h,j≥ x_ _j,h-1,j+p_ _j,h-1,j ∀j∈J,h=2,…,m ∀ j∈ J,h=2,…,m (78) xi,j≥xi,k+pi,k−2V⋅zi,j,k x_i,j≥ x_i,k+p_i,k-2V· z_i,j,k ∀j,k∈J,j<k,i∈M ∀ j,k∈ J,j<k,i∈ M (79) xi,k≥xi,j+pi,j−2V⋅(1−zi,j,k) x_i,k≥ x_i,j+p_i,j-2V·(1-z_i,j,k) ∀j,k∈J,j<k,i∈M ∀ j,k∈ J,j<k,i∈ M (80) xσj,m,j+pσj,m,j≤C x_ _j,m,j+p_ _j,m,j≤ C ∀j∈J ∀ j∈ J (81) zi,j,k∈0,1 z_i,j,k∈\0,1\ ∀j,k∈J,j<k,i∈M ∀ j,k∈ J,j<k,i∈ M (82) V=∑j∈J∑i∈Mpi,j V= _j∈ J _i∈ Mp_i,j (83) J=1,…,n J=\1,…,n\ (84) M=1,…,m M=\1,…,m\ (85) xi,j∈ℤ x_i,j ∀j∈J,i∈M ∀ j∈ J,i∈ M (86) where C denotes the makespan, J is the set of jobs with |J|=n|J|=n, and M is the set of machines with |M|=m|M|=m. σj,h _j,h represents the machine required for the h-th operation of job j, where each job consists of exactly m operations, and no two operations of the same job are processed on the same machine. xi,jx_i,j denotes the start time of job j on machine i, and pi,jp_i,j is the processing time of job j on machine i. The binary variable zi,j,kz_i,j,k indicates whether job j starts before job k on machine i. V is a sufficiently large positive constant (big-M value). B.8 Open-Shop Scheduling Problem The Open Shop Scheduling Problem[44] is defined as follows: Given n jobs and m machines, each job must be processed exactly once on each machine, but the processing order of machines for any job is not predetermined and can be chosen freely. The processing time of each job on each machine is given and may vary across jobs and machines. The constraints are that (1) each machine can process at most one job at a time, and (2) each job can be processed on only one machine at a time. The objective is to determine a feasible schedule, including the processing sequence on each machine and for each job, that minimizes the makespan, i.e., the total time required to complete all jobs. The mathematical model of this problem represented in the proposed modeling language is shown in Formulas 87-99. min C C (87) s.t. s.t. 0≤xi,j≤V 0≤ x_i,j≤ V ∀j∈J,i∈M ∀ j∈ J,i∈ M (88) xk,i≥xj,i+pj,i−2V⋅wi,j,k x_k,i≥ x_j,i+p_j,i-2V· w_i,j,k ∀i∈J,j,k∈M,j<k ∀ i∈ J,j,k∈ M,j<k (89) xj,i≥xk,i+pk,i−2V⋅(1−wi,j,k) x_j,i≥ x_k,i+p_k,i-2V·(1-w_i,j,k) ∀i∈J,j,k∈M,j<k ∀ i∈ J,j,k∈ M,j<k (90) xi,j≥xi,k+pi,k−2V⋅zi,j,k x_i,j≥ x_i,k+p_i,k-2V· z_i,j,k ∀i∈M,j,k∈J,j<k ∀ i∈ M,j,k∈ J,j<k (91) xi,k≥xi,j+pi,j−2V⋅(1−zi,j,k) x_i,k≥ x_i,j+p_i,j-2V·(1-z_i,j,k) ∀i∈M,j,k∈J,j<k ∀ i∈ M,j,k∈ J,j<k (92) xi,j+pi,j≤C x_i,j+p_i,j≤ C ∀i∈M,j∈J ∀ i∈ M,j∈ J (93) zi,j,k∈0,1 z_i,j,k∈\0,1\ ∀i∈M,j,k∈J,j<k ∀ i∈ M,j,k∈ J,j<k (94) wi,j,k∈0,1 w_i,j,k∈\0,1\ ∀i∈J,j,k∈M,j<k ∀ i∈ J,j,k∈ M,j<k (95) V=∑i∈M∑j∈Jpi,j V= _i∈ M _j∈ Jp_i,j (96) J=1,…,n J=\1,…,n\ (97) M=1,…,m M=\1,…,m\ (98) xi,j∈ℤ x_i,j ∀j∈J,i∈M ∀ j∈ J,i∈ M (99) where C denotes the makespan, J is the set of jobs with |J|=n|J|=n, and M is the set of machines with |M|=m|M|=m. xi,jx_i,j denotes the start time of job j on machine i, and pi,jp_i,j is the processing time of job j on machine i. The binary variable zi,j,kz_i,j,k indicates whether job j starts before job k on machine i. The binary variable wi,j,kw_i,j,k indicates whether job i starts on machine j before it starts on machine k. V is a sufficiently large positive constant (big-M value). B.9 Shifted Sphere Function The Shifted Sphere Function is a benchmark from IEEE CEC 2005[46]. The mathematical model of this problem represented in the proposed modeling language is shown in Formulas 100-103. min ∑i=1Dzi2+b _i=1^Dz_i^2+b (100) s.t. s.t. zi=xi−oi z_i=x_i-o_i i=1,…,D i=1,…,D (101) b=−450 b=-450 (102) −100≤xi≤100 -100≤ x_i≤ 100 i=1,…,D i=1,…,D (103) where x1x_1 to xDx_D are the decision variables, the sequence (o1,o2,…,oD)(o_1,o_2,…,o_D) denotes the optimal solution, and b is the optimal objective value. B.10 Shifted Schwefel’s Problem The Shifted Schwefel’s Problem is a benchmark from IEEE CEC 2005[46]. The mathematical model of this problem represented in the proposed modeling language is shown in Formulas 104-107. min ∑i=1D(∑j=1izj)2+b _i=1^D( _j=1^iz_j)^2+b (104) s.t. s.t. zi=xi−oi z_i=x_i-o_i i=1,…,D i=1,…,D (105) b=−450 b=-450 (106) −100≤xi≤100 -100≤ x_i≤ 100 i=1,…,D i=1,…,D (107) where x1x_1 to xDx_D are the decision variables, the sequence (o1,o2,…,oD)(o_1,o_2,…,o_D) denotes the optimal solution, and b is the optimal objective value. B.11 Shifted Rosenbrock’s Function The Shifted Rosenbrock’s Function is a benchmark from IEEE CEC 2005[46]. The mathematical model of this problem represented in the proposed modeling language is shown in Formulas 108-111. min ∑i=1D−1(100(zi2−zi+1)2+(zi−1)2)+b _i=1^D-1(100(z_i^2-z_i+1)^2+(z_i-1)^2)+b (108) s.t. s.t. zi=xi−oi+1 z_i=x_i-o_i+1 i=1,…,D i=1,…,D (109) b=−390 b=-390 (110) −100≤xi≤100 -100≤ x_i≤ 100 i=1,…,D i=1,…,D (111) where x1x_1 to xDx_D are the decision variables, the sequence (o1,o2,…,oD)(o_1,o_2,…,o_D) denotes the optimal solution, and b is the optimal objective value. Appendix C Reduction Rules of OP-to-MaxSAT Reduction In the OP-to-MaxSAT reduction, numerical variables are encoded as signed binary fixed-point numbers, shown in Formula 18. The reduction rules for reducing constraints and the objective of optimization problems are as follows: C.1 Reduction Rule for the Full Adder: FullAdder(x,y,cin,z,cout)FullAdder(x,y,c_in,z,c_out) The rule models a full adder that takes Boolean inputs x, y, and cinc_in, and produces the sum z and the carry-out coutc_out. This rule is proposed in [75]. The clauses generated by this rule are shown in Formula 112. x∨¬y∨cin∨zx∨y∨¬cin∨z¬x∨¬y∨cin∨¬z¬x∨y∨¬cin∨¬z¬x∨cout∨zx∨¬cout∨¬z¬y∨¬cin∨couty∨cin∨¬cout¬x∨¬y∨¬cin∨zx∨y∨cin∨¬z array[]cx y c_in z\\ x y c_in z\\ x y c_in z\\ x y c_in z\\ x c_out z\\ x c_out z\\ y c_in c_out\\ y c_in c_out\\ x y c_in z\\ x y c_in z\\ array (112) This rule generates 0 intermediate Boolean variables and 10 clauses. C.2 Reduction Rule for the Half Adder: HalfAdder(x,y,z,cout)HalfAdder(x,y,z,c_out) The rule models a half adder that takes Boolean inputs x and y, and produces the sum z and the carry-out coutc_out. The clauses generated by this rule are shown in Formula 113. x∨¬y∨z¬x∨¬y∨¬z¬x∨cout∨zx∨¬cout∨¬zy∨¬coutx∨y∨¬z array[]cx y z\\ x y z\\ x c_out z\\ x c_out z\\ y c_out\\ x y z\\ array (113) This rule generates 0 intermediate Boolean variables and 6 clauses. C.3 Reduction Rule for the Two’s Complement: Complement(,′)Complement( a, a ) The rule models the relation between a signed binary fixed-point number =am+nam+n−1⋯a0 a=a_m+na_m+n-1·s a_0 and its two’s complement encoding ′=am+n′am+n−1′⋯a0′ a =a _m+na _m+n-1·s a _0. The clauses generated by this rule are shown in Formula 114. am+n∨¬ai∨ai′i=0,…,m+n−1am+n∨ai∨¬ai′i=0,…,m+n−1am+n∨¬am+n′¬am+n∨d0¬am+n∨HalfAdder(¬ai,di,ai′,di+1)i=0,…,m+n−1¬am+n∨dm+n∨am+n′¬am+n∨¬dm+n∨¬am+n′⋁i=0m+n−1ai′∨¬am+n′ array[]cla_m+n a_i a _i&i=0,…,m+n-1\\ a_m+n a_i a _i&i=0,…,m+n-1\\ a_m+n a _m+n\\ a_m+n d_0\\ a_m+n HalfAdder( a_i,d_i,a _i,d_i+1)&i=0,…,m+n-1\\ a_m+n d_m+n a _m+n\\ a_m+n d_m+n a _m+n\\ _i=0^m+n-1a _i a _m+n\\ array (114) where d0d_0 to dm+nd_m+n are intermediate Boolean variables. This rule generates m+n+1m+n+1 intermediate Boolean variables and 8m+8n+58m+8n+5 clauses. C.4 Reduction Rule for the Adder Supporting Two Inputs: Adder(′,′,′)Adder( a , b , c ) The rule models an adder that takes the two’s complement encodings ′ a and ′ b as inputs, and produces the two’s complement of the sum ′ c . The clauses generated by this rule are shown in Formula 115. ¬d0¬am+n′∨¬bm+n′∨cm+n′am+n′∨bm+n′∨¬cm+n′ai′∨bi′∨¬di+1i=0,…,m+n¬ai′∨¬bi′∨di+1i=0,…,m+nFullAdder(ai′,bi′,di,ci′,di+1)i=0,…,m+n array[]cl d_0\\ a _m+n b _m+n c _m+n\\ a _m+n b _m+n c _m+n\\ a _i b _i d_i+1&i=0,…,m+n\\ a _i b _i d_i+1&i=0,…,m+n\\ FullAdder(a _i,b _i,d_i,c _i,d_i+1)&i=0,…,m+n\\ array (115) where d0d_0 to dm+nd_m+n are intermediate Boolean variables. This rule generates m+n+1m+n+1 intermediate Boolean variables and 12m+12n+1512m+12n+15 clauses. C.5 Reduction Rule for the Adder Supporting Multiple Inputs: MultiAdder(1′,2′,⋯,k′,′)MultiAdder(\ a _1, a _2,·s, a _k\, c ) The rule models a more powerful adder that takes the two’s complement encodings 1′ a _1 to k′ a _k as inputs (k≥2k≥ 2), and produces the two’s complement of the sum ′ c . The clauses generated by this rule are shown in Formula 116. (k=2)→Adder(1′,2′,′)(k=3)→Adder(1′,2′,′)Adder(′,3′,′)(k≥4)→MultiAdder(1′,⋯,⌊k/2⌋′,1′)MultiAdder(⌊k/2⌋+1′,⋯,k′,2′)Adder(1′,2′,′) array[]l(k=2)→ Adder( a _1, a _2, c )\\ (k=3)→ BmatrixAdder( a _1, a _2, e )\\ Adder( e , a _3, c ) Bmatrix\\ (k≥ 4)→ BmatrixMultiAdder(\ a _1,·s, a _ k/2 \, b _1)\\ MultiAdder(\ a _ k/2 +1,·s, a _k\, b _2)\\ Adder( b _1, b _2, c )\\ Bmatrix\\ array (116) where ′ e , 1′ b _1, and 2′ b _2 are intermediate variables. This rule generates (2k−3)m+(2k−3)n+(2k−3)(2k-3)m+(2k-3)n+(2k-3) intermediate Boolean variables and 12(k−1)m+12(k−1)n+15(k−1)12(k-1)m+12(k-1)n+15(k-1) clauses. C.6 Reduction Rule for Sum Expression: Sum(1,2,⋯,k,)Sum(\ a_1, a_2,·s, a_k\, c) The rule models the expression =∑i=1ki c= _i=1^k a_i, where i a_i and c are signed binary fixed-point numbers. The clauses generated by this rule are shown in Formula 117. Complement(i,i′)i=1,…,kMultiAdder(1′,⋯,k′,′)Complement(,′) array[]clComplement( a_i, a _i)&i=1,…,k\\ MultiAdder(\ a _1,·s, a _k\, c )\\ Complement( c, c ) array (117) This rule generates (4k−1)m+(4k−1)n+(4k−1)(4k-1)m+(4k-1)n+(4k-1) intermediate Boolean variables and (20k−4)m+(20k−4)n+(20k−10)(20k-4)m+(20k-4)n+(20k-10) clauses. C.7 Reduction Rule for Equal Expression: Equal(,)Equal( a, b) The rule models the expression = a= b, where a and b are signed binary fixed-point numbers. The clauses generated by this rule are shown in Formula 118. ¬am+n∨¬bm+n∨eam+n∨bm+n∨eam+n∨¬bm+n∨¬e¬am+n∨bm+n∨¬e¬e∨¬ai∨bii=0,…,m+n−1¬e∨ai∨¬bii=0,…,m+n−1e∨¬aii=0,…,m+n−1e∨¬bii=0,…,m+n−1 array[]cl a_m+n b_m+n e\\ a_m+n b_m+n e\\ a_m+n b_m+n e\\ a_m+n b_m+n e\\ e a_i b_i&i=0,…,m+n-1\\ e a_i b_i&i=0,…,m+n-1\\ e a_i&i=0,…,m+n-1\\ e b_i&i=0,…,m+n-1\\ array (118) where e is an intermediate Boolean variable. This rule generates 1 intermediate Boolean variable and 4m+4n+44m+4n+4 clauses. C.8 Reduction Rule for Not Equal Expression: NotEqual(,)NotEqual( a, b) The rule models the expression ≠ a≠ b, where a and b are signed binary fixed-point numbers. The clauses generated by this rule are shown in Formula 119. ¬am+n∨¬bm+n∨eam+n∨bm+n∨eam+n∨¬bm+n∨¬e¬am+n∨bm+n∨¬e¬e∨¬ai∨bi∨pii=0,…,m+n−1¬e∨ai∨¬bi∨pii=0,…,m+n−1¬e∨¬ai∨¬bi∨¬pii=0,…,m+n−1¬e∨ai∨bi∨¬pii=0,…,m+n−1¬e∨⋁i=0m+n−1pie∨⋁i=0m+n−1ai∨⋁i=0m+n−1bi array[]cl a_m+n b_m+n e\\ a_m+n b_m+n e\\ a_m+n b_m+n e\\ a_m+n b_m+n e\\ e a_i b_i p_i&i=0,…,m+n-1\\ e a_i b_i p_i&i=0,…,m+n-1\\ e a_i b_i p_i&i=0,…,m+n-1\\ e a_i b_i p_i&i=0,…,m+n-1\\ e _i=0^m+n-1p_i\\ e _i=0^m+n-1a_i _i=0^m+n-1b_i\\ array (119) where e and pip_i are intermediate Boolean variables. This rule generates m+n+1m+n+1 intermediate Boolean variables and 4m+4n+64m+4n+6 clauses. C.9 Reduction Rule for Less-Than Expression: LessThan(,)LessThan( a, b) The rule models the expression < a< b, where a and b are signed binary fixed-point numbers. The clauses generated by this rule are shown in Formula 120. am+n∨¬bm+n¬am+n∨bm+n∨⋁i=0m+n−1ai∨⋁i=0m+n−1bi¬qm+n¬pm+n¬ai∨bi∨qii=m,…,m+n−1¬qi+1∨qii=m,…,m+n−1ai∨qi+1∨¬qii=m,…,m+n−1¬bi∨qi+1∨¬qii=m,…,m+n−1ai∨¬bi∨pii=m,…,m+n−1¬pi+1∨pii=m,…,m+n−1¬ai∨pi+1∨¬pii=m,…,m+n−1bi∨pi+1∨¬pii=m,…,m+n−1⋁i=0m−1ai∨⋁i=0m−1bi∨d¬ai∨¬di=0,…,m−1¬bi∨¬di=0,…,m−1¬d∨qii=0,…,m−1¬d∨pii=0,…,m−1d∨¬ai∨bi∨qii=0,…,m−1d∨¬qi+1∨qii=0,…,m−1d∨ai∨qi+1∨¬qii=0,…,m−1d∨¬bi∨qi+1∨¬qii=0,…,m−1d∨ai∨¬bi∨pii=0,…,m−1d∨¬pi+1∨pii=0,…,m−1d∨¬ai∨pi+1∨¬pii=0,…,m−1d∨bi∨pi+1∨¬pii=0,…,m−1q0∨p0¬qi∨¬pi∨qi+1∨pi+1i=0,…,m+n−1am+n∨bm+n∨¬qi∨pii=0,…,m+n−1¬am+n∨¬bm+n∨qi∨¬pii=0,…,m+n−1 array[]cla_m+n b_m+n\\ a_m+n b_m+n _i=0^m+n-1a_i _i=0^m+n-1b_i\\ q_m+n\\ p_m+n\\ a_i b_i q_i&i=m,…,m+n-1\\ q_i+1 q_i&i=m,…,m+n-1\\ a_i q_i+1 q_i&i=m,…,m+n-1\\ b_i q_i+1 q_i&i=m,…,m+n-1\\ a_i b_i p_i&i=m,…,m+n-1\\ p_i+1 p_i&i=m,…,m+n-1\\ a_i p_i+1 p_i&i=m,…,m+n-1\\ b_i p_i+1 p_i&i=m,…,m+n-1\\ _i=0^m-1a_i _i=0^m-1b_i d\\ a_i d&i=0,…,m-1\\ b_i d&i=0,…,m-1\\ d q_i&i=0,…,m-1\\ d p_i&i=0,…,m-1\\ d a_i b_i q_i&i=0,…,m-1\\ d q_i+1 q_i&i=0,…,m-1\\ d a_i q_i+1 q_i&i=0,…,m-1\\ d b_i q_i+1 q_i&i=0,…,m-1\\ d a_i b_i p_i&i=0,…,m-1\\ d p_i+1 p_i&i=0,…,m-1\\ d a_i p_i+1 p_i&i=0,…,m-1\\ d b_i p_i+1 p_i&i=0,…,m-1\\ q_0 p_0\\ q_i p_i q_i+1 p_i+1&i=0,…,m+n-1\\ a_m+n b_m+n q_i p_i&i=0,…,m+n-1\\ a_m+n b_m+n q_i p_i&i=0,…,m+n-1\\ array (120) where d, qiq_i, and pip_i are intermediate Boolean variables. This rule generates 2m+2n+22m+2n+2 intermediate Boolean variables and 15m+11n+615m+11n+6 clauses. C.10 Reduction Rule for Less-Than-or-Equal-To Expression: LessEqual(,)LessEqual( a, b) The rule models the expression ≤ a≤ b, where a and b are signed binary fixed-point numbers. The clauses generated by this rule are shown in Formula 121. am+n∨¬bm+n∨¬aii=0,…,m+n−1am+n∨¬bm+n∨¬bii=0,…,m+n−1¬qm+n¬pm+n¬ai∨bi∨qii=m,…,m+n−1¬qi+1∨qii=m,…,m+n−1ai∨qi+1∨¬qii=m,…,m+n−1¬bi∨qi+1∨¬qii=m,…,m+n−1ai∨¬bi∨pii=m,…,m+n−1¬pi+1∨pii=m,…,m+n−1¬ai∨pi+1∨¬pii=m,…,m+n−1bi∨pi+1∨¬pii=m,…,m+n−1⋁i=0m−1ai∨⋁i=0m−1bi∨d¬ai∨¬di=0,…,m−1¬bi∨¬di=0,…,m−1¬d∨qii=0,…,m−1¬d∨pii=0,…,m−1d∨¬ai∨bi∨qii=0,…,m−1d∨¬qi+1∨qii=0,…,m−1d∨ai∨qi+1∨¬qii=0,…,m−1d∨¬bi∨qi+1∨¬qii=0,…,m−1d∨ai∨¬bi∨pii=0,…,m−1d∨¬pi+1∨pii=0,…,m−1d∨¬ai∨pi+1∨¬pii=0,…,m−1d∨bi∨pi+1∨¬pii=0,…,m−1am+n∨bm+n∨¬qi∨pii=0,…,m+n−1¬am+n∨¬bm+n∨qi∨¬pii=0,…,m+n−1 array[]cla_m+n b_m+n a_i&i=0,…,m+n-1\\ a_m+n b_m+n b_i&i=0,…,m+n-1\\ q_m+n\\ p_m+n\\ a_i b_i q_i&i=m,…,m+n-1\\ q_i+1 q_i&i=m,…,m+n-1\\ a_i q_i+1 q_i&i=m,…,m+n-1\\ b_i q_i+1 q_i&i=m,…,m+n-1\\ a_i b_i p_i&i=m,…,m+n-1\\ p_i+1 p_i&i=m,…,m+n-1\\ a_i p_i+1 p_i&i=m,…,m+n-1\\ b_i p_i+1 p_i&i=m,…,m+n-1\\ _i=0^m-1a_i _i=0^m-1b_i d\\ a_i d&i=0,…,m-1\\ b_i d&i=0,…,m-1\\ d q_i&i=0,…,m-1\\ d p_i&i=0,…,m-1\\ d a_i b_i q_i&i=0,…,m-1\\ d q_i+1 q_i&i=0,…,m-1\\ d a_i q_i+1 q_i&i=0,…,m-1\\ d b_i q_i+1 q_i&i=0,…,m-1\\ d a_i b_i p_i&i=0,…,m-1\\ d p_i+1 p_i&i=0,…,m-1\\ d a_i p_i+1 p_i&i=0,…,m-1\\ d b_i p_i+1 p_i&i=0,…,m-1\\ a_m+n b_m+n q_i p_i&i=0,…,m+n-1\\ a_m+n b_m+n q_i p_i&i=0,…,m+n-1\\ array (121) where d, qiq_i, and pip_i are intermediate Boolean variables. This rule generates 2m+2n+32m+2n+3 intermediate Boolean variables and 16m+12n+316m+12n+3 clauses. C.11 Reduction Rule for the Multiplier: Multiplier(,,)Multiplier( a, b, c) The rule models an multiplier that takes signed binary fixed-point numbers a and b as inputs, produces the product c. The clauses generated by this rule are shown in Formula 122. ¬am+n∨bm+n∨cm+nam+n∨¬bm+n∨cm+n¬am+n∨¬bm+n∨¬cm+nam+n∨bm+n∨¬cm+n¬ai∨¬bj∨Ti,ji=0,…,m+n−1,j=0,…,m+n−1,1≤i+j≤2m+n−1ai∨¬Ti,ji=0,…,m+n−1,j=0,…,m+n−1,1≤i+j≤2m+n−1bj∨¬Ti,ji=0,…,m+n−1,j=0,…,m+n−1,1≤i+j≤2m+n−1¬di,0∨Ti,0i=1,…,m+n−1di,0∨¬Ti,0i=1,…,m+n−1¬dm+n,0¬e0,i=1,…,m+n−1FullAdder(Ti,j,di+1,j−1,ei,j,di,j,ei+1,j)i=0,…,m+n−1,j=1,…,m+n−1,1≤i+j≤2m+n−1¬dm+n,j∨em+n,j=1,…,m−1dm+n,j∨¬em+n,j=1,…,m−1¬ci∨di+m−mini+m,m+n−1,mini+m,m+n−1i=0,…,m+n−1ci∨¬di+m−mini+m,m+n−1,mini+m,m+n−1i=0,…,m+n−1¬e2m+n−j,j=m,…,m+n−1¬ai∨¬bii=0,…,m+n−1,j=0,…,m+n−1,i+j>2m+n−1 array[]cl a_m+n b_m+n c_m+n\\ a_m+n b_m+n c_m+n\\ a_m+n b_m+n c_m+n\\ a_m+n b_m+n c_m+n\\ a_i b_j T_i,j&i=0,…,m+n-1,j=0,…,m+n-1,1≤ i+j≤ 2m+n-1\\ a_i T_i,j&i=0,…,m+n-1,j=0,…,m+n-1,1≤ i+j≤ 2m+n-1\\ b_j T_i,j&i=0,…,m+n-1,j=0,…,m+n-1,1≤ i+j≤ 2m+n-1\\ d_i,0 T_i,0&i=1,…,m+n-1\\ d_i,0 T_i,0&i=1,…,m+n-1\\ d_m+n,0\\ e_0,i&i=1,…,m+n-1\\ FullAdder(T_i,j,d_i+1,j-1,e_i,j,d_i,j,e_i+1,j)&i=0,…,m+n-1,j=1,…,m+n-1,1≤ i+j≤ 2m+n-1\\ d_m+n,j e_m+n,j&j=1,…,m-1\\ d_m+n,j e_m+n,j&j=1,…,m-1\\ c_i d_i+m- \i+m,m+n-1\, \i+m,m+n-1\&i=0,…,m+n-1\\ c_i d_i+m- \i+m,m+n-1\, \i+m,m+n-1\&i=0,…,m+n-1\\ e_2m+n-j,j&j=m,…,m+n-1\\ a_i b_i&i=0,…,m+n-1,j=0,…,m+n-1,i+j>2m+n-1\\ array (122) where Ti,jT_i,j, di,jd_i,j, and ei,je_i,j are intermediate Boolean variables. This rule generates 2m2+4mn+m+32n2+32n2m^2+4mn+m+ 32n^2+ 32n intermediate Boolean variables and 13m2+26mn−4m+7n2+2n+113m^2+26mn-4m+7n^2+2n+1 clauses. C.12 Reduction Rule for Product Expression: Product(1,2,⋯,k,)Product(\ a_1, a_2,·s, a_k\, c) The rule models the expression =∏i=1ki c= _i=1^k a_i, where i a_i and c are signed binary fixed-point numbers. The clauses generated by this rule are shown in Formula 123. ⋁j=0m+n−1ai,j∨di=1,…,k⋁j=0m+n−1ai,j∨eii=1,…,k¬ai,j∨¬eii=1,…,k,j=0,…,m+n−1⋁i=1kei∨¬d⋁j=0m+n−1cj∨d¬d∨¬cjj=0,…,m+n−1d∨Multiplier(1,2,2)d∨Multiplier(i−1,i,i)i=3,…,kd∨¬bk,j∨cjj=0,…,m+nd∨bk,j∨¬cjj=0,…,m+n array[]cl _j=0^m+n-1a_i,j d&i=1,…,k\\ _j=0^m+n-1a_i,j e_i&i=1,…,k\\ a_i,j e_i&i=1,…,k,j=0,…,m+n-1\\ _i=1^ke_i d\\ _j=0^m+n-1c_j d\\ d c_j&j=0,…,m+n-1\\ d Multiplier( a_1, a_2, b_2)\\ d Multiplier( b_i-1, a_i, b_i)&i=3,…,k\\ d b_k,j c_j&j=0,…,m+n\\ d b_k,j c_j&j=0,…,m+n\\ array (123) where d and eie_i are intermediate Boolean variables. This rule generates 2(k−1)m2+4(k−1)mn+32(k−1)n2+2(k−1)m+52(k−1)n+2k2(k-1)m^2+4(k-1)mn+ 32(k-1)n^2+2(k-1)m+ 52(k-1)n+2k intermediate Boolean variables and 13(k−1)m2+26(k−1)mn+7(k−1)n2+(7−3k)m+(3k+1)n+3(k+1)13(k-1)m^2+26(k-1)mn+7(k-1)n^2+(7-3k)m+(3k+1)n+3(k+1) clauses. C.13 Reduction Rule for Power Expression: Power(,k,)Power( a,k, c) The rule models the expression =k c= a^k (k∈ℤk ), where a and c are signed binary fixed-point numbers. The clauses generated by this rule are shown in Formula 124. ¬(k=0)∨¬cii=0,…,m+n,i≠m¬(k=0)∨cm¬(k=1)∨¬ai∨cii=0,…,m+n¬(k=1)∨ai∨¬cii=0,…,m+n¬(k=−1)∨Product(,,)¬(|k|>1)∨Power(,⌊|k|/2⌋,1)¬(|k|>1)∨Product(1,1,2)¬(|k|>1)∨¬(|k|mod2=1)∨Product(2,,3)¬(k>1)∨¬d2+(|k|mod2),i∨cii=0,…,m+n¬(k>1)∨d2+(|k|mod2),i∨¬cii=0,…,m+n¬(k<−1)∨Product(2+(|k|mod2),,) array[]l (k=0) c_i&i=0,…,m+n,i≠ m\\ (k=0) c_m\\ (k=1) a_i c_i&i=0,…,m+n\\ (k=1) a_i c_i&i=0,…,m+n\\ (k=-1) Product(\ a, c\, 1)\\ (|k|>1) Power( a, |k|/2 , d_1)\\ (|k|>1) Product(\ d_1, d_1\, d_2)\\ (|k|>1) (|k|mod2=1) Product(\ d_2, a\, d_3)\\ (k>1) d_2+(|k|mod2),i c_i&i=0,…,m+n\\ (k>1) d_2+(|k|mod2),i c_i&i=0,…,m+n\\ (k<-1) Product(\ d_2+(|k|mod2), c\, 1) array (124) where i d_i is an intermediate variable, 1 is the signed binary fixed-point encoding of number 1. When k=0k=0, this rule generates 0 intermediate Boolean variables and m+n+1m+n+1 clauses. When k=1k=1, this rule generates 0 intermediate Boolean variables and 2(m+n)+22(m+n)+2 clauses. When k=−1k=-1, this rule generates 2m2+4mn+32n2+2m+52n+42m^2+4mn+ 32n^2+2m+ 52n+4 intermediate Boolean variables and 13m2+26mn+m+7n2+m+7n+913m^2+26mn+m+7n^2+m+7n+9 clauses. When k>1k>1, this rule generates ⌊log2|k|⌋(2m+2n+2)+(∑i=2⌊log2|k|⌋(|k|mod2i))(2m2+4mn+32n2+2m+52n+4) _2|k| (2m+2n+2)+( _i=2 _2|k| (|k|mod2^i))(2m^2+4mn+ 32n^2+2m+ 52n+4) intermediate Boolean variables and ⌊log2|k|⌋(3m+3n+1)+(∑i=2⌊log2|k|⌋(|k|mod2i))(13m2+26mn+m+7n2+m+7n+9)+(1+(|k|mod2))(m+n+1) _2|k| (3m+3n+1)+( _i=2 _2|k| (|k|mod2^i))(13m^2+26mn+m+7n^2+m+7n+9)+(1+(|k|mod2))(m+n+1) clauses. When k<−1k<-1, this rule generates ⌊log2|k|⌋(2m+2n+2)+(∑i=2⌊log2|k|⌋(|k|mod2i))(2m2+4mn+32n2+2m+52n+4) _2|k| (2m+2n+2)+( _i=2 _2|k| (|k|mod2^i))(2m^2+4mn+ 32n^2+2m+ 52n+4) intermediate Boolean variables and (⌊log2|k|⌋−1)(3m+3n+1)+(1+∑i=2⌊log2|k|⌋(|k|mod2i))(13m2+26mn+m+7n2+m+7n+9)+(1+(|k|mod2))(m+n+1)+2(m+n)( _2|k| -1)(3m+3n+1)+(1+ _i=2 _2|k| (|k|mod2^i))(13m^2+26mn+m+7n^2+m+7n+9)+(1+(|k|mod2))(m+n+1)+2(m+n) clauses. C.14 Reduction Rule for Absolute Value Expression: Absolute(,)Absolute( a, c) The rule models the expression =|| c=| a|, where a and c are signed binary fixed-point numbers. The clauses generated by this rule are shown in Formula 125. ¬cm+n¬ai∨cii=0,…,m+n−1ai∨¬cii=0,…,m+n−1 array[]cl c_m+n\\ a_i c_i&i=0,…,m+n-1\\ a_i c_i&i=0,…,m+n-1\\ array (125) This rule generates 0 intermediate Boolean variables and 2m+2n+12m+2n+1 clauses. C.15 Reduction Rule for Floor Expression: Floor(,)Floor( a, c) The rule models the expression =⌊⌋ c= a , where a and c are signed binary fixed-point numbers. The clauses generated by this rule are shown in Formula 126. ¬cii=0,…,m−1¬am+n∨cm+nam+n∨¬cm+n⋁i=0m−1ai∨d¬ai∨¬di=0,…,m−1¬d∨eam+n∨ed∨¬am+n∨¬e¬e∨¬ai∨cii=m,…,m+n−1¬e∨ai∨¬cii=m,…,m+n−1¬hme∨HalfAdder(ai,hi,ci,hi+1)i=m,…,m+n−1 array[]cl c_i&i=0,…,m-1\\ a_m+n c_m+n\\ a_m+n c_m+n\\ _i=0^m-1a_i d\\ a_i d&i=0,…,m-1\\ d e\\ a_m+n e\\ d a_m+n e\\ e a_i c_i&i=m,…,m+n-1\\ e a_i c_i&i=m,…,m+n-1\\ h_m\\ e HalfAdder(a_i,h_i,c_i,h_i+1)&i=m,…,m+n-1\\ array (126) This rule generates n+3n+3 intermediate Boolean variables and 2m+8n+72m+8n+7 clauses. C.16 Reduction Rule for Ceil Expression: Ceil(,)Ceil( a, c) The rule models the expression =⌈⌉ c= a , where a and c are signed binary fixed-point numbers. The clauses generated by this rule are shown in Formula 127. ¬cii=0,…,m−1¬am+n∨cm+nam+n∨¬cm+n⋁i=0m−1ai∨d¬ai∨¬di=0,…,m−1¬d∨e¬am+n∨ed∨am+n∨¬e¬e∨¬ai∨cii=m,…,m+n−1¬e∨ai∨¬cii=m,…,m+n−1¬hme∨HalfAdder(ai,hi,ci,hi+1)i=m,…,m+n−1 array[]cl c_i&i=0,…,m-1\\ a_m+n c_m+n\\ a_m+n c_m+n\\ _i=0^m-1a_i d\\ a_i d&i=0,…,m-1\\ d e\\ a_m+n e\\ d a_m+n e\\ e a_i c_i&i=m,…,m+n-1\\ e a_i c_i&i=m,…,m+n-1\\ h_m\\ e HalfAdder(a_i,h_i,c_i,h_i+1)&i=m,…,m+n-1\\ array (127) This rule generates n+3n+3 intermediate Boolean variables and 2m+8n+72m+8n+7 clauses. C.17 Reduction Rule for Maximum Expression: Max(1,2,⋯,k,)Max(\ a_1, a_2,·s, a_k\, c) The rule models the expression =maxi=1ki c= _i=1^k\ a_i\, where i a_i and c are signed binary fixed-point numbers. The clauses generated by this rule are shown in Formula 128. LessEqual(i,)i=1,…,kEnumerationDomain(,1,2,⋯,k) array[]clLessEqual( a_i, c)&i=1,…,k\\ EnumerationDomain( c,\ a_1, a_2,·s, a_k\)\\ array (128) This rule generates 3km+3kn+5k3km+3kn+5k intermediate Boolean variables and (21k+2)m+(17k+2)n+(9k+3)(21k+2)m+(17k+2)n+(9k+3) clauses. C.18 Reduction Rule for Minimum Expression: Min(1,2,⋯,k,)Min(\ a_1, a_2,·s, a_k\, c) The rule models the expression =mini=1ki c= _i=1^k\ a_i\, where i a_i and c are signed binary fixed-point numbers. The clauses generated by this rule are shown in Formula 129. LessEqual(,i)i=1,…,kEnumerationDomain(,1,2,⋯,k) array[]clLessEqual( c, a_i)&i=1,…,k\\ EnumerationDomain( c,\ a_1, a_2,·s, a_k\)\\ array (129) This rule generates 3km+3kn+5k3km+3kn+5k intermediate Boolean variables and (21k+2)m+(17k+2)n+(9k+3)(21k+2)m+(17k+2)n+(9k+3) clauses. C.19 Reduction Rule for Integer Domain: IntegerDomin(,L,R)IntegerDomin( a,L,R) The rule declares that the domain of a is defined as ∈ℤ a and L≤RL≤ a≤ R, where a is a signed binary fixed-point number, L and R are constant integers(L<RL<R). The clauses generated by this rule are shown in Formula 130. ¬aii=0,…,m−1¬(k1>0)∨¬am+n¬(k2<0)∨am+n¬(L=0)∨¬am+n∨¬aii=m,…,m+n−1¬(R=0)∨am+n∨¬aii=m,…,m+n−1¬aii=m,…,m+n−1,2i−m>max|k1|,|k2|¬(L≠0∧|L|<2n−1∧|L−1|≠2⌈log2max|L|,|R|⌉)∨LessEqual(,)¬(R≠0∧|R|<2n−1∧|R+1|≠2⌈log2max|L|,|R|⌉)∨LessEqual(,) array[]l@ -12eml a_i -120.00018pt&i=0,…,m-1\\ (k_1>0) a_m+n -120.00018pt\\ (k_2<0) a_m+n -120.00018pt\\ (L=0) a_m+n a_i -120.00018pt&i=m,…,m+n-1\\ (R=0) a_m+n a_i -120.00018pt&i=m,…,m+n-1\\ a_i -120.00018pt&i=m,…,m+n-1,2^i-m> \|k_1|,|k_2|\\\ (L≠ 0 |L|<2^n-1 |L-1|≠ 2 _2 \|L|,|R|\ ) LessEqual( L, a) -120.00018pt\\ (R≠ 0 |R|<2^n-1 |R+1|≠ 2 _2 \|L|,|R|\ ) LessEqual( a, R) -120.00018pt\\ array (130) This rule generates 4m+4n+64m+4n+6 intermediate Boolean variables and 33m+24n+8+max0,n−1−log2⌊max|L|,|R|⌋33m+24n+8+ \0,n-1- _2 \|L|,|R|\ \ clauses. C.20 Reduction Rule for Real Domain: RealDomin(,L1,R1,L2,R2)RealDomin( a,L_1,R_1,L_2,R_2) The rule declares that the domain of a is defined as ∈ℝ a , L1≤L2L_1≤ a≤ L_2, and L2<<R2L_2< a<R_2, where a is a signed binary fixed-point number, L1L_1, L2L_2, R1R_1 and R2R_2 are constant integers (maxL1,L2<maxR1,R2 \L_1,L_2\< \R_1,R_2\). The clauses generated by this rule are shown in Formula 131. ¬(L1>0∨L2≥0)∨¬am+n¬(R1<0∨R2≤0)∨am+n¬(L1=0)∨¬am+n∨¬aii=0,…,m+n−1¬(R1=0)∨am+n∨¬aii=0,…,m+n−1¬(L2=0∨R2=0)∨⋁i=0m+n−1ai¬aii=0,…,m+n−1,2i−m>max|maxL1,L2|,|minR1,R2|¬(L1≠0∧|L1|<2n)∨LessEqual(1,)¬(L2≠0∧|L2|<2n∧|L2|≠2⌈log2max|maxL1,L2|,|minR1,R2|⌉)∨LessThan(2,)¬(R1≠0∧|R1|<2n)∨LessEqual(,1)¬(R2≠0∧|R2|<2n∧|R2|≠2⌈log2max|maxL1,L2|,|minR1,R2|⌉)∨LessThan(,2) array[]l@ -18eml (L_1>0 L_2≥ 0) a_m+n -180.00027pt\\ (R_1<0 R_2≤ 0) a_m+n -180.00027pt\\ (L_1=0) a_m+n a_i -180.00027pt&i=0,…,m+n-1\\ (R_1=0) a_m+n a_i -180.00027pt&i=0,…,m+n-1\\ (L_2=0 R_2=0) _i=0^m+n-1a_i -180.00027pt\\ a_i -180.00027pt&i=0,…,m+n-1,2^i-m> \| \L_1,L_2\|,| \R_1,R_2\|\\\ (L_1≠ 0 |L_1|<2^n) LessEqual( L_1, a) -180.00027pt\\ (L_2≠ 0 |L_2|<2^n |L_2|≠ 2 _2 \| \L_1,L_2\|,| \R_1,R_2\|\ ) LessThan( L_2, a) -180.00027pt\\ (R_1≠ 0 |R_1|<2^n) LessEqual( a, R_1) -180.00027pt\\ (R_2≠ 0 |R_2|<2^n |R_2|≠ 2 _2 \| \L_1,L_2\|,| \R_1,R_2\|\ ) LessThan( a, R_2) -180.00027pt\\ array (131) This rule generates 62m+46n+20+max0,n−1−log2⌊max|maxL1,L2|,|minR1,R2|⌋62m+46n+20+ \0,n-1- _2 \| \L_1,L_2\|,| \R_1,R_2\|\ \ clauses and 8m+8n+108m+8n+10 intermediate Boolean variables. C.21 Reduction Rule for Enumeration Domain: EnumerationDomain(,1,2,⋯,k)EnumerationDomain( a,\ b_1, b_2,·s, b_k\) The rule declares that the domain of a is defined as ∈1,2,⋯,k a∈\ b_1, b_2,·s, b_k\, where a and i b_i are signed binary fixed-point numbers. The clauses generated by this rule are shown in Formula 132. ¬aj∨¬bi,j∨di,ji=1,…,k,j=0,…,m+naj∨bi,j∨di,ji=1,…,k,j=0,…,m+naj∨¬bi,j∨¬di,ji=1,…,k,j=0,…,m+n¬aj∨bi,j∨¬di,ji=1,…,k,j=0,…,m+n⋁j=0m+n¬di,j∨eii=1,…,kdi,j∨¬eii=1,…,k,j=0,…,m+n⋁i=1kei⋁i=1k¬bi,j∨ajj=0,…,m+n⋁i=1kbi,j∨¬ajj=0,…,m+n array[]cl a_j b_i,j d_i,j&i=1,…,k,j=0,…,m+n\\ a_j b_i,j d_i,j&i=1,…,k,j=0,…,m+n\\ a_j b_i,j d_i,j&i=1,…,k,j=0,…,m+n\\ a_j b_i,j d_i,j&i=1,…,k,j=0,…,m+n\\ _j=0^m+n d_i,j e_i&i=1,…,k\\ d_i,j e_i&i=1,…,k,j=0,…,m+n\\ _i=1^ke_i\\ _i=1^k b_i,j a_j&j=0,…,m+n\\ _i=1^kb_i,j a_j&j=0,…,m+n\\ array (132) where eie_i and di,jd_i,j are intermediate Boolean variables. This rule generates km+kn+2kkm+kn+2k intermediate Boolean variables and (5k+2)m+(5k+2)n+6k+3(5k+2)m+(5k+2)n+6k+3 clauses. C.22 Reduction Rule for the Normalization of Objective Value: Normalization(,)Normalization( a, c) The rule models the expression =+2n c= a+2^n, where a is a signed binary fixed-point number, and b is an unsigned binary fixed-point number. The clauses generated by this rule are shown in Formula 133. Complement(,(¬cm+n)cm+n−1⋯c0) array[]cl matrixComplement( a,( c_m+n)c_m+n-1·s c_0)\\ matrix array (133) This rule generates m+n+1m+n+1 intermediate Boolean variables and 8m+8n+58m+8n+5 clauses. Appendix D Detailed Comparison in Solution Quality Table 7: Comparison in Solution Quality (Part 1 of 3) Optimization Problem Instance The Objective Values of Solutions Optimal Solution GORED CPLEX Gurobi SCIP GA EA PSO Graph Coloring Problem [41] myciel3 4.0 4.0 4.0 4.0 4.0 4.0 4.0 7.0 myciel4 5.0 5.0 5.0 5.0 5.0 11.0 6.0 15.0 myciel5 6.0 6.0 6.0 6.0 6.0 32.0 23.0 32.0 queen5_5 5.0 5.0 5.0 5.0 5.0 13.0 12.0 19.0 queen6_6 7.0 7.0 7.0 7.0 7.0 29.0 21.0 29.0 queen7_7 7.0 7.0 7.0 7.0 7.0 44.0 35.0 44.0 queen8_8 9.0 9.0 9.0 9.0 9.0 59.0 51.0 57.0 anna 11.0 11.0 11.0 11.0 11.0 121.0 93.0 101.0 david 11.0 11.0 11.0 11.0 11.0 72.0 53.0 61.0 huck 11.0 11.0 11.0 11.0 11.0 63.0 36.0 53.0 jean 10.0 10.0 10.0 10.0 10.0 64.0 36.0 52.0 games120 9.0 9.0 9.0 9.0 9.0 107.0 92.0 94.0 miles250 8.0 8.0 8.0 8.0 8.0 118.0 80.0 88.0 Traveling Salesman Problem [42] burma14 3323.0 3323.0 3323.0 3323.0 3323.0 3406.0 3406.0 4011.0 ulysses16 6859.0 6859.0 6859.0 6859.0 6859.0 6919.0 6983.0 7569.0 ulysses22 7013.0 7013.0 7013.0 7013.0 7013.0 7073.0 7808.0 8896.0 gr17 2085.0 2085.0 2085.0 2085.0 2085.0 2158.0 2345.0 2751.0 gr21 2707.0 2707.0 2707.0 2707.0 2707.0 2775.0 3612.0 4382.0 gr24 1272.0 1272.0 1272.0 1272.0 1272.0 1326.0 1721.0 1875.0 fri26 937.0 937.0 937.0 937.0 937.0 1020.0 1149.0 1244.0 bayg29 1610.0 1610.0 1610.0 1610.0 1610.0 1644.0 2652.0 2416.0 bays29 2020.0 2020.0 2020.0 2020.0 2020.0 2073.0 3319.0 3244.0 dantzig42 699.0 699.0 699.0 699.0 699.0 713.0 1143.0 1011.0 swiss42 1273.0 1273.0 1273.0 1273.0 1273.0 1288.0 2770.0 2441.0 Capacitated Vehicle Routing Problem [43] E-n13-k4 247.0 247.0 247.0 247.0 247.0 256.0 247.0 278.0 E-n22-k4 375.0 375.0 375.0 375.0 375.0 375.0 462.0 467.0 E-n23-k3 569.0 569.0 569.0 569.0 569.0 570.0 720.0 791.0 P-n16-k8 450.0 450.0 450.0 450.0 450.0 450.0 465.0 471.0 P-n19-k2 212.0 212.0 212.0 212.0 212.0 212.0 236.0 266.0 P-n20-k2 216.0 216.0 216.0 216.0 216.0 216.0 268.0 295.0 P-n21-k2 211.0 211.0 211.0 211.0 211.0 211.0 255.0 283.0 P-n22-k2 216.0 216.0 216.0 216.0 216.0 216.0 259.0 276.0 Two-Echelon Vehicle Routing Problem [41] E-n13-k4-1 280.0 280.0 280.0 280.0 280.0 290.0 280.0 306.0 E-n13-k4-2 286.0 286.0 286.0 286.0 286.0 296.0 286.0 286.0 E-n13-k4-3 284.0 284.0 284.0 284.0 284.0 296.0 284.0 290.0 E-n13-k4-4 218.0 218.0 218.0 218.0 218.0 246.0 218.0 218.0 E-n13-k4-5 218.0 218.0 218.0 218.0 218.0 232.0 218.0 232.0 E-n13-k4-6 230.0 230.0 230.0 230.0 230.0 238.0 230.0 238.0 E-n13-k4-7 224.0 224.0 224.0 224.0 224.0 286.0 224.0 246.0 E-n13-k4-8 236.0 236.0 236.0 236.0 236.0 290.0 236.0 252.0 E-n13-k4-9 244.0 244.0 244.0 244.0 244.0 252.0 244.0 256.0 E-n13-k4-10 268.0 268.0 268.0 268.0 268.0 298.0 268.0 278.0 E-n13-k4-11 276.0 276.0 276.0 276.0 276.0 290.0 276.0 290.0 E-n13-k4-12 290.0 290.0 290.0 290.0 290.0 290.0 290.0 290.0 E-n13-k4-13 288.0 288.0 288.0 288.0 288.0 292.0 288.0 290.0 E-n13-k4-14 228.0 228.0 228.0 228.0 228.0 274.0 228.0 262.0 E-n13-k4-15 228.0 228.0 228.0 228.0 228.0 270.0 228.0 232.0 E-n13-k4-16 238.0 238.0 238.0 238.0 238.0 274.0 238.0 238.0 E-n13-k4-17 234.0 234.0 234.0 234.0 234.0 286.0 234.0 246.0 E-n13-k4-18 246.0 246.0 246.0 246.0 246.0 290.0 246.0 252.0 E-n13-k4-19 254.0 254.0 254.0 254.0 254.0 290.0 254.0 256.0 E-n13-k4-20 276.0 276.0 276.0 276.0 276.0 290.0 276.0 280.0 Table 8: Comparison in Solution Quality (Part 2 of 3) Optimization Problem Instance The Objective Values of Solutions Optimal Solution GORED CPLEX Gurobi SCIP GA EA PSO Multidimensional Knapsack Problem [41] mknap1-1 3800.0 3800.0 3800.0 3800.0 3800.0 3800.0 3800.0 3800.0 mknap1-2 8706.1 8706.1 8706.1 8706.1 8706.1 8706.1 8706.1 8706.1 mknap1-3 4015.0 4015.0 4015.0 4015.0 4015.0 4015.0 4015.0 3985.0 mknap1-4 6120.0 6120.0 6120.0 6120.0 6120.0 6120.0 6120.0 6000.0 mknap1-5 12400.0 12400.0 12400.0 12400.0 12400.0 12400.0 12400.0 12360.0 mknap1-6 10618.0 10618.0 10618.0 10618.0 10618.0 10604.0 10618.0 10531.0 mknap1-7 16537.0 16537.0 16537.0 16537.0 16537.0 16452.0 16519.0 16374.0 mknap2-11 4554.0 4554.0 4554.0 4554.0 4554.0 4554.0 4554.0 4527.0 mknap2-12 4536.0 4536.0 4536.0 4536.0 4536.0 4536.0 4536.0 4411.0 mknap2-13 4115.0 4115.0 4115.0 4115.0 4115.0 4115.0 4115.0 3985.0 mknap2-14 4561.0 4561.0 4561.0 4561.0 4561.0 4561.0 4561.0 4505.0 mknap2-15 4514.0 4514.0 4514.0 4514.0 4514.0 4514.0 4514.0 3870.0 mknap2-16 5557.0 5557.0 5557.0 5557.0 5557.0 5557.0 5557.0 5140.0 mknap2-17 5567.0 5567.0 5567.0 5567.0 5567.0 5567.0 5567.0 5331.0 mknap2-18 5605.0 5605.0 5605.0 5605.0 5605.0 5605.0 5605.0 5592.0 mknap2-19 5246.0 5246.0 5246.0 5246.0 5246.0 5246.0 5246.0 5164.0 mknap2-20 6339.0 6339.0 6339.0 6339.0 6339.0 6339.0 6339.0 6005.0 mknap2-21 5643.0 5643.0 5643.0 5643.0 5643.0 5643.0 5643.0 4955.0 mknap2-22 6339.0 6339.0 6339.0 6339.0 6339.0 6339.0 6339.0 5900.0 mknap2-23 6159.0 6159.0 6159.0 6159.0 6159.0 6159.0 6159.0 5862.0 Job-Shop Scheduling Problem [44] Ta01 1231.0 1231.0 1231.0 1231.0 1231.0 1757.0 1778.0 1549.0 Ta02 1244.0 1244.0 1244.0 1244.0 1244.0 1759.0 1744.0 1688.0 Ta03 1218.0 1218.0 1218.0 1218.0 1218.0 1711.0 1757.0 1554.0 Ta04 1175.0 1175.0 1175.0 1175.0 1175.0 1749.0 1762.0 1590.0 Ta05 1224.0 1224.0 1224.0 1224.0 1224.0 1778.0 1722.0 1663.0 Ta06 1238.0 1238.0 1238.0 1238.0 1238.0 1721.0 1764.0 1611.0 Ta07 1227.0 1227.0 1227.0 1227.0 1227.0 1768.0 1786.0 1629.0 Ta08 1217.0 1217.0 1217.0 1217.0 1217.0 1745.0 1775.0 1593.0 Ta09 1274.0 1274.0 1274.0 1274.0 1274.0 1758.0 1818.0 1705.0 Ta10 1241.0 1241.0 1241.0 1241.0 1241.0 1765.0 1811.0 1533.0 Open-Shop Scheduling Problem [44] Ta01 193.0 193.0 193.0 193.0 193.0 193.0 193.0 196.0 Ta02 236.0 236.0 236.0 236.0 236.0 236.0 236.0 245.0 Ta03 271.0 271.0 271.0 271.0 271.0 271.0 271.0 272.0 Ta04 250.0 250.0 250.0 250.0 250.0 250.0 250.0 255.0 Ta05 295.0 295.0 295.0 295.0 295.0 295.0 295.0 301.0 Ta06 189.0 189.0 189.0 189.0 189.0 189.0 189.0 209.0 Ta07 201.0 201.0 201.0 201.0 201.0 201.0 201.0 204.0 Ta08 217.0 217.0 217.0 217.0 217.0 217.0 217.0 229.0 Ta09 261.0 261.0 261.0 261.0 261.0 261.0 261.0 272.0 Ta10 217.0 217.0 217.0 217.0 217.0 217.0 217.0 221.0 Ta11 300.0 300.0 300.0 300.0 300.0 307.0 301.0 309.0 Ta12 262.0 262.0 262.0 262.0 262.0 267.0 264.0 277.0 Ta13 323.0 323.0 323.0 323.0 323.0 345.0 337.0 347.0 Ta14 310.0 310.0 310.0 310.0 310.0 321.0 312.0 336.0 Ta15 326.0 326.0 326.0 326.0 326.0 335.0 332.0 360.0 Ta16 312.0 312.0 312.0 312.0 312.0 323.0 321.0 361.0 Ta17 303.0 303.0 303.0 303.0 303.0 319.0 308.0 314.0 Ta18 300.0 300.0 300.0 300.0 300.0 310.0 301.0 316.0 Ta19 353.0 353.0 353.0 353.0 353.0 363.0 366.0 389.0 Ta20 326.0 326.0 326.0 326.0 326.0 346.0 331.0 361.0 Quadratic Assignment Problem [45] esc16d 16.0 16.0 16.0 16.0 16.0 16.0 16.0 16.0 esc16e 28.0 28.0 28.0 28.0 28.0 30.0 28.0 32.0 esc16f 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 esc16g 26.0 26.0 26.0 26.0 26.0 26.0 26.0 26.0 esc16i 14.0 14.0 14.0 14.0 14.0 14.0 14.0 14.0 esc16j 8.0 8.0 8.0 8.0 8.0 8.0 8.0 8.0 esc32e 2.0 2.0 2.0 2.0 2.0 2.0 2.0 2.0 esc32g 6.0 6.0 6.0 6.0 6.0 6.0 6.0 6.0 Table 9: Comparison in Solution Quality (Part 3 of 3) Optimization Problem Instance The Objective Values of Solutions Optimal Solution GORED CPLEX Gurobi SCIP GA EA PSO Shifted Sphere Function [46] sphere10 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 sphere20 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 sphere30 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 sphere40 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 sphere50 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 sphere60 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 sphere70 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 sphere80 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 sphere90 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 sphere100 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -438.3 Shifted Schwefel’s Problem [46] schwefel10 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 -450.0 schwefel20 -450.0 -450.0 -450.0 -450.0 -450.0 -449.1 -450.0 -450.0 schwefel30 -450.0 -450.0 -450.0 -450.0 -450.0 -445.2 103.6 -450.0 schwefel40 -450.0 -450.0 -450.0 -450.0 -450.0 -441.4 8233.4 -450.0 schwefel50 -450.0 -450.0 -450.0 -450.0 -450.0 -412.6 32025.9 -434.1 schwefel60 -450.0 -450.0 -450.0 -450.0 -450.0 -189.9 58776.7 954.3 Shifted Rosenbrock’s Function [46] rosenbrock10 -390.0 -390.0 -390.0 -390.0 -390.0 -367.0 -390.0 -368.3 rosenbrock20 -390.0 -390.0 -390.0 -390.0 -390.0 -318.6 -380.1 -364.4 rosenbrock30 -390.0 -390.0 -390.0 -390.0 -390.0 -269.4 -364.4 -376.5 rosenbrock40 -390.0 -390.0 -390.0 -390.0 -390.0 -305.7 -355.8 -364.9 rosenbrock50 -390.0 -390.0 -390.0 -390.0 -390.0 -178.3 -344.2 -304.9 rosenbrock60 -390.0 -390.0 -390.0 -390.0 -390.0 -304.4 -334.4 510.9 rosenbrock70 -390.0 -390.0 -390.0 -390.0 -390.0 -164.1 -326.8 -207.2 rosenbrock80 -390.0 -390.0 -390.0 -390.0 -390.0 -105.1 -315.0 -245.1 rosenbrock90 -390.0 -390.0 -390.0 -390.0 -390.0 -212.9 -306.1 371.8 rosenbrock100 -390.0 -390.0 -390.0 -390.0 -390.0 -232.3 -297.7 -242.6