Suggesting Variable Order for Cylindrical Algebraic Decomposition via Reinforcement Learning
Authors: Fuqi Jia
Yuhang Dong
Minghao Liu
Pei Huang
Feifei Ma
Jian Zhang
Venue: NeurIPS 2023 poster (2023)
Keywords: Reinforcement Learning
Graph Neural Network
Cylindrical Algebraic Decomposition.
TL;DR: This paper proposes two novel RL approaches combined with GNNs for Suggesting Variable Order for Cylindrical Algebraic Decomposition.

Abstract: Cylindrical Algebraic Decomposition (CAD) is one of the pillar algorithms of symbolic computation, and its worst-case complexity is double exponential to the number of variables. Researchers found that variable order dramatically affects efficiency and proposed various heuristics. 
The existing learning-based methods are all supervised learning methods that cannot cope with diverse polynomial sets.
This paper proposes two Reinforcement Learning (RL) approaches combined with Graph Neural Networks (GNN) for Suggesting Variable Order (SVO). One is GRL-SVO(UP), a branching heuristic integrated with CAD. The other is GRL-SVO(NUP), a fast heuristic providing a total order directly. We generate a random dataset and collect a real-world dataset from SMT-LIB. The experiments show that our approaches outperform state-of-the-art learning-based heuristics and are competitive with the best expert-based heuristics. Interestingly, our models show a strong generalization ability, working well on various datasets even if they are only trained on a 3-var random dataset. The source code and data are available at https://github.com/dongyuhang22/GRL-SVO.

Suggesting Variable Order for Cylindrical Algebraic Decomposition via Reinforcement Learning
Fuqi Jia!.3", Yuhang Dong 3", Minngho Liul.3 Pei Huang'. Feifei 2a and Jian Zhang!.3+
SSttt Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
2 Laboratory of Parallel Software and Computational Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
University of Chinese Academy of Sciences, Beijing, China *Stanford University, Stanford, USA
{jiafq, liumh, wwlummmmfff...... maffs /..os..ccccc.. ac cn, dongyuhang220maill 1s. www.uuc.c................. cn, @hangee@@ttanfod.ccm edu
Abstract
Cylindrical Algebraic Decomposition (CAD) is one of the pillar algorithms of symbolic computation, and its worst-case complexity is double exponential to the number of variables. Researchers found that variable order dramatically affects efficiency and proposed various heuristics. The existing learning carning-based methods are all supervised learning methods that cannot cope with diverse polynomial sets. This paper proposes two Reinforcement Learning (RL) approaches combined with Graph Neural Networks (GNN) for Suggesting Variable Order (SVO). One is GRL-SVO(UP), branching heuristic integrated with CAD. The other is GRL- SVO(NUP), a fast heuristic providing total order directly. We generate random dataset and collect real-world dataset from SMT-LIB. The experiments show that our approaches outperform state-of-the-arr soarning-basee heuristics and are competitive with the best expert-based heuristics. Interestingly, our models show a strong generalization ability, working well on various datasets even they are only trained on 3-var random dataset. The source code and data available
Introduction
As learned in school, we know how to answer the question of whether a quadratic equation for x has a real root. For example,
ba + = 0,
where b, unknowns. We answer it by checking whether the discriminant is non-negative,
ie., 82 - 4c 2 0. What if the number and degree variables increase, and the formula involves the combination of the universal quantifier (V), existential quantifier (3), and logical operators (and(A), or(V), not(-))? Checking whether polynomials satisfy some mathematical constraints is difficult problem and has puzzled mathematicians since ancient times. Until the 1930s, Alfred Tarski (I] answered the question by proving that the theory of real closed fields admits the elimination of quantifiers and gives a quantifier elimination procedure. Unfortunately, the procedure was impractical due to its non-clementary complexity. In 1975, George Collins discovered the first relatively efficient algorithm, Cylindrical Algebraic Decomposition (CAD) (2] Currently, CAD (and variants) has
'These authors contributed equally.
Cooresponding authors.
37th Conference on Neural Information Processing Systems (NcurIPS 2023).

---

(a) x <
(b) x x
(c) y -
Figure 1: Examples of CAD. Figure la shows cells of {y x²). Figure 1b and Ic are CAD with different variable orders on {x y + 4x zy. -x 2xy 1).
become one of the most fundamental algorithms in symbolic computation and is widely used in computational geometry 3 robot motion planning constraint programming 6
7
More precisely, CAD an algorithm that eliminates (technically called preject) variables one by one and finally results in list of regions that are sign-invariant to the polynomials (technically called cells). CAD provides an efficient quantifier climination in real space, thereby enabling the solution of various problems related to polynomials. For example, the space of the discriminant of the quadratic equation (i.e., b² 4c 2 0) can be the combination of satisfied cells. We provide a detailed description in Appendix [ Due its powerful analytical ability and great versatility, it is also accompanied by huge limitations. The theoretical worst complexity is double exponential to the number of variables
Researchers have conducted in-depth studies on improving efficiency. According to theoretical and practical research, there lives very important conclusion that "variable order in CAD can be crucially important"
10 [2 [3 15 [6]. The selection variable orders has a great effect on the time, memory usage well as the number of cells in CAD. As example, (8] introduces category of problems where one variable order leads to a result with double exponential complexity to the number of variables, while another order yields a constant-sized result.
8 9
In this paper, we present Graph- Reinforcement Learning for Suggesting Variable Order (GRL-SVO) approach for CAD. It has two variants: GRL-SVO(UP) (i.e., utilizing project) and GRI-SVO(NUPP) (i.e., not utilizing project). GRI-SVO(UP) is integrated into the CAD and can select the "best" next projecting variable. Considering the high cost of interacting with the symbolic computation tool, we also propose a fast approach transition (i.e., project) via two rules (update rule and delete rule). It can report total variable order before the CAD process. To evaluate the effectiveness the models, we conduct a dataset of random polynomial sets with to 9 variables and collected instances from SMT-LIB 1 17 to form a real-world dataset. Experimental results show that our approaches outperform state-of-the-an learning- based heuristics and are competitive with the best expert-basee heuristics. GRL-SVO also exhibits a strong generalization capability. The models are only trained on a 3-var random dataset, but they still work well other datasets.
which will simulate the state
2 Background and Related Work
In this section, we briefly introduce some basic definitions of CAD 2 works of SVO and give an overview of the techniques used.
18 We classify the previous
2.1 Cylindrical Algebraic Decomposition (CAD)
A Cylindrical Algebraic Decomposition (CAD) is a decomposition algorithm of set of polynomials ordered R" space resulting in finite sign-invariant regions, named cells. As shown Figure there are 3 cells with different colors (two infinite regions and the curve), and any points in the cell lead to the same sign of y x². Let R[x] be the ring of polynomials the variable vector [1, In] with coefficients in R [9]

---

Definition (Cell), For any finite set Q S R(x),, cell of Q is defined as maximally connected set in I" where the sign of every polynomial in Q is constant.
CAD accepts set of polynomials and fixed variable order and mainly consists of three running phases: project, root isolate, and lift. The project phase eliminates a variable of a polynomial set once at time. It will result in a new projected polynomial set that carries enough information to ensure possible decomposition. After repeating calls to project, CAD constitutes step-like like (from n-l variables to variable) set of projected polynomials. The root isolate procedure isolates all roots of the univariate polynomial set, and the roots split I into some segmentations. The lift phase samples in the segmentations and assigns the sampled value to the former projected polynomial set so that the former polynomial set will become univariate polynomial set. After repeating rool isolate and lift n --11 times, CAD reconstructs the entire space via set of cells characterized by the sample points. Since the CAD process and the project operators are not prerequisites understand our approach, we arrange more details in Appendix A Here, we exemplify the process and the effect of different variable orders.
Example 2.1. Consider polynomial set {x²y + 4x² + zy, -2² + 2xy-xxaz - 1} as in Figure Iband Ic
CAD process. Assume that the variable order is x x y. CAD eliminates y first and results in a polynomial set {z, x² + 1, 1, + 10x² + 1} (i.e., project phase). The polynomial set has only one root x = 0 (i.e., root isolation phase). Then R will be split into three segmentations: {a < 0. 0, 0}. We sample {x -5, 0. 5] and result in three different polynomial sets: (-100y + 100,- - 10y- 26), {-1), and {130y + 100, 10y
26} (i.e. lift phase). ) Let's take
the first polynomial
as an example, and it has two roots, ie., { 13 (i.e., root isolation phase).
Then I will be split into five segmentations: {
13 y
13
5 < y < 13 y 13.3 y > T33. ingn-invariant region, the whole
10
As shown in Figure| Tb the sample red point 15, 4) can represent
shaded area (i.e., x + 4x² + ry < ~ -2² + 2zy - 1< 0 AZ < 0).
Effect of different variable orders. Figure L eliminates then x and results in 13 cells, and Figure Tc first eliminates x then y and results in 89 cells, almost seven times that of the former.
2.2 Suggesting Variable Order for Cylindrical Algebraic Decomposition
An Expert-Based (EB) heuristic is a sequence of meticulous mechanized rules. It is mainly derived from theoretical analysis or large number of observations practical instances and summarized by experts. The heuristics can capture the human-readable characteristics of the problem. A Learning- Based (LB) heuristic will suggest an order through the scoring function or variable selection distribution given by the learning model. It can exploit features deep inside the problem statement via high-dimensional abstraction.
Another important indicator is whether invoking project, as the project phases are time-consuming for SVO heuristics in practice. In the following, UP denotes heuristics utilizing project, and NUP denotes hcuristics not utilizing project.
EB & UP. The heuristics sotd (sum of total degree) [00], and ndrr (number of distinct real roots) 12 will project utilizing all different variable orders until the polynomial sets with only one variable. Then sord will select the order with the smallest sum of total degrees for each monomial, while ndrr will select the order with the smallest number of distinet real roots. Because of the combinatorial explosion of orders, the heuristics projecting all orders only work on the case with a small number of variables. Based on CAD complexity analysis, gmods [13 selects the variable with the lowest degree sum in the polynomial set after each project phase.
EB & NUP. The heuristics brown g and triangular [I]] introduced series of rules about statistical features like degree, total degree, and occurrence to distinguish the importance of variables. The heuristic chord [14] also provides an efficient algorithm based on the associated graph. It makes variable order via perfect elimination ordering on the graph. Note that chord heuristic only works on the chordal graph. is a special case that, after each project phase, the graph only removes the linked edges of the projected variable without changing the other components.
LB & UP. To the best of our knowledge, no heuristic should be classified into this category.
IB & NUP. The approach EMLP [5] utilizes an MLP neural network. The network takes the selected statistics of the polynomial set input and outputs label for variable order directly. If the
3

---

polynomial set has 3 variables, then 3! 6 output labels are necessary for the neural network. The approach PVO [16] combines neural network and EB & NUP heuristies like brown and triangular. The neural network is trained to predict the best first variable while the EB & NUP heuristics decide other parts of orders. These kinds of heuristics work on variables most in their experiments.
According to the classification, our proposed approaches, GRL-SVO(UP) and GRL-SVO(NUP), can be categorized as LB & UP and LB & NUP, respectively.
2.3 Graph Neural Network and Reinforcement Learning
Graph Neural Networks (GNNs) are a class of deep learning models for graph-structured data. GNNs include many variants according to the characteristics of the problems, such as GCN [19] GAT 20). superGAT [21], and so on. Reinforcement Learning (RL) is an advanced machine learning paradigm where an agent learns make decisions by interacting with its environment. It includes various frameworks, such as REINFORCE 222 DQN 233, and so on. By leveraging the expressive power of
GNNs to learn complex graph structures and the adaptability Reinforcement Learning (RL) to find optimal maaiing policies, researchers have remarkably succeeded in combinatorial algorithm design [24 25 26]. GRL-SVO based on an Advantage Actor-Critic (A2C) framework 24 27
with Graph Network (28)
3 Method
This section starts with the problem formulation for the framework, followed by an overview and description of the graph representation and architecture. Finally, we introduce the state transition without project, which is the key technique for GRL-SVO(NU)),
3.1 Problem Formulation
We now give the formulation of SVO for CAD. Our goal is to improve CAD efficiency by suggesting better variable order. Computation time and memory usage are important indicators, but they will be affected by random factors, such as CPU clock, usage rate, etc. As the main output of CAD, cells can be the best candidate. In order to measure the quality of the result, the number of cells is an appropriate indicator that intuitively shows the effect of CAD [29]. In theory, large number of cells means that the partitions are fragmented compared to small number of cells. Usually, the polynomial set generated from project phase is complex and difficult for the next phases of CAD. In practice, the number of cells also strongly correlates the computation time and memory usage. Figures of the relation are listed in Appendix B and we found that the computation time and memory usage increase when the number of cells increases. The objective to minimize the number of cells N N(Q, o), where Q C RR [c] is a polynomial set with coefficients in R and is the given variable order, i.c., min (Q,
By analyzing the input polynomial set Q, we can derive the variable order so that we ought to minimize the objective:
min N(Q,
The difficulties of this framework mainly come from two aspects:
Huge input space. The expression of polynomial compressed, and any slight change in form (such as power) will change the geometric space drastically. The EB heuristics may become inefficient when encountering characteristies beyond the summarized patterns.
Huge output space. The number of variable orders and the number of variables have factorial relationship. i.c., variables resulting in n! different variable orders. For example, variables lead 3628800 candidate variable orders. sotd like, ndrr-like, and EMI-P-like heuristics become impractical due to the vast number of candidate variable orders.
3.2 GRL-SVO Overview
In this paper, considering the challenges mentioned above, we propose the GRL-SVO approach, and Figure 2 shows the overall architectures. For huge input space, compress the polynomial

---

(wtt Synbolyi Corpuctticn Toel)
(wicbaal Sprateli Comprtaaii Toxl)
Endeowmnn
Deltte
Preedted PobaenaiiSei
Updare
Acto
CNN
IPy )
CNN
(FAX)
(a) GRL-SVO((P)
(b) GRL-SVO(NUP)
The architecture GRL-SVO(UP) and GRI-SVO(NUP) where ((,2)) ML.P(CONCAT(- for updating the embedding for the neighbours of x. The dashed lines represent that will be only utilized in training mode.
Figure
information into an associated graph [30] with embeddings, which is simple and can depict the relationship between variables. For huge output space, utilize the neural network to predict the next best variable, and by repeating until no variables are left, the trajectory corresponds to a variable order. In detail, the actor neural network provides distribution of actions, i.e., the choice of variables. The critic neural network scores the total order and stabilizes the training process as state-dependent baseline. GNN encodes each variable of the current state as high-dimensional embedding, and additional neural network components transform them into our policy. As for transformation, GRL-SVO(UP) and GRL-SVO(NUP) environment of GRL-SVO(UP) projects the selected variable and reorganizes the total graph, while that (NUPS))(NU)) updates the graph via the update rule and delete rule.
different in utilizing project. The
3.3
Graph Representation
The graph of a polynomial set can different. We introduce a graph structure that can reflect the coupling relationship between variables.
Definition 2 (Associated Graph (30).. Given a polynomial set F, and the variable set of F, var(F), associated graph Gr E) of F is undirected graph, where E {(1;, 2;)
F, D., Zz E var(f))
In other words, if two variables appear in the same polynomial, they will have an edge.
GNNs have invariance permutations and awareness of input sparsity 3I 32 33].
The strength
similarly applies to our work. The associated graph is pure and simple, which only retains information related to variables and "neighbors" in the same polynomial. Note that such graph can easily become a complete graph. For example, I + 222 + 33 + I4 corresponds to complete associated graph. So, we need to distinguish nodes via rich embeddings. detailed in Appendix B The embeddings are proposed based on former research [16] (34] and our observations. The embedding vectors of variables will be first normalized via the z-score method, i.c..
[x] -mean( (epcan((FF)) ( [w]))
[x]
, var (varFF),
std({E,(u1))
where Fo is the corresponding polynomial set and E, [xr denotes the j-th scalar of the original embedding of variable
The graph representation a tuple AF, X²) where A E {0, 1]nx= is the adjacency matrix of the associated graph and X E Raxd a normalized node embedding matrix for variables.
To encode the representation, we utilize stack of k GNN layers, Formula (5.7) in 28 The process encodes the representations X [0)+ x In 1]] via
X [u] = (Xx(m)) -0 og
Σ
X
Ø bibia))
vEA(u)
where oi se and 0i nenggh trainable parameter matrices in R # and denotes the activation
function. 0r bias is the trainable bias term in di Hi+1 and N (u) is the set of neighbours of variable
5

---

2. H' is the dimension of hidden channels, and H = d. The layer will aggregate the local information of variables and update the embedding sequentially. Finally, we obtain the internediate tuple (F*, X*).
3.4
Architecture
3.4.1
Markov Decision Process (MDP)
State Space and Action Space. GRL-SSVOUPPNUP will suggest variable order for any polynomial set. The state space includes the graph representation of any polynomial set, i.e., S= (G (F), 10 x) Although it is very large space, the state provides sufficient statistics to evaluate actions. Action corresponds to candidate variable to project. For given state the action space is A var(Fa) where F. denotes the polynomial set of current state s.
Environment. At the time t, the environment of GRL-SVO(UP) takes current state and selected variable (action a²) as input and outputs set of CAD. That of TRL-SVO(NUP only removes the selected variable and linked edges from the current state s and updates embeddings via neural networks, which is detailed in Section 3.5
state s'~1 via processing the projected polynomial
Reward. The number of cells is sufficient reflect the impact of variable order on efficiency. R(ars²) -F
oo / denotes the reward for a given variable order under the initial state s" ie., the negative number of cells divided by a static normalization factor M. If the order leads to running timeout and cannot obtain the number of cells, R(o (() -1 directly. The reward of agent policy will increase as the training progresses.
3.4.2 Neural Network Architecture
Neural Network. The actor network 0g Rxd + IR" combines an MLP and softmax layer that transforms the X₁ of s the action distribution time t. The action obeys the distribution, i.e.,
a' ~ O2 (X(t) sofftmao(MTPP(XX))
The critic network 0g Rund + R is a combination of MeanPool and MLP layers, where MeanPool : Raxd + Rd. The critic value is defined as
O (x M MMP
Training, The parameters of GRL-SVO {0g: Oa, 0c} will go through an end-to-end training process via stochastic gradient descent method. Given initial state s, we aim learn the parameters of stochastic policy (als), which assigns high probabilities to order with small number of cells and low probabilities order with a large number of cells. Our neural network architecture uses the chain rule to factorize the probability of a variable order a as po(ass)
II= (a'1s, o²*), where (o(a"l [s, <tt) 9a (X²) is current action distribution. o² is the t-th element in the variable order and is the partial order from of -²-1, The training objective the expected reward, which is defined as J s0 Eo R(als).
Through the well-known REINFORCE algorithm
35 the gradient of the training objective is (eJ(0) s) (l -()o-=(())) Volggpp(o)))
where c(s) (x5)) is the predicting critic value.
Through Monte Carlo sampling, we obtain i.i.d polynomial sets corresponding states $1. $2, :.. SN ~ S, and N variable orders ~ po(-ss;). So we update the parameters of neural networks via
0a 0₂
(R(a))s)) cl Volooooooos)))
N
N
1
0. - 0e
+
(R(a,ls)- Vo(cs))
N
Inference. inference time, we generate an order greedy selection. For the i-th element the order a, we select the variable with the maximal probability, i.c., arg max (p(x)s, =()),

---

where V = var (ar(FF)-s) is the set of variables that have not been projected at time t. After selecting variables times, we obtain the total order o.
3.5 State Transition without Project
We provide an LB & NUP heuristic to free from interaction with the symbolic computation tools. It simulates the project via a neural network for embedding transformation and delete rule.
X2
X1
X2
As an example, Figure shows a specific case of state transition. The polynomial set changes after project phase the variable T4. where 307=4
(a)
(b)
Figure 3: The associated graph of { 4.3rs
4x -1 is reduced to +1 11,11111200
12r₂ + 3afar 4x 1] Figure 3a Assume
-1 +1+1,a +f without T4 while the polynomial 29 4r3.33 + 12z2 +3 remains unchanged. So, the embedding of neigh- bors of 24, i.e., 21,, will change greatly while that of other variables will change slightly. Besides, the projected variable should also be removed from the associated graph. Based on the aforementioned inspiring situations, we propose two rules for approximately simulating project.
31 (21-1,
that we select x4 to project, it results x - 12. +3) 1, - - + 1, + .ं
1,
and the associated graph is shown in Figure 3b
At time 1, assume z; is the next projecting variable. We mainly consider the projected variable's influence on its 1-hop neighbor variables.
Update Rule. We update the embedding X without project for other variables Iy via
Φ1 (6((a))) [xy]"=1 X(x;](=1),
A|m][=a]]11 otherwise,
X[x,]' x
X [1;)] 18-1
where o(a, = MLP(CONCAT((..))) b)) is the neural network that simulates the project for embedding transformation.
Delete Rule. It will trivially remove a; and edges linked to x; and update A, the state correspondingly.
t RemoneRowColumee (X, Mop(a;)),
Map(x.)),
X <- RemoveRow (X,
Mup(ι;) + (1,(a,))11,i44
where the function Map(x) V > N. maps the variable to the index in matrix and X, the operation Remove ConoounoooCluumn A, Mop(z;)) removes the row and column of variable x; from A, and the operation Reeooeeoow X, . Map(x.) (I)) removes the row of variable z; from X.
After such transitions, the state will feed the model defined by Section 3.4 and obtain the next projecting variable. After calling the model times, the trajectory corresponds variable order suggested by GRL-SVO(NUP).
Experiments
4.1 Setup
Implementation and Environments. We utilized PyTorch Geometric 33 for implementations of our approach. The hyper-parameters are listed in Appendix We utilized the NVIDIA Tesla V100 GPU for training. After the heuristics output the variable order, all instances with the given variable order are run with MAPLE 2018 on an Intel Xeon Platinum 8153 CPU (2.00GHz). The run-time limit is 900 seconds, and the time to predict variable order is also counted.
Dataset. We utilize two CAD datasets: random and LIB.LIB. The detailed parameters of random generation and collecting methods for SMT-LIB are presented in Appendix B
The random dataset contains 7 categories from 3-var to 9-var. We generate 20000 3-var instances and split them into training, testing, and validation sets in a ratio 8:1:1. We pre-run all 3!- variable orders and remove non-conforming instances where some variables are eliminated due to random
7

---

-015
(a)
(b)
(c)
Figure 4: The performance of all heuristics. Figure 4a and 4b correspond to the training phase, and the horizontal lines represent the timeout instances of corresponding heuristics on the training set. Figure 4c the PT graph over number variables.
O; remove the instances that are all timeout under 6 orders. The rest sets have 14990, 1871, and 1887 instances, respectively. The other categories contain 1000 instances. They are generated by randpoly of MAPLE. We also collect SMT-LIB dataset where there are from v-r to 9-var instances with numbers (5908, 1371, 131, 123, 318, 41, 24].
generation, for example,
Baselines. We compare our approach with two kinds of state-of-ther art heuristics, UP or NUP. For UP, we compare our approaches with sotd and ndrr implemented in the ProjectionCAAD package 37 Besides, we also implement gmods [13 in MAPLE. For NUP, we compare our approaches with brown, and triangular implemented in the RegularChains package [38]. EMLP approach proposed by England (15) and its implementation only supports 3-var instances. PVO(brown) and PVO(triangular) are PVO approaches combined with EB & NUP heuristics, brown and triangular, respectively. The provided implementations [16 only support 4,5,6-var instances.
Criterion. Assume T and denote the running time and number cells. AVG.T and AVG.N denote the average of T and N. If an instance runs timeout, we count the maximum time (900 seconds) and the maximum number of cells of this instance solved by other heuristics into the calculation. We remove the instances that all heuristics lead to CAD timeout, as such instances can not distinguish the ability of heuristies. PT and #SI denote the variable order prediction time used by heuristics and the number of solved instances within the time limit. For UP heuristics, PT also takes project time into consideration. Except for #SI, the criteria are the smaller, the better.
We conduct three experiments to evaluate our approaches. First of all, we only train the models on the 3-var random dataset. Then, we generalize the trained models on random datasets with up to 9 variables and the SMT-LIB dataset. Finally, we compare GRL-SVO(UPP and GRL-SVO and discuss different application scenarios. We list ablation experiments Appendix [ investigating the effect of features (of the initial embedding). network size, network structure, reward normalization factor M, GNN architecture, and coefficient. We also list additional results in Appendix D including results under other criteria and performance of fine-tuning.
Experiments.
4.2 Results
Training GRL-SVO. Figure 4a and Figure 4b show the performance during training with the instances in the training set. GRL-SVO outperforms the other heuristics through training and shows a rapid performance improvement. The UP heuristics are better than the NUP heuristics. The inference can be more accurate because the UP heuristics obtain more information than the NUP heuristics. In the beginning, GRL-SVO(NUP) with the random initial parameters is better than GRL-SVO(UP). After training, GRL-SVO(UP) shows better performance.
Generalization. We only train on the 3-var dataset and generalize the models to the other datasets. After removing all timeout instances, there are 1876, 651, 416, 354, 349, 409, and 383 instances for the random dataset from 3-var to 9-var; for the SMT-LIB dataset, 1777, 387, 17 instances for 3-var, 4-var to 6-var and 7- to 9-var, respectively. Table shows the performance
all heuristics, and the best scores are bolded. GRL-SVO(UP) is the only LB approach with UP heuristics, achieving the best performance among most UP and NUP heuristics except for the 4-var category. GRL-SVO(NUP) also achieves competitive performance compared to other NUP heuristics. GRL-SVO also shows
8

---

Table 1: The performance of all heuristics, The dash "_ indicates that the method does not support the category.
Calegodies
SLP
EB
LM
LM
misspaior
P1D PHOliiimplari
GRL-SVONUUP)
snid
gread
GRL-SHONEIP)
1772
1784
1693
1owetooot)
128.0
AVE.N
2427.34
2669.67
2166.67
2149:07
2195.80
2009.68
757
415
175
401
102
483
K25
255
311
3T5
4
AVG. T
152,87
394.71
360.33
376,71
314.57
85.12
2M2.06
215.48
191.45
AVG.N
5241.95
S565.00
63
S582.45
5131.40
3925.28
4248.45
4640. 18
4764.33 55
#81
236
302
242
218
258
43
27
329
346
4FG.1
454.2
474.77
418
46545
420
817.67
851.55
21
317.79
NVE.N
12300.70
13224,18
11795.00
12555.82
12590.49
14538669
14845.67
10466.79
9744,58
AVG.T
50L.75
552.14
400.73
527,86
439.02
169
254.40
214.55
AVG.N
2069900
33440.23
20181.56
19280.97 57
19300.07
253066 50
23539 10
17561.
16715.20
881
163
115
153
270
297
7/var
AVG.T
148.55
651.55
552
957.75
5M7.79 TV
313.73
345.57
AVG.Y
27700.1
23705.70
27300.05
36452.64
304.6.33 51
24465-99 59
23452 30
831
171
172
110
315
S-var
4
601.90
654,20
597.09
950,00
003.00
372.34
332,00
49112.02
AVG.T
665.41
690029
625.09
900.00
500,00
431.11
374.7H
AVG.N
45275.67
40631.78
469666.0
52173.03
$2175.00 01
42594 25
42270.91
#57
1770
1Td
1075
1756
1150
1283
1772
1773
SMT-LIB (3-var)
4V2.7
20.33
23.68
$3.00
22.36
34.38
65.10
18.32
18.53
AVG.N
6469.79
N00 a6
7000.07
4104.43 43
1472.11
4160175
2675.22
3500 84
837
TGi
150
3TV
379
37V
SMI-LIB (4-var 6-Na))
4VE.7
86,00
99:95
85.32
35,98
DIL1T
105.18
142.32
59.96
67.51
11
SMTLLIB vor
.VG.T
308,14
177.32
339
$41.53
588.33
260.3
329.91
.VG.N
53971,24
$9675,00 04
$1570,88
$1470.41
62185.82
50381.12
5631241
competitive performance in the real-world dataset, SMT-LIB dataset. Note that although the heuristics sotd perform better than GRL-SVO(UP) on the 4-var instances, they run timeout in most instances from 5-var due to the combinatorial explosion of the number of variable orders as shown in Figure 4c] The NUP heuristics take a short prediction time, and the polylines in Figure [4] For example, an instance with 7 variables leads 7! 5040 variable orders to project for sold and ndrr.
4.3 Discussion on GRL-SYO(UPINUP)
As in Table D GRL-SVO(UP)) performs better in #SI, A AVG.T, AVG.N compared to GRL- SVO(NUP). It is understandable because GRL-SVO(UP) receives more real-world information from the projected polynomial set at each step. As in Figure 4c GRL-SVO(NUP) is faster than GRL- SVO(UP). The inference time of GRL-SVO but there is an obvious increase of GRL-SVV((P)) As the number of variables grows, the time of project and interactions between GRL-SVO(UP) and symbolic computation tools will be critical. It is also the bottleneck of UP heuristics like GRL-SVO(UP), gmods, sotd, and ndrr. Therefore, the application scenarios corresponding to the two models will be different.
is almost unchanged with the increase of variables,
Internalizing GRL-SVO(UP) into the CAD process a promising option. As project is an algorithm component of CAD, internalization will help reuse the results of projection and reduce the interaction time. GRL-SVO(NUP) cheap and can extract information directly from polynomial representations. It might be applied to other tools that do not use the entire CAD process. As a canonical example, the automated reasoning tools like Z3 5 YICES2 (6. CVC5 utilize project partially only for generating lemmas when solving non- non-lineee linear arithmetic problems. At the beginning of solving, they also require a fixed variable order. For tasks that are time-critical and do not utilize full CAD in the solving process, GRL-SVO(NUP) seems to be better option.
Limitations
Our graph representation cannot embed complete information on polynomials. The associated graph simple and only shows the relationship between variables. Through selection, we conduct the embedding of graph nodes, but they still ignore plenty of minutiae information, for example, the distribution of coefficients. Besides, the lack of sufficiently large datasets is also a matter of urgency. We can generate large amounts of random data but may lack practical instances for training. Another slight limitation is the prediction time. Python and Py Torchh are both heavy techniques. The prediction time of GRL-SVO shown in Figure 4c is actually not much different from other heuristics.

---

Conclusion and Future Work
In the paper, we have proposed the first RL-based approach to suggest variable order for cylindrical algebraic decomposition. It has two variants: GRL-SVO(UP) for LB & UP and GRL-SVO(NUP) for LB & NUP. GRL-SVO(UP) can suggest branching variables in the CAD process; GRL-SVO(NUP) can suggest total variable order before the CAD process. Our approaches outperform state-of-the-art learning-basee -base heuristics and are competitive with the best expert-basee heuristics. Our RL-based approaches also show strong learning and generalization ability. Future work is to deploy our approach to practical applications, such as constructing an RL-based package for MAPLE and an algorithm component for automated reasoning tools for non-linear arithmetic solving.
Acknowledgement
This work has been supported by the National Natural Science Foundation of China (NSFC) under grants No.61972384 and No.62132020. Feifei Ma also supported by the Youth Innovation Promo- tion Association CAS under grant No. Y202034. The authors would like thank Bican Xia, Jiawei Liu, and the anonymous reviewers for their comments and suggestions.
References
[1] Alfred Tarski. A Decision Method for Elementary Algebra and Geometry. In Quantifier elimination and cylindrical algebruic decomposition, pages 84. Springer, 1998.
[2] George E Collins. Quantifier elimination for real closed fields by cylindrical algebraic decom- postion. In Automata theory and formal languages, pages 134-183. Springer, 1975.
[3] Mark de Berg, Otfried Cheong, Marc J. van Kreveld, and Mark H. Overmars. Computational Geometry: Algorithms and Applications, 3rd Edition. Springer, 2008
[4] Steven M. Valalee. Planning Algorithms. Cambridge University Press, 2006.
[5] Dejan Jovanovic and Leonardo Mendonça de Moura. Solving Non-lineal Arithmetic. In IJCAR 2012, volume 7364 of Lecture Notes in Computer Science, pages
Springer, 2012.
[6] Dejan Jovanovic. Solving Nonlinear Integer Arithmetic with MCSAT. In VMCA/ 2017, volume 10145 of Lecture Notes in Computer Science, pages 330-346. Springer, 2017.
[7] Fuqi Jia, Rui Han, Pei Huang, Minghao Liu, Feifei Ma, and Jian Zhang. Improving Bit-Blasting for Nonlinear Integer Constraints. In ISSTA 2023, pages 14-25. ACM, 2023.
[8] Christopher W. Brown and James H. Davenport. The Complexity of Quantifier Elimination and Cylindrical Algebraic Decomposition. In ISSAC 2007, pages 54-60. ACM, 2007.
[9] Christopher W Brown. Companion to the Tutorial: Cylindrical Algebraic Decomposition. United States Naval Academy, 2004.
[10] Andreas Dolzmann, Andreas Seidl, and Thomas Sturm. Efficient Projection Orders for CAD. In ISSAC 2004, pages 111-118. ACM, 2004.
[11] Changbo Chen, James H. Davenport, François Lemaire, Mare Moreno Maza, Bican Xia, Rong Xiao, and Yuzhen Xie. Computing the Real Solutions of Polynomial Systems with the RegularChains Library in Maple. ACM Commun. Comput. Algebra, 1563/4):166-168, 2011.
[12] Russell Bradford, James H. Davenport, Matthew England, and David J. Wilson. Optimising Problem Formulation for Cylindrical Algebraic Decomposition. In CICM 2013, volume 7961 of Lecture Notes in Computer Science, pages 19-34. Springer, 2013.
[13] Tereso del Río and Matthww England. New Heuristic to Choose Cylindrical Algebraic Decomposition Variable Ordering Motivated by Complexity Analysis. In CASC 2022, volume 13366 of Lecture Notes in Computer Science, pages 300-317. Springer, 2022.
10

---

[14] Haokun Li, Bican Xia, Huiying Zhang, and Tao Zheng. Choosing Better Variable Orderings for Cylindrical Algebraic Decomposition via Exploiting Chordal Structure. Symb. Comput. 1 116:324-344, 2023.
[15] Matthew England and Dorian Floreseu. Comparing Machine Learning Models to Choose the Variable Ordering for Cylindrical Algebraic Decomposition. In CICM 2019, volume 1617 of Lecture Notes in Computer Science, pages 93-108. Springer, 2019.
[16] Changbo Chen, Zhangpeng Zhu, and Haoyu Chi. Variable Ordering Selection for Cylindrical Algebraie Decomposition with Artificial Neural Networks. In ICMS 2020, volume 12097 of Lecture Notes in Computer Science, pages 281 2-1- Springer, 2020.
[17] Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www. SMT-LIB org. 2016.
[18] Dennis S. Amon, George E. Collins, and Scott McCallum. Cylindrical Algebraic Decomposition I: The Basic Algorithm. SIAM Comput., 13(4):865-85) 877, 1984.
[19] Thomas N. Kipf and Max Welling. Semi-Supervised Classification with Graph Convolutional Networks. In ICLR 2017. OpenReview.net, 2017.
[20] Petar Velickovic, Guillem Cucurull, Arantxa Casanova, Adriana Romero, Pietro Liò, and Yoshua Bengio. Graph Attention Networks. In ICLR 2018. OpenReview.net, 2018.
[21] Dongkwan Kim and Alice Oh. How to Find Your Friendly Neighborhood: Graph Attention Design with Self-Supervision. In ICLR 2021. OpenReview.net, 2021.
[22] Richard S. Sutton, David A. McAllester, Satinder Singh, and Yishay Mansour. Policy Gradient Methods for Reinforcement Learning with Function Approximation. In NIPS 1999, pages 1057-1063. The MIT Press, 1999.
[23] Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Alex Graves, Ioannis Antonoglou, Daan Wierstra, and Martin A. Riedmiller. Playing Atari with Deep Reinforcement Learning. CORR, abs/1312 2013.
[24] Irwan Bello, Hieu Pham, Quoe V. Le, Mohammad Norouzi, and Samy Bengio. Neural Combi- natorial Optimization with Reinforcement Learning. In ICLR 2017. OpenReview.net, 2017.
[25] Vitaly Kurin, Saad Godil, Shimon Whiteson, and Bryan Catanzaro. Can Q-Learning with Graph Networks Learn a Generalizable Branching Heuristic for SAT Solver? In NIPS 2020. OpenReview.net, 2020.
[26] Yao Qin, Hua Wang, Shanwen Yi, Xiaole Li, and Linbo Zhai. A Multi-Objective Reinforce- ment Learning Algorithm for Deadline Constrained Scientific Workflow Scheduling in Clouds. Frontiers of Computer Science, 15:1-12, 2021.
[27] Volodymyr Mnih, Adrià Puigdomènech Badia, Mchdi Mirza, Alex Graves, Timothy P. Lillicrap. Tim Harley, David Silver, and Koray Kavukcuoglu. Asynchronous Methods for Deep Reinforee- ment Learning. In ICML 2016, volume 48 of JMLR Workshop and Conference Proceedings, pages 1928 1937. JMLR.org, 2016.
[28] William Hamilton. Graph representation learning. Morgan & Claypool Publishers, 2020.
[29] Russell J. Bradford, James H. Davenport, Matthew England, Scott McCallum, and David J. Wilson. Truth Table Invariant Cylindrical Algebraic Decomposition. J. Symb. Comput., 76:1-35, 2016.
[30] Chenqi Mou, Yang Bai, and Jiahua Lai. Chordal Graphs in Triangular Decomposition in Top-Down Style. J. Symb. Comput., (02:108-131, 2021.
[31] Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L., Dill. Learning SAT Solver from Single-Bit Supervision. In ICLR 2019. OpenReview.net, 2019.
11

---

[32] Minghao Liu, Fan Zhang, Pei Huang, Shuzi Niu, Feifei Ma, and Jian Zhang. Learning the Satisfiability of Pseudo-Boolean Problem with Graph Neural Networks. In CP 2020, volume 12333 of Lecture Notes in Computer Science, pages 885-896 Springer, 2020.
[33] Quentin Cappart, Didier Chételat, Elias B. Khalil, Andrea Lodi, Christopher Morris, and Petar Velickovic. Combinatorial Optimization and Reasoning with Graph Neural Networks. In IJCAI 2021, pages 4348 4385. ijcai..rg. 2021.
[34] Zongyan Huang, Matthew England, J. Wilson, James H. Davenport, Lawrence C. Paulson, and James P. Bridge. Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition. In CICM 2014, volume 8543 of Lecture Notes in Computer Science, pages 92-107. Springer, 2014.
[35] Ronald J. Williams. Simple Statistical Sradient-Following Algorithms for Connectionist Reinforcement Learning. Mach. Learn., 8:229- 256, 1992.
[36] Matthias Fey and Jan E. Lenssen. Fast Graph Representation Learning with Py PyTorch Geometric. In ICLR Workshop on Representation Learning Graphs and Manifolds, 2019.
[37] Matthew England, David J. Wilson, Russell J. Bradford, and James H. Davenport. Using the Regular Chains Library to Build Cylindrical Algebraic Decompositions by Projecting and Lifting. In ICMS 2014, volume 8592 of Lecture Notes in Computer Science, pages 458-465. Springer, 2014.
[38] François Lemaire, Marc Moreno Maza, and Yuzhen Xie. The RegularChains library in MAPLE. SIGSAM Bull., 39(3)96-97, 2005.
[39] Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. CVC5: Versatile and Industrial- Strenggh SMT Solver. In TACAS 2022, volume 13243 of Lecture Notes in Computer Science, pages 415 442. Springer, 2022.
[40] Scott McCallum. An Improved Projection Operation for Cylindrical Algebraic Decomposition. In EUROCAL 1985, volume 204 of Lecture Notes in Computer Science, pages 277-278. Springer, 1985.
[41] Wei-Lin Chiang, Xuanqing Liu, Si Si, Yang Li, Samy Bengio, and Cho-Jui Hsieh. Cluster-gen: An efficient algorithm for training deep and large graph convolutional networks. In Proceedings of the 25th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining, KDD 2019, Anchorage, AK, USA, August 4-8, 2019, pages 257-266. ACM, 2019.
[42] Shyam A. Tailor, Felix Opolka, Pietro Liò, and Nicholas D. Lane. Adaptive filters and aggregator fusion for efficient graph convolutions. CoRR, abs/2104.0148) 2021.
[43] Shaked Brody, Uri Alon, and Eran Yahav. How attentive are graph attention networks? In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022.
[44] Jiaxuan You, Zhitao Ying, and Jure Leskovec. Design space for graph neural networks. In Ad- vances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual, 2020.
[45] Xavier Bresson and Thomas Laurent. Residual gated graph convnets. CoRR, 171.0771 2017.
[46] William L. Hamilton, Zhitao Ying, and Jure Leskovec. Inductive Representation Learning on Large Graphs. In NIPS 2017, pages 1024-1034, 2017.
[47] Yunsheng Shi, Zhengjie Huang, Shikun Feng, Hui Zhong, Wenjing Wang, and Yu Sun. Masked label prediction: Unified message passing model for sumi-super classification. In Pro- ceedings of the Thirtieth International Joint Conference on Artificial Intelligence, 2021, Virtual Event/ Montreal, Canada, 19-27 August 2021, pages 1 1548-1554 ijcai.org, 2021.
12

---

A Cylindrical Algebraic Decomposition
A.1 Detailed Description
A.1.1 Polynomial
N and R denote the set of natural numbers and real numbers, respectively. Let x = { 1** Fnn be the variable set, where 21 x2 <... In, is the order of the variables.
A term f/3 is finite production of powers of variables, i.e. IT "2 where diy N as the degree of the variable Zzz- We denote Dj=1 dig as the degree of the term.
polynomial P E [[]]] of general form is finite sum of terms, i.e., P >xn Ctt, where oj E Rs coefficient of term 4. In addition, the equivalent nested form of polynomial Q R[ 1.
Q 0m 1 + am- dm-1
Go:
where < d1 < ..... < dm. and the coefficients a; are polynomials in IR [ -T,- with 0m o O. We denote as main variable, dm as degree, am as leading coefficient of the polynomial Q. For example, given a variable order 21 < x2 < 23,
32, 32,
22222 120g + Ji 3133 + T223
((x1 1)m2)a33 + (x1 1 x2)x3.
The degree of i zgas. zgag. vz. 2233, 2243 are 4,3,2,2,, while that of the polynomial p(21, xz) is 2, and leading coefficient is ((x1 + 1)x22..
A.1.2 Cylindrical Algebraic Decomposition
A Cylindrical Algebraic Decomposition (CAD) is a decomposition algorithm of set of polynomials in ordered RR space resulting in finite sign-invariant regions, named cells. After CAD, it can query limited set of sample points in corresponding cells. Due to the sign of each polynomial is either always positive, always negative, or always zero on any given cell, one can determine the sign of the polynomials at any point in R" using this set of sample points.
Note that computing the CAD of set of univariate polynomials cone-dimensional CAD) is quite simple. We only need to calculate all the real roots of the polynomials, and the cells are precisely these real roots themselves along with the intervals they divide. This leads to motivation for computing the CAD of a set of polynomials with variables, which involves recursively reducing the construction of a k-dimensional CAD to the construction of (A= - 1)-dimensional CAD, until reaching the recursive boundary of computing a one-dimensional CAD, and then constructing higher-dimensiona. CAD from lower-dimensional CAD continuously.
Formally, the algorithm consists of three components: projection, root isolation, and lift. A diagram is shown Figure 5 The project phase eliminates the variables of a polynomial set Ps with n variables by strictly defined projection operator proj in a given order 2 < I2 < ... < I,, until only one where P. = proj(Pi+1) contains only variable Tı left, resulting polynomial sets P..... Pr-11,
the variables ..,... .y. P. can be constructed from the CAD of P:-1- Then the root isolate and lift phases are alternated successively. To make the following statement compatible, we replace the notation of P1 with Pt, Let N(i) denote the number of cells generated by P; (also equals to the number of sample points). We set (0) to be 1. The root isolate phase will output all roots of univariate polynomial set. When i = 1, the roots of Pi, split R into ((1) cells. Let SP.,k, I k < N - 1) denote the set of sample points of the cells generated by P., and SP, denote the union of SP.. Actually, SP, is precisely the sample points of the cells generated by P. and [SP, = N (1). The lift phase assigns each sample point st,k of SP, to variables of P.+1. i.e., (I1, T2, (I,, to polynomials in P+11, resulting in univariate polynomial sets P.+1,, < k S N()). Invoking the root isolate phase will obtain each SP.+1, & and finally their union SP.+1- After repeating root isolate and lift for n 1 times, we achieve the cells of P,, characterized by the sample points SP,, The paper provides concrete example of the CAD process in Example 2.1.
The projection operator is carefully designed to ensure that the CAD of
.xa) + s;,,, 1 < k < N().
The projection operator proj plays a key role the CAD process, which carries enough information to ensure that the CAD of any set of polynomials P can be constructed from the CAD of PP))
13

---

Spp e R²)
Project
Lift
Pa-1:ff B"xa Kn-tI
1 (p B=-1)
Project
Lift
Project
Lift
P::ff e R[s]]
SP;: (p R]
Root Isolation
Figure 5: The process of CAD.
The first projection operator that satisfies the above property is designed by George Collins[2), which too complicated, however. Here, we introduce another classic simplified projection operator, the McCallum Projection Operator [4)] It is the default projection operator used in the ProjectionCAD package 37 and our architecture of GRL-SVO(UP).
In mathematics, the resultant is used to determine whether two polynomials have common zeros, while the discriminant is used to determine if one polynomial has repeated roots. Both these two tools are crucial in the construction of the projection operator. We first introduce the definitions of the resultant and the discriminant, and then the McCallum Projection Operator is detailed in Definition
Definition (Resultant). Let f1, f2 be two polynomials in (11,,..... Inl. Assume that
f1 am + am 1 2 11 + ap.
J2 = bnoan + bn- 18 and-- ..... bo- The resultant of fi and f2 with respect Ina Res(f1, f2, is:
am
am-1
am
am-1
40
f2, =
Om
am-
bn
bn-1
bn
bn-1
bo
bn
b
bu
Definition 4 (Discriminant). Let be polynomial in R[x1, nn..
Assume that
f am= n
a. 1m--17 12
ag.
The discriminant of with respect to Fa, Dis( x,) is:
Dis(f, (-1) mim
Øs DIn xn).
Res(f,
Om
Definition 5 (McCallum Projection Operator). Let F (fi...., fk} be of polynomials in R[21.... pn The McCallum projection operator, proj.- a mapping that maps F to proj... (F), where proj... (F) is the set of polynomials in E[ 2n-1l defined by:
The coefficients of each polynomial in F.
The discriminant of each polynomial in with respect to Tn.
The resultant of any two different polynomials fo J3 in with respect to Fa-
Another important component in the CAD algorithm is the real root isolation algorithm, which accepts of univariate polynomials and results in all the roots (actually, the arbitrarily small intervals that contain each root) of the univariate polynomials. This can be accomplished by invoking
14

---

the subalgorithm RootIsolation multiple times and adjusting the upper and lower bounds of the initial interval for each univariate polynomial.
We provide the specifics of the algorithm RootIsolation in Algorithm 2 Before that, some necessary concepts like the sign variation, the 1-norm, and the Sturm sequence are introduced, which play role in the algorithm Rootlsolation.
Definition 6 (Sign Variation), For a sequence of non-zero real numbers e: C1 cg. "., Cj. the sign variation of V(c), is:
V - Mill S < k&0;041 <0),
For sequence of univariate polynomials S: fi. f2. "., fk. the sign variation of S at real number (S( is:
V. (S) = V33),
where 3 is the real number sequence (1),, f2(a). ... fa
Definition 7 (1-norm). Given univariate polynomial am am Am + Om 12 Am + + The
I-norm of f. Ilfll,
||
ail.
1=0
Algorithm SturmSequence
Input: f: univariate polynomial
Output: sturm: the Sturm Sequence of f
1: sturm
2: h +
3: g + f
4: t- -rem(g, h,
5: while r X 0 do
6: Append r to slurm
7:
h g-g
8:
g g+r
9:
r+ rem h, x)
10: end while
return sturm
Algorithm 2 Rootlsolation
Input: f: univariate polynomial
Output: (a, ff has real root in (a, b) where a, b are rational numbers
1: S + SturmSeqqencce(F
3: < 1/ -I1
2:
4: if (S) = (S) then
5: return failure
6: end if
7: while V.(S) Vi(8) > 1 do
8:
ct atb
9: if VS)
> Vi(S) then
10: bec
else
12:
13:
end if
14:
end while
15: return (a, b)
15

---

20
100
Venoo Uisg0 HIU
Tire
10
105
101
Harber
Mamber
(a)
(b)
Figure 6: The relationships between the number of cells and other important indicators. Figure 6a and Figure rbjeessctyy correspond to the relationships between the number of cells and computation time and the relationships between the number cells and memory usage. Five hundred instances of 3-var are randomly selected from the random dataset to construct the two scatterplots.
A.2 Case Study: Discriminant
Actually, whether x² + bæ + = O has a real root is equivalent to checking the satisfiability of
3r.x² bu + c 0. Let's elaborate on why the quantified formula 3r.x² ba + c 0 can
be transformed into an equivalent quantifier-free formula 6 4e 2 0 via CAD techniques. By feeding the CAD algorithm with the set of polynomial {x.² + bæ c} and an order decomposes I3 into 9 cells:
x, CAD
b
b
b b
62
C
4
C
4
C
4
vba 4n0
/12--a0
b
/b2 - 4nc
8
2
2
2
b
62
6a
I
yB2 4nc
2
1b2 4ac
<
2 +
b
/b2 40c
b
b
1
b
6
ba
ba
b
Note that the sign of the polynomial x² + bu + c is zero if and only if (b, c,,,,, belongs to cells:
b
b = b
b
2
2 C
C
c < T b
4
6
4ac
/B 4nc
2
2
So we know that there must exist x such that x² + br + 0 when b2 - 4c > 0 or b² - 4c 0. and it is impossible find x such that x² br c 0 when b² 4c < 0. So, we can conclude the quantified formula Zr.z² + br + c= 0 is equivalent to the quantifier-fi free formula b² - 4c 2 0. In fact, similar processes can be abstracted into universal algorithm to solve the quantifier elimination problems in the real closed field. See 2 for more details.
A.3 Relation of #Cells And Efficiency
As in Figure there is a strong correlation between the number of cells produced and the computation time, as well as the memory usage. When the number of cells increases, the computation time and the memory usage also increase.
16

---

Table 3: Parameters of random dataset generation.
Table 2: Parameters of randpoly function.
Parameter
Description
#vars
coeffs
expons
terms
vars
List or set of variables
(and(-100.1100))
rand(U..2)
rand(3..6)
coeff's expons
Generator of coefficients
rand(-100..1000
r0nd(0..2)
3
Generator of exponents
rand(-100..100)
ra.d(0..2))
terms degree
Number of terms
rand(-100..100)
(U..(
3
Total degree for a dense polynomial
7
tand(-100...l)
(a.d(0..2)
3
dense
The polynomial to be dense
rand(-100.. 100.
rand(0..2)
3
homageneous
The polynomial is homogeneous
rand(-100..100)
rand(0..2)
B Experiment Setup
B.1 Datasets
B.1. Random Dataset
We generated the random polynomial via the randpoly(vars, opts) function in MAPLE, where opts are specifying properties like coeffs, expons, terms, degree. dense, homogeneous. Table 2 lists the descriptions of parameters. We also show an example of random polynomial generation.
For example, randpoly(Ix1,) I2, T2, terms = 4, expons = rand(O..2), coeffs = rand(-100..100) will generate polynomial,
56m 4xf + 37.112233 32x1 122233
where (an is random number generator in the range of [a, bj. Note that the random polynomial is sparse and non-homogeneeus by default. We also ignore the parameter degree, because it is only valid in the case of dense random polynomial generation.
Table lists the parameters for randpoly for generating the random dataset, where #vars = n corresponds to list of variables (2, .n]]
The random number for terms is generated with Python's 's random library outside the MAPLE script. If the polynomial produced by MAPLE lacks a constant term, one is added, ranging from -100 to 100, using the same Python library.
B.1.2 SMT-LIB Dataset
The SMT-LIB dataset is built by the instances that only involve real constraints in the QF NRA category the SMT-LIB [17]. Using the Python interface of 23[5), we parse the instances to extract the polynomial sets, discarding any instances that cannot be correctly parsed. Then we categorize the processed polynomial sets based on the number of variables and finally build the SMT-I.IB dataset, containing instances ranging from 3 9 variables with counts (5908, 1371, 131, 123, 318, 41, 24). Furthermore, we observed that there are numerous polynomial sets in the dataset that yield the same result after factoring out the irreducible factors, which are indistinguishable from CAD algorithms. So we cluster them and only one instance of each clustering is included in the dataset, resulting in {1777, 387, 17} instances for 3-var, v-rar to 6-var and 7-var 9-var, respectively.
B.2 Neural Networks
Table lists the hyper-parametert of the GNN encoder, the networks used in GRL-SVO(NUP)' architecture to transform the original embeddings linearly and simulate the project process, actor network, critie network, and RL architecture.
C Ablation Experiments
C.1 The Efffec of Features
There are 14 different features to characterize a variable listed in Table We conduct an experiment on the effect of features. We make masks for these features, where the mask will the features that we do not care about zero.
17

---

Table 4: The hyper ppper-paramttrss.
Category
Parameter
Value
GNN
The number GNN layers
GNN
The number of Intermediate layer features
256 meun
GNN
Aggregation method
GNN
Use bias
True
NUP transform
The MLP layer features
[14, 256, 128, 64]
NUP simulate
The ML.P layer features
[128, 512, 256, 64]
Actor
The size of MLP layer features
[256. 512, 128,
Critic
The size of MLP layer features
[256. 512, 128, I]
RL
Batch size
32
RI.
Learning rale
2e-5
RL
Training maximum epoch
RL
Reward normalization factor (M)
50000
Table 5: The original embedding of a variable in an associated graph.
Symbol
Description
E(())
Number of other variables occurring the same polynomials
Ex(2)
Number of polynomials containing x Maximum degree of among all polynomials
Es(2)
E4(2)
Sum of degree of among polynomials
Es(2)
Maximum degree of leading coefficient of x among all polynomials
Ea(2)
Maximum number of terms containing among all polynomials
E((2)
Maximum degree of all terms containing
Ex(r)
Sum of degree of all Sum of degree of leading coefficient
containing
Eg(x)
Ev((1)
Sum of number of terms containing Proportion of z occurring in polynomials Proportion of æ occurring in terms Maximum number of other variables occurring in the same term Maximum number of other variables occurring in the same polynomial
En(r)
Ex(rr
Es((r)
Ema(r)
1. One-hot masks (test the effect of single feature), for example, to test the effect of E1, the corresponding one-hot mask is (1, O. O, O, O, 0. 0, 0, 0, 0). Multiplying with input feature will result in feature vector with only Ei while others are 0.
2. Operation masks (test the effect of different operations in features) will group features according to their operation type (maximum, sum, and proportion). Note that we treat E1, E2 as sub-features utilizing sum operation.
Max: Es, Es, Eo, E7, E1a, E14
Sum: E1, E2, E4, Es, Eg, E10
Prop: F11, FJ2
3. Object masks (test the effect of different objects in features) will group features according to their target objects (variable, term, and polynomials).
Var: E,, Eg. Es, E1a, E14
Term: Es, EG, E7, Es, Eg, E10, E12
Poly: Fe,, Fn
4. Because degree a common feature that most heuristics are concerned with, testing the effect of degree is necessary. Degree masks will group features according whether they utilize degree.
Degree: Eg. Es, Es,
NoDegree: E1, Ez, Es, Ero, Eu1 E1s, E1s, Ei4
Table and Table the results of different single, operation, object, and degree features. We can conclude that only one feature is not enough. The sum, term, and degree may be the most important factors, as using Sum/ Sww/Tumm/Deeee Temt//////eereee features will result in the largest difference in performance.
18

---

Table 6: The performance different single features.
E13
C1a
252,0
AVG.N
211.58
211.3
AYG.N
Table 7: The performance of different feature classifications.
Operation
Object
Degree
Max
Sum
Prop
Var
Term
Poly
Degree
NoDegree
#57
1640
1754
1670
1635
1726
1462
1723
1683
NUP
AVG. T
159.42
101.21
147.48
152.11
116.39
249.17
114.95
141.65
AVG.N
2444.09
2145.71
2496.74
2250.21
2300.32
2857.07
2177.08
2468.04
#S7
1788
1707
1751
1770
1713
UP
AVG.T T
119.80
81.93
129.53
119.32
102.07
211.55
91.31
125.53
AVG.N
2346.79
2082.22
2369.74
2184.08
2232.74
2743.79
2103.21
2359.62
C.2
The Effect of Network Size
conduct an experiment on the effect of network size, and the results are listed Table The number of GNN layers (for short, #G) E [1. 2, 3, 4, and the number of Intermediate layer features (for short, #I) E {32, 64, 128, 256, 512) where Actor and Critic will keep the same proportion 2:4:1. Note that the input dimension of Actor and Critic is the same #L For example, if #I 32, then the dimension of the Actor and Critic are both [32, 64, 16, 1]. Elements in the following tables are #SI in the validation set and #SI in the testing respectively.
C.3 The Effeet of Network Structure
We conduct an experiment on the effect of network structure. We build two models: one without embedding (NO EMB), and the other without edge (NO EDGE). Note that the GNN updating operator we used is x Wix; + W₂ Σ (EN(() Gj Xj + b. As edges are not considered in NO EDDE, actually, the operator will be For NO_EMB, #1 = 1459, AVG. T = 252.03, A AVG.N = 2874.91. Table 9 of DO_EGE testing DO_EGGE is good, and GRI-SVO can still outperform such models. We explore the performance of NO (DGE(NU(U)) under different sizes of parameters with GRL-SVO(NU)), MLP_ AP_4__12 has twice as many parameters as ours. GRL-SVO(NUP) can outperform all MLPs as shown in Figure 7 It is the advantage of the graph structure where variable can grasp neighbor information.
Wix, + b. So NO EDGE is equivalent MLP.
shows the result The performance of NO_EMB drops dramatically while that of
C.4 The Effect of Reward Normalization Factor (M)
We
make ablation experiment on M that we train the models with ==10000, 20000, 50000(ours), 100000, and without M. Note that there is no M, the reward (the number of cells) will be relatively large integer. As shown in Table TO M is necessary. The first number is the result of the validation set, while the second is the result of the testing set.
C.5 The Effect of GNN Architecture
We conduct experiments using different GNN architectures available in PyTorch Geometric that have similar formal parameters as the GNN architecture we used: ClusterGCNConv 41,, EGConv 42
Table 8: The performance (#SI) of GRL-SVO(NUP) and GRL-SVO(UP).
GRL-SVOINUP)
GRL-SVOUP
32
64
128
256
512
32
64
128
256
512
1754,1737
1756,1741
1771.1755
1770,1765
1764,1765
1767,1759
1768.1755
1777,1774
1789,1789
1790.1793
2
1771.1764
1762,1747
1765.1763
1767,1766
1764,1768
1773,1763
1780.1777
1778.1776
1786,1793
1788.1794
1765,1758
1766.1758
1761,1766
1770.1769
1782,1785
4
1765_1761
1768,1761
1764.1762
1766.1765
1769,1765
1775,1766
1784,1775
1780.1779
1792,1794
1788.1793
1768.1762
1765,1763
1771.1759
1766,1761
1763,1762
1779.1779
1784,1781
1788.1797
1792,1790
1791.1790
19

---

Table 9: The performance of NO EDGE under different sizes,
ML.P 2 256
MI._ 3 256
MI.P 4 -__266
MI.P MI.P_4_512
#SI
1763
1763
1764
1756
AVG.T
97.89
98,43
97.68
99.08
AVG.N
2132.33
2140.18
2129.33
2148.64
GRL-SVOONUF)
180
PRL-SVOINUP)
1500
MIP 2222256
NLP 2.256
MLP MUP.3,256
MLP 3,256
Number of 1E 600 Instannes
1403
MLP_4_256
-KP_4,512
Number of Thm cout mncttrttt oc
1.0
MIP_4_112
ML5.4_256
1,000
120
1000
900
100
40
80
90
10
50
90
1000
Epochs
Epacchs
(a) On training set
(b) On validation set
Figure 7: The training process of NO_EDGE and GRL-SVO(NUP),
4 ResGatedGraph- that each graph neural network (GNN) is capable of effectively learning this problem. Our approach not reliant on the specific GNN structure.
FiLmCony 42). LEConv 42 GATConv 20). GATv2Conv
43
GeneralConv
Conv 45 SageConv 46). TransformerCon [47. We could observe from Table 1htht
C.6 The Effect of Coeflicient
With regard the choice of variable order, the current works do not consider coefficient (both heuristics), Some experts in Symbolic Computation believe that the
Expert-Based or Learning- reason may be related to the calculation of CAD projection: CAD projection uses two polynomials to make a resultant (Definition 3) to eliminate common variable, so it first depends on the common variable set of these polynomials (which does not involve coefficient); secondly, the amount of calculation generally depends on the degree of public variables because the degree determines the size of the resultant matrix. For practical instances, the variation range of the coefficients is uncontrollable, which will increase the difficulty of Learning- carning-Based design and training the neural network. The impact of the coefficient the problem is complex. We provide some intuition through Figure
(a) { + 4x my. 2² + 2ry 1), y 13, < x 89;
(b) {a'y + 8x.2 zy. -2 2ny 1),0 < 13,y
89;
(c) {a'y - 4x² zy, -y,-2² + 2ry 1), y 45, x x 125;
(d) {x"y + xy, 2ny - 1}, - 29, 4 x: 101;
(e) (-x2y + zy, - =² 2ny 11, x yy: 45,y 97.
Table 10: The performance of different M.
NO
1000
10000
50000 (ours)
100000
#SI
1677, 1666
1672. 1669
1764, 1769
1766. 1765
1766, 1765
NUP
AVG.T
133.06, 142.19
140.28, 142.56
93.03, 95.57
91.68. 97.78
93.46, 97.51
AVG.N
2230.65,
2214.20
2250.11.
2222.47
2134,50, 2136.30
2129.45. 2142.98
2147.43, 21577.6
#ST
TT82, 1196
1726, 1723
1789, 1795
1792. 1795
1791, 1793
UP
AVG.T
387.16, 381.11
109.12. 115.13
73.86, 80.20
72.02. 79.57
73.68. 79.88
AVG.N
3125.50, 3101.32
2100.53, 2097.48
2058.08,
2.81.92
2062.09, 2075.23
2058.05. 2070.75
20

---

Table 11: The performance of GRL-SVO(NUP) with different GNN architectures.
ClusterGCNCony
EGConv
FiLmConv
LEConv
GATConv
1767
1765
1760
1761
1726
AVG.T
94.26
98.53
96.49
96.76
119.72
AVG.N
2144.66
2177.32
2136.67
2151.75
2166.78
GATv2Conv
ConeralConv
ResGGatedGraphhonv
SugeConv
TranshormerCom
#SI
1762
1768
1759
1765
1769
AVG.T
104. 14
95.17
96.25
96.74
94.45
AVG.N
2184.86
2132.81
2146.59
2131.22
2134.51
(a)
(b)
(c)
(d)
Figure 8: The results of slight changes of coefficients.
The number of cells of (a) and (b) the same, while (c), (d), and (e) different. But the best variable order is the same (æ < y/ in these cases. To a certain extent, in these cases, the coefficient mostly affects the number of cells. We conduct experiment coefficient that have randomly modified the coefficients (in [-100, 100]) of 1000 instances randomly selected from 3-var testing set. Since the coefficients were the only modification made, we used the original variable order generated from the unaltered instances. Our models continue to outperform other heuristics, as demonstrated by Table [2] We observe slight decline in the performance all heuristics, indicating that the coefficient also plays a significant role as parameter (although it may not be the most crucial one).
D
Additional Results
D.1 Results Under Other Criteria
Assume and N denote the runming time and number cells. COMAVG. and COMAVG.N denote the average of T and N of the instances that all heuristics solved within the time limit. Since the sotd and ndrr heuristics are not applicable to most instances with the number of variables more than 5, we remove the comparison with these two heuristics the results of the new criteria.
There are 1325, 292, 142, 106, 84, 103, and 87 common instances that all heuristics except sotd and ndrr solved within the time limit for the random dataset from 3-v to 9-var; and for the SMT-LIB dataset, 1670, 354, 9 instances for 3-var, 4-var to 6-var and 7-var to 9-var, respectively. Table [3 shows the results and the best scores are bolded. We can observe that GRL-SVO still achieves relatively good performance under the new criteria.
D.2 Performance of Fine-Tuning
As GRL-SVO(UP) has demonstrated strong generalization abilities and achieved the best performance on almost all datasets, there is still room for further improvement in the generalization capabilities of GRL-SVO(NUP). So, we further investigate the performance of GRL-SVO(NUP) after fine-
Table 12: The performance of different heuristics after the coefficients are randomly modified.
brown
triangular
EMLP
sotd
ndrr
gmods
GRL-SVOXNUP)
GRL-SVO'UP)
#SI
831
762
855
898
842
867
892
912
A
155.42
212.50
125.54
79.73
141.29
100.30
79.96
64.89
AVG.N
2380.67
2606.40
2353.11
2065.13
2288.08
2162.19
2100.57
2023,58
21

---

Table 13: The performance different heuristics under the new criteria. The dash x." indicates that the method does not support the category.
Categorics
KUP
UP
EB
LB
EB
FMIP
PROlboma)
PVOUnimmpler)
GRE-SWONNTP))
S-var(tes))
COMAVG
COMAVG.
1968
1474.50
23.28
4-var
COMAVG.N N
CDMAVG.
2286. 79
24.25
2476.00
14,07
2227 53
23.22
2306. 90
13.75
2018.79
20.30
1730.37
12.48
1759
13.82
5 vur
COSAAVG
COMAVG. N
4624,89
27.90
5222.5
12.51
4355 15
27.35
4866649
30.26
42%8.3
31.36
5415.34
19:35
3340.59
15.82
COMAAV
$2.71
38,95
56,23
40.57
38.38
32.67
22.95
COMAVG.
7761.30
6733.09
5440.62
CORAVG
31.96
35.41
COMAYG.
9285-12
975557
6526.24
COMVVG
10245
11831
67.18
COMAYG
15184.9
07
14730.24
11063,10
12075 62
Swaar
COMAVG
COMANG
2004544
131.36
23814.45
169.5
18132.05
123.07
16094.35
56.77
15995,08
96.90
SMF-LB (3-ar)
COMAVO 7
COMAVG.N N
3236.61
10.41
3746.72
12307
6391.53
11.72
2906,43
T0:66
2736.89
3.47
2815.23
1AAY
SMY-1I8
COMAVG.
C
19,75
16815.00
41.00
14730.50 58
15160.00
25,000
(7-var 9-var)
COMAVG.N
17169.67
17169.67
6149.89
12609.22
14919667
Table 14: The performance of NUP heuristics, with the performance of GRL-SVO(NUP) after
fine-tuning. The dash "_" indicates that the method does not support the category.
Categories
NUP
EB
brown
triangular
EMLP
PVO(brown)
PVOttringgalar GRL-SVOINUP)
#31
1620
1304
1686
1772
3-var(test)
AVG.T
170.63
227.60
140.06
94.07
AVG.N
2421.18
2663.09
2384.29
2157.92
#31
415
376
408
392
456
4-var
AVG.T
352.7
394.71
360.33
376.71
298.74
AVG.N
$258.57
5539.73
5338.45
5536.28
5060.19
#31
236
202
242
218
253
S-var
AVG.T T
435.64
495.34
419.50
466.47
394.12
AVG.N
12465.41
13493.00
11932.31
12826.53
11586.65
#SI
175
149
180
160
204
6-var
AVG.T T
500.62
551.15
489.57
526.80
432.64
AVG.N
20487.45
20068.22
20029.06
18993.53
19407.97
#ST
163
118
175
7-var
AVG.T 549.15
632.62
$22.35
AVG.N
28552.12
29182.78
27779.48
#3I
173
138
177
8-var
AVG.T 601.17
653.60
594.77
AVG.N
39540.72
40902.42
38957.71
#31
151
125
171
9-var
AVG.T T
651.36
691.92
619.39
AVG.N
48860.36 36
50315.52
47406.84
#SI
1770
1763
1675
1768
SMT-LIB (3-var)
AVG.T T
20.33
23.68
83.09
20.86
AVG.N
4449.77
5070.46
7654.04
4014.59
#TST
374
372
372
372
365
SMT-LIB (4-var to 6-var)
AVG.T
83.92
87.85
86.22
86.88
88.42
AVG.N
24514.73
24178.54
22953.99
22644.04
20910.95
#ST
13
12
12
SMT-LIIB (7-var 9-var)
AVG.T
308.14
377.32
341.21
AVG.N
53971.24
58675.94
52381.82
tuning. We conduct case study on fine-tuning, utilizing 100 instances with 4 variables. All the hyperparameters employed during the training process were identical those listed in Table
As shown in Table 14 after fine-tuning, GRL-SVO(NUP) exhibits the best performance among all NUP methods across all categories of the random dataset. The #SI indicator for GRL-SVO(NUP) showed enhancements ranging from 1.00% to 14.38% across the 4-var to 9-var categories of the random dataset, with slight improvements also observed in the SMT-LIB dataset. Although fine-tuning can help improve the efficiency of GRL-SVO(NUP) the approach is not fit for the instances with relatively larger number of variables, as we need run the most variable orders of each instance to build training dataset. So, for high-dimensional instances, how to fine-tune is promising direction.
22


Reviews:
[{"review_id": "LvedQ3hIgD", "reviewer": "Reviewer_HXCT", "summary": "This paper proposed a new method for suggesting the variables order for Cylindrical Algebraic Decomposition (CAD) problem. Their method utilized Graph Neural Networks (GNN) and Reinforcement Learning(RL). They proposed two variants: one utilizing projection(UP) and one without projection (NUP). They test their methods on two datasets and showed that the UP method outperforms nearly all methods on nearly all tasks, while the NUP method outperforms almost all NUP method. In addition, the UP method they proposed is the first LB and UP method, according to their report.\n\nIn summary, I think this is a very creative application of RL and GNN on combinatorial optimization problems, though some improvement and ablation study can be made. The writing is very good, and the comparison to the current methods is complete and well categorized.", "questions": "See above.", "limitations": "See above.", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. They proposed two algorithm: GRL-SVO(UP) and GRL-SVO(NUP), utilizing the techniques in RL and GNN to optimize the number of cells  of CAD problem for a certain variable order. I think this idea is creative and worth investigating.\n2. Their explanation to CAD and SVO(suggesting variable orders) is very clear (especially the detailed version in the appendix), and they gave many example to help people who are not familiar with CAD (like me) to quickly understand what they are doing. \n3. The experiments showed that their method outperform most of the current methods on most datasets, and they also compare the UP method and NUP method they developed.\n4. The writing is very good and the literature review is clear and complete.", "weaknesses": "In general this is a good paper. Below are my personal suggestion for a better paper. I do not expect you to add more experiments during the short rebuttal period, so you should not worry about it.\n\n1. The interpretability is relatively weak. Compared to the Expert based methods, the learning-based method typically use some black-box model such as deep neural networks, GNN or RL to optimize the number of cells of CAD problem. However, more explanation and ablation study can be done, although in general, this GNN+RL method is a black box. For example, in EB methods, people often use some human-created features to suggest the variables order. Since you encode 14 human-crafted features in the graph embedding matrix, maybe you can show which features in the matrix are the most important? Or does this completely depend on the property of the set of polynomials? Also, since you use the adjacent matrix of association graph as well as the variable embeddings as inputs, what will happen if you simply input the adjacent matrix or variable embedding? Will the performance drop drastically? \n\n2. There might be overfitting when you apply a large neural networks on a small set of data. In your experiments, the NN is four-layers with hundreds of hidden size, but the data size is relatively small with only thousands and even hundreds of data. So I am not sure whether there will be overfitting in your training. I think one possible solution is to try to use a smaller neural networks to train the model and evaluate it (also you can try a larger one) to see whether the performance will drop when the size increases. Another question is, I do not see how you use the validation dataset (in Line 269, you said the training : validation : testing is 8:1:1). Typically the validation set is used to tune some hyperparameters, but I do not see in the appendix that you tuned any parameter using this set.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your feedback. Your suggestions are very important and helpful to improve the quality of our work. So we have arranged as many experiments as possible to further discuss our results.\n\n``` \nSince you encode 14 human-crafted features in the graph embedding matrix, maybe you can show which features in the matrix are the most important?\n```\nExperiment 1: We conduct an experiment on the effect of features and will append it to the Appendix. We make masks for these 14 features, where the mask will set the features that we do not care about as zero:\n1. One-hot masks (test the effect of a single feature), for example, to test the effect of $E_1$, the corresponding one-hot mask is (1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0). Multiplying with input feature will result in a feature vector with only $E_1$ while others are 0.\n2. Operation masks (test the effect of different operations in features) will group features according to their operation type (maximum, sum, and proportion). Note that we treat $E_1, E_2$ as sub-features utilizing sum operation.\n-  Max: $E_3,E_5,E_6,E_7,E_{13},E_{14}$\n-  Sum: $E_1,E_2,E_4,E_8,E_9,E_{10}$\n-  Prop: $E_{11},E_{12}$\n3. Object masks (test the effect of different objects in features) will group features according to their target objects (variable, term, and polynomials).\n-  Var: $E_1,E_3,E_4,E_{13},E_{14}$\n-  Term: $E_5,E_6,E_7,E_8,E_9,E_{10},E_{12}$\n-  Poly: $E_2,E_{11}$\n4. Because degree is a common feature that most heuristics concern, testing the effect of degree is necessary. Degree masks will group features according to whether utilize degree. \n-  Degree: $E_3,E_4,E_5,E_7,E_8,E_9$\n-  NoDegree: $E_1,E_2,E_6,E_{10},E_{11},E_{12},E_{13},E_{14}$\n\nDue to space limitations, we do not list the results of a single feature. It shows that only one feature is not enough. The best performing feature is $E_{12}$ (on GRL-SVO(UP)) with #SI = 1706, AVG.T = 129.86, AVG.N = 2386.24. Table 1 in the PDF attachment shows the results of operation, object, and degree features.\n\nThe sum, term, and degree may be the most important factors, as whether using Sum/Term/Degree features will result in the largest difference on performance.\n\n```\nsince you use the adjacent matrix of association graph as well as the variable embeddings as inputs, what will happen if you simply input the adjacent matrix or variable embedding? Will the performance drop drastically?\n```\nExperiment 2: We conduct an experiment on the effect of architecture and will append it to the Appendix. We build two models: one without embedding (NO_EMB), and the other without edge (NO_EDGE). Note that the operator of GraphConv in PyG is $\\mathbf{x}^{\\prime} _i = \\mathbf{W} _1 \\mathbf{x} _i + \\mathbf{W} _2 \\sum _{j \\in \\mathcal{N}(i)} e _{j,i} \\cdot \\mathbf{x} _j$. As there is no edge weight in our models, actually the operator we use is $\\mathbf{x}^{\\prime}_i = \\mathbf{W} _1 \\mathbf{x} _i + \\mathbf{W} _2 \\sum _{j \\in \\mathcal{N}(i)} \\mathbf{x} _j$. NO_EDGE will lead $\\mathcal{N}$ to be empty, and $W_2$ will lose its effect, so it will be MLPs. Table 2 in the PDF attachment shows the results of NO_EDGE(MLP) and NO_EMB.\n\nThe performance of NO_EMB drops dramatically while that of NO_EDGE is good. GRL-SVO can still outperform such models and GRL-SVO(NUP) outperforms much more. Due to NUP training time is relatively short (compared to UP), we continue to train GRL-SVO(NUP) and NO_EDGE(NUP) to 30 epochs and explore the performance of NO_EDGE under different sizes of parameters. MLP_4_512 has twice as many parameters as ours. GRL-SVO(NUP) can outperform all MLPs as shown in Figure 1. It is the advantage of the graph structure where a variable can grasp neighbor information.\n\n\n```\nI think one possible solution is to try to use a smaller neural networks to train the model and evaluate it (also you can try a larger one) to see whether the performance will drop when the size increases.\n```\nExperiment 3: We have conducted an experiment on the effect of size and will append it to the Appendix. # GNN layers (for short, #G) $\\in$ {1, 2, 3, 4, 5} and # Intermidiate layer features (for short, #I) $\\in$ {32, 64, 128, 256, 512}$ where Actor and Critic will keep the same proportion 2:4:1. Note that the input dimension of Actor and Critic is the same as #I. For example, if #I = 32, then the dimension of the Actor and Critic are both [32, 64, 16]. Elements in the following tables are #SI in the validation set, #SI in the testing set, respectively. The first table is the performance (#SI) of GRL-SVO(NUP) and the second is the performance (#SI) of GRL-SVO(UP).\n\n\n| | 32 | 64 | 128 | 256 | 512 |\n| --- | --- | --- | --- | --- | --- |\n| 1 | 1754,1737 | 1756,1741 | **1771**,1765 | 1770,1765 | 1764,1765 |\n| 2 | 1771,1764 | 1762,1747 | 1765,1763 | 1767,1766 | 1764,1768 |\n| 3 | 1765,1758 | 1756,1744 | 1766,1758 | 1761,1766 | 1770,**1769** |\n| 4 | 1765,1761 | 1768,1761 | 1764,1762 | 1766,1765 | 1769,1765 |\n| 5 | 1768,1762 | 1765,1763 | 1771,1759 | 1766,1761 | 1763,1762 |\n\n\n| | 32 | 64 | 128 | 256 | 512 |\n| --- | --- | --- | --- | --- | --- |\n| 1 | 1767,1759 | 1768,1758 | 1777,1774 | 1789,1789 | 1790,1793 |\n| 2 | 1773,1763 | 1780,1777 | 1778,1776 | 1786,1793 | 1788,**1794** |\n| 3 | 1781,1767 | 1783,1778 | 1782,1785 | 1788,**1794** | 1786,1793 |\n| 4 | 1775,1766 | 1784,1775 | 1780,1779 | **1792**,**1794** | 1788,1793 |\n| 5 | 1779,1779 | 1784,1781 | 1788,1797 | **1792**,1790 | 1791,1790 |\n\nThe results show that (4,256) seems a better option. If the size is larger than (4, 256), i.e., (4, 512), (5, 256), (5, 512), the effect of the network dropped slightly. \n\n```\nI do not see how you use the validation dataset (in Line 269, you said the training : validation : testing is 8:1:1).\n```\nWe have selected the best model parameters during training via the validation dataset and will append the results of selecting hyperparameters to the Appendix."}, {"review_id": "u3WzrCUJuQ", "reviewer": "Reviewer_zrjH", "summary": "This work proposes a reinforcement learning based method for the selection of a more efficient variable order for the downstream CAD(cylindrical algebraic decomposition) task. The objective is to minimize the number of cells, a suitable metric that intuitively reflects CAD efficiency. The proposed GRL-SVP(UP/NUP) utilizes the inductive biases of GNNs to learn the relationships among the variables in the polynomial set and will output a variable order for CAD via the Actor-Critic algorithm.\n\nSummary:\nThe main novelty lies in the utilization of RL and GNN for the problem of suggesting variable order for CAD and brings the benefit of better empirical performance and generalization. It contributes to the field as the first work to try RL method for this task and it can be further improved by exploring how to encode polynomial coefficients as edge information, boost prediction time, etc. The inclusion of an interpretive analysis outlining the reasoning behind the variable order proposed by the RL approach would enrich the paper's contribution and reader's understanding.", "questions": "1. Could you clarify the role of polynomial coefficients within your proposed graph representation? Specifically, are these coefficients incorporated into the graph structure or the node embeddings? Furthermore, what is your perspective on the potential importance of these coefficients for determining optimal variable orderings?\n2. Could you elaborate on how GRL-SVO(UP) and GRL-SVO(NUP) are complementary to each other?", "limitations": "Yes, the author has adequately addressed limitations in the designated section.", "rating": 7, "confidence": 3, "soundness": 2, "presentation": 3, "contribution": 3, "strengths": "Pros:\n1. It effectively reframes the polynomial set as an associated graph, thereby capitalizing on the inherent advantages of GNNs such as permutation invariance and sparse input awareness. This approach may potentially unveil complex variable interrelationships that could otherwise be overlooked by traditional handcrafted heuristics.\n2. This study is the first to utilize reinforcement learning to treat this task as a reinforcement problem.\n3. Experimental results show compelling evidence for this method when compared to other heuristic methods in the past. And this approach exhibits good generalization when scaled to higher variable problems.\n4. The paper seems to be well-structured and provides sufficient detail about the experiments.", "weaknesses": "Cons:\n1. The associated graph representation may not fully capture all information about the polynomials such as the coefficients. It only encodes relationships between variables. This could be a limitation as the coefficients in a polynomial do carry significant mathematical information. \n2. The proposed approach doesn't significantly enhance the inference time compared to existing heuristics as in Figure 4c.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for the valuable feedback.\n```\nCould you clarify the role of polynomial coefficients within your proposed graph representation? Specifically, are these coefficients incorporated into the graph structure or the node embeddings? Furthermore, what is your perspective on the potential importance of these coefficients for determining optimal variable orderings?\n```\nIndeed, with regard to the choice of variable order, the current works do not consider coefficients (both Expert-Based or Learning-Based heuristics). Some experts in Symbolic Computation believe that the reason may be related to the calculation of CAD projection: CAD projection uses two polynomials to make a resultant (definition 1 in the Appendix) to eliminate a common variable, so it first depends on the common variable set of these two polynomials (which does not involve coefficients); secondly, the amount of calculation generally depends on the degree of public variables, because the degree determines the size of the resultant matrix. \nFor practical instances, the variation range of the coefficient is uncontrollable, which will increase the difficulty of Learning-Based design and training the neural network. \nThe impact of coefficients on the problem is complex. We are trying to provide some intuition through Figure 2 in the PDF attachment. \n- (a): $\\{ x^3y+4x^2+xy, -x^2+2xy-1 \\}, x \\prec y: 13, y \\prec x: 89$;\n- (b): $\\{ x^3y+8x^2+xy, -x^2+2xy-1 \\}, x \\prec y: 13, y \\prec x: 89$;\n- (c): $\\{ x^3y-4x^2+xy, -x^2+2xy-1 \\}, x \\prec y: 45, y \\prec x: 125$;\n- (d): $\\{ x^3y+4x^2+xy, x^2+2xy-1 \\}, x \\prec y: 29, y \\prec x: 101$;\n- (e): $\\{ -x^3y+4x^2+xy, -x^2+2xy-1 \\}, x \\prec y: 45, y \\prec x: 97$.\n\nThe number of cells of (a) and (b) are the same, while (c), (d), and (e) are different. But the best variable order is the same ($x \\prec y$) in these cases. To a certain extent in these cases, the coefficient mostly affects the number of cells.\n\nExperiment 4: We conduct an experiment on the coefficient and will append it to the Appendix. We have randomly modified the coefficient (in [-100, 100]) of 1000 instances randomly selected from the 3-var testing set. Since the coefficients were the only modification made, we used the original variable order generated from the unaltered instances. Our models continue to outperform other heuristics, as demonstrated by the results obtained.\n\n| | brown | triangular | EMLP | sotd | ndrr | gmods | GRL-SVO(NUP) | GRL-SVO(UP)|\n| --- | --- | --- | --- | --- | --- | --- | --- | --- |\n| #SI | 831 | 762 | 855 | 898 | 842 | 867 | 892 | **912** |\n| AVG.T | 155.42 | 212.50 | 125.54 | 79.73 | 141.29 | 100.30 | 79.96 | **64.89** |\n| AVG.N | 2380.67 | 2606.40 | 2353.11 | 2065.13 | 2288.08 | 2162.19 | 2100.57 | **2023.58** |\n\nWe also observe a slight decline in the performance of all heuristics, indicating that the coefficient plays a significant role as a parameter (although it may not be the most crucial one). Effectively analyzing coefficients poses a challenging problem, and we will endeavor to address this issue in the future.\n\n```\nCould you elaborate on how GRL-SVO(UP) and GRL-SVO(NUP) are complementary to each other?\n```\nWe will revise the unexplained description in the next version. It corresponds to a case where GRL-SVO encounters a large instance. Although GRL-SVO(UP) exhibits superior performance, it is time-consuming due to the involvement of projection and interaction with symbolic calculation tools. As a compromise, we can utilize GRL-SVO(UP) to predict the initial variables for the variable order, while employing GRL-SVO(NUP) for predicting the remaining variables, or vice versa. Alternatively, cross-invoking both methods can also be considered as a viable solution. In this particular case, they complement each other effectively.\n"}, {"review_id": "mh4BGhR6Da", "reviewer": "Reviewer_Ydm9", "summary": "Given a curve y = x^2, it partitions the x-y plane into three sets where the sign y-x^2 is the same. On the curve y-x^2 it is zero, above the curve y = x^2, sign is positive and below the curve it is negative. Thus the polynomial has 3 cells - regions where the sign is invariant.\nGiven a polynomial with n-variables there is a mathematical procedure (project, root-isolate and lift) to identify cells.  The mathematical procedure may results in different cells depending upon on how the variables are ordered. The objective is to choose a variable ordering in order to minimize the number of cells generated by the mathematical procedure.\n\nThe contribution of the paper is to formulate a graph representation of the problem (the state), the action is the variable permutation and the reward is minimizing the number of cells. The  REINFORCE algorithm is used.\n\n", "questions": "1. The performance improves very quickly according to Figure 4. Is there an explanation. How stable are the runs of REINFORCE ?", "limitations": "NA", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "1. It is nice to see that RL is being used for such problems. It is a nice and natural fit.\n2. The model is trained on 3-variable set but generalizes to upto 9 variable set. ", "weaknesses": "1. The novelty is on setting up the problem. There is not much RL novelty.\n2. REINFORCE has high variance. There should be more analysis of the impact of the algorithm on the solution.\n", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for the valuable feedback.\n\n```\nThe performance improves very quickly according to Figure 4. Is there an explanation. How stable are the runs of REINFORCE ?\n```\n\nAs an example, the brown heuristic (EB & NUP in Section 2.2) only utilizes three statistical features: degree, total degree, and occurrence to distinguish the importance of variables, where it can also achieve a good result. GRL-SVO(UP/NUP) focus on a superset of such heuristics. They have a greater probability to construct a relatively effective heuristic by organizing these features, and 3-var instances are relatively small and suitable for learning. Therefore, it is reasonable that the models have a quick improvement in the first few epochs.\n\nBesides, due to the quick improvement caused by the first epoch, the subsequent variations of metrics become very hard to see in Figure 4. We have redrawn the plots starting from the second epoch, referring to Figure 3 in the PDF attachment. It can be observed that REINFORCE exhibits some instability."}, {"review_id": "1MdzrROwux", "reviewer": "Reviewer_gZi1", "summary": "Cylindrical algebraic decomposition (CAD) is a technique to decompose a multi-dimensional space into a finite number of cells. CAD cells are built to respect a set of polynomial constraints such that each constraint has constant truth value in each cell. As stated by the authors, the variable ordering in the CAD algorithm significantly influences the computational time, memory usage, and the number of cells. The authors used Reinforcement Learning based approaches to choose an optimal variable ordering. The authors represented a polynomial set in a graph, in addition to the embeddings formed with different indicators of each polynomial (e.g. degree statistics ), and used the number of obtained cells as a quality measure of the result. The authors used the Advantage Actor-Critic (A2C) framework to improve CAD by suggesting a better variable order. The actor neural network was represented by Graph Neural Network as they are permutation invariant.", "questions": "- What is the used architecture of the GNN? The authors mentioned “GraphConv” and cited the paper [26]. I didn’t see how the two are related to each other. If you are referring to the layer “GraphConv” in the DGL library, the adequate name in the paper is “Garph Convolution Network layer [Kipf and Welling 2017]”.\n- Also, the paper [26] is more a method to enhance the expressiveness of a GNN rather than a GNN architecture.", "limitations": "- The authors mentioned the limitations of their approaches in section 5.", "rating": 5, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- Reinforcement Learning methods are widely adopted to optimize non-differentiable objectives, and the authors demonstrate its potential in choosing the variable order for CAD algorithms .\n- The experimental results demonstrate that their method outperforms the baseline.", "weaknesses": "The paper lacks some ablation studies.\n- The advantage of using a GNN and a graph representation of polynomial sets: The authors mentioned that GNNs are invariant to permutation, the results should indeed be independent from the order of the polynomial in the set, but there are simpler Neural Network that are invariant to permutation. Can we empirically check how much a GNN enhances the performance of GRL-SVO? To check this, the authors can for instance replace the GNN with an MLP performed on each polynomial embedding and then do a mean aggregation to have a learnable representation of the whole polynomial set.\n- I would also encourage authors to test different GNN architectures (e.g. GAT, GATv2, GraphSage ...) for the ablation study. \n- What is the effect of normalization factor “M” on the performance and speed of GRL-SVO?\n- More experiments should be carried out to assess robustness. \n- Code not shared to verify results.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for the feedback and valuable comments. \n\n```\nCan we empirically check how much a GNN enhances the performance of GRL-SVO? To check this, the authors can for instance replace the GNN with an MLP performed on each polynomial embedding and then do a mean aggregation to have a learnable representation of the whole polynomial set.\n```\nGRL-SVO(UP/NUP) accepts the set of variable embeddings, and then GNNs encode the variable embedding into intermediate learnable representations. The actor makes decisions based on this information. We think utilizing polynomial embedding seems to be a new task different from our work. We have conducted an experiment on a simple neural network with MLP layers for nodes without edges. The MLP layer will convert variable embeddings (not polynomial embedding) into their learnable representations. It is also invariant to permutation. It is Experiment 2 (NO_EDGE(MLP) in Table 2 and Figure 1 in PDF attachment) in the response for reviewer HXCT. We will append it to the Appendix. \n\nThe main result is that GRL-SVO can outperform these MLP models with different sizes. It is the advantage of the graph structure where a variable can grasp neighbor information.\n\nCombining our work with polynomial embedding for suggesting variable order is also a promising direction, we will investigate it in the future.\n\n```\nI would also encourage authors to test different GNN architectures (e.g. GAT, GATv2, GraphSage ...) for the ablation study.\n```\n\nWe have arranged experiments on different GNN architectures and will append the results to the Appendix. While the experiments are still ongoing, we have included a subset of the complete experiments on GraphSage in Table 3, which can be found in the PDF attachment.\n\n```\nWhat is the effect of normalization factor $M$ on the performance and speed of GRL-SVO?\n```\nExperiment 6: We make an ablation experiment on $M$ and will append it to the Appendix. We train the models with $M$=10000, 20000, 50000(ours), 100000, and without $M$. Note that if there is no $M$, the reward (the number of cells) will be a relatively large integer. As shown in Table 4, $M$ is necessary. The first number is the result of the validation set, while the second is the result of the testing set.\n\n```\nCode not shared to verify results.\n```\nWe have submitted our source code to AC. We will clean and release the source code and dataset for the experiments in this paper on GitHub. \n\n```\nWhat is the used architecture of the GNN? The authors mentioned ''GraphConv'' and cited the paper [26]. I didn’t see how the two are related to each other. If you are referring to the layer ''GraphConv'' in the DGL library, the adequate name in the paper is ''Graph Convolution Network layer [Kipf and Welling 2017]''.\nAlso, the paper [26] is more a method to enhance the expressiveness of a GNN rather than a GNN architecture.\n```\n\nWe apologize for the confusion and will revise it in the next version. \nFirst, we utilize PyTorch Geometric (PyG) for the implementation in Section 4.1, not the DGL library. There is a difference between the names of the two libraries.\nSecond, The operator of GraphConv in PyG is $\\mathbf{x}^{\\prime} _i = \\mathbf{W} _1 \\mathbf{x} _i + \\mathbf{W} _2 \\sum _{j \\in \\mathcal{N}(i)} e _{j,i} \\cdot \\mathbf{x} _j$. As there is no edge weight in our models, actually the operator we use is $\\mathbf{x}^{\\prime} _i = \\mathbf{W} _1 \\mathbf{x} _i + \\mathbf{W} _2 \\sum _{j \\in \\mathcal{N}(i)} \\mathbf{x} _j$. Note that a basic GNN model has the (5.7) formula (basic GNN model) in section 5.1.3 of the book ''Graph Representation Learning'' by William L. Hamilton. $$\n\\mathbf{h}^{(k)} _u = \\sigma(\\mathbf{W}^{(k)} _{self} \\mathbf{h}^{(k-1)} _u + \\mathbf{W}^{(k)} _{neigh} \n\\sum _{v \\in \\mathcal{N}(u)} \\mathbf{h}^{(k-1)} _v + b^{(k)})\n$$ Our model is a simple instance of a basic GNN model where $\\sigma = relu$, $\\mathcal{N}$ means the nodes connecting to $u$, and $\\mathbf{W}^{(k)} _{self}$ and $\\mathbf{W}^{(k)} _{neigh}$ are all learnable parameters. \nWe will revise the citation [26] to (5.7) in ''Graph Representation Learning'' as we used and write down the used GNN formula in the paper.\n"}]

Author rebuttal:
We would like to express our sincere gratitude for the reviewers' valuable feedbacks, which are quite helpful to enhance the quality and clarity of our work. We have designed some experiments and attempted to complete them as many as possible during this short period. We will add the missing experiments that the reviewers are concerned about to the Appendix. The PDF attachment contains some tables and figures. 

**Notes on Additional Experiments** 
If not specified otherwise, all models are trained on the 3-var set in 10 epochs. The best model parameters are selected on the 3-var validation set, and the models are tested on the 3-var testing set. GRL-SVO (UP/NUP) are the models trained in 10 epochs for fair comparison. The performance of GRL-SVO(NUP) and GRL-SVO(UP) for 3-var testing set in 10 epoches are #SI = 1765, AVG.T = 97.78, AVG.N = 2142.98; #SI = 1794, AVG.T = 79.57, AVG.N = 2075.23, respectively. 

Meta-review: The reviewers agreed the proposed two algorithms, GRL-SVO(UP) and GRL-SVO(NUP), utilizing the techniques in RL and GNN to optimize the number of cells of CAD problem for a certain variable order, are creative and worth investigating. The empirical results are also solid. I recommend the paper be accepted. Please incorporate the reviewers' suggestions as promised.
Decision: Accept (poster)