key: cord-0047187-8rya30w9 authors: Chen, Changbo; Zhu, Zhangpeng; Chi, Haoyu title: Variable Ordering Selection for Cylindrical Algebraic Decomposition with Artificial Neural Networks date: 2020-06-06 journal: Mathematical Software - ICMS 2020 DOI: 10.1007/978-3-030-52200-1_28 sha: b09234eeec153615bc2fdc71270e7ec5c7b0e9a2 doc_id: 47187 cord_uid: 8rya30w9 Cylindrical algebraic decomposition (CAD) is a fundamental tool in computational real algebraic geometry. Previous studies have shown that machine learning (ML) based approaches may outperform traditional heuristic ones on selecting the best variable ordering when the number of variables [Formula: see text]. One main challenge for handling the general case is the exponential explosion of number of different orderings when n increases. In this paper, we propose an iterative method for generating candidate variable orderings and an ML approach for selecting the best ordering from them via learning neural network classifiers. Experimentations show that this approach outperforms heuristic ones for [Formula: see text]. Cylindrical algebraic decomposition (CAD) was introduced by Collins for solving real quantifier elimination problems [14] . The original framework for computing CAD introduced by Collins is based on a projection and lifting scheme, which has now been gradually improved by many others [1, 3, 5, [19] [20] [21] [22] [23] . In 2009, Moreno Maza, Xia, Yang and the first author [13] proposed a new way for computing CAD, which first computes a cylindrical decomposition of complex space and then transforms it into a CAD of real space based on the technique of triangular decompositions and regular chains [13] . Its efficiency was substantially improved in [7] based on an incremental algorithm, which can also take advantage of equational constraints. A complete and efficient algorithm for real quantifier elimination based on it was proposed in [12] . Moreover, it can utilize disjunctive equational constraints via computing a truth table invariant CAD [2] . Today, despite of its doubly exponential complexity [6, 14] , CAD has been efficiently implemented in many softwares such as QEPCAD, Mathematica, RED-LOG and Maple, and found wide applications in geometry theorem proving, stability analysis of dynamical systems, control system design, verification of hybrid systems, program verification, nonlinear optimization, automatic parallelization, and so on. Recently, it also finds applications on studying quantum nonlocality [8] . The choice of variable ordering has been shown to have a great impact on the performance of CAD, both theoretically [6] and in practice [15] . Several heuristic methods for variable ordering selection have been proposed. In particular, two heuristic strategies [4, 9] are implemented in the SuggestVariableOrder (SVO) command of the RegularChains library in Maple. On the other hand, it also becomes a natural option to predict the best variable ordering by the approaches of artificial intelligence, among which machine learning is a natural choice [16] [17] [18] 24, 25] . Existing work for selecting variable ordering by machine learning focus on the trivariate case. For more than three variables, it becomes more difficult to obtain sufficient labelled data due to the doubly exponential behavior of CAD in terms of the number of variables n. Another difficulty is the exponential explosion of number of different orderings when n increases. In this paper, we first propose an iterative approach for generating a better variable ordering starting from the one given by SVO. Then we reduce the potential n! number of classes to predict for the variable ordering problem to n by training a neural network classifier with data generated by the iterative approach. Experiments show that both the iterative approach and the machine learning approach outperform SVO for n = 4, 5, 6. The organization of the paper is as follows. In Sect. 2, we briefly review the concept of CAD and the problem of variable ordering selection. In Sect. 3 and Sect. 4, we present respectively the iterative and the machine learning approaches. In Sect. 5, we show the effectiveness of our approaches by experimentation. Finally, we draw the conclusion in Sect. 6. Consider a set of polynomials F ⊂ Q[x 1 , . . . , x n ] and a variable ordering x i1 > · · · > x in . An F -invariant cylindrical algebraic decomposition (CAD) partitions R n into disjoint and cylindrically arranged semi-algebraic subsets (called cells) such that the projection of any two cells onto R k (with coordinate variables x i n−k+1 , . . . , x in ), 1 ≤ k ≤ n − 1, is either disjoint or identically equal. The variable ordering also specifies the order to eliminate variables and the order to construct CAD from projection factors or a complex cylindrical decomposition. The algorithms presented in [2, 10, 13] for computing CADs based on regular chains have been implemented in the command CylindricalAlgebraicDecompose in the RegularChains library of Maple [11] . Its latest version is available from http://www.regularchains.org and we use the version from http://www. arcnl.org/cchen/software/cadorder. In the RegularChains library, the command SuggestVariableOrder (SVO for short) implements two different heuristic methods for variable ordering selection, namely the one by Brown [4] (with option "decomposition = cad", SVO(B) for short) and the one by Chen et al. [9] (default option, SVO(C) for short). The variable ordering plays an important role in the efficiency of computing CAD, as illustrated by the following example. Table 1 lists the computation times and number of cells for several variable orders. As we can see, for this example, current heuristic methods avoid picking the worst variable order, but also miss the best variable order. In this section, we present an iterative variable ordering selection method, called IVO, for cylindrical algebraic decomposition. It starts with an initial ordering x i1 > x i2 > · · · > x in provided by SVO. Then it calls a subroutine, called RVO, to generate n orderings in a round-robin manner and picks the best by calculating the shortest time of computing CAD with them. Next, it fixes the largest variable and calls RVO again on the rest ones to select the second largest variable, and so on. Precise description of IVO and RVO are given as below. We denote by || the concatenation of two sequences. -Algorithm RVO. , Q (i) = Q and record the running times. 4. Compare these running times with t and return the shortest one and the corresponding order. -Algorithm IVO. -Input: a set of polynomials F ; a sequence of variables X. -Output: a permutation of X, which defines a descending variable order. -Steps: 1. If X ≤ 1, return X. It is easy to see that IVO calls CAD at most 2 + n k=1 (k − 1) = (n 2 − n + 2)/2 times. In the rest of this paper, if no confusion arises, we denote by SVO(*) an oracle that always returns the better ordering between SVO(B) and SVO(C) and by SVO either of the three. To train a useful machine learning model for predicting the best variable ordering for CAD, it is important to have a dataset of enough labelled examples and the size of the dataset cannot be too small. On the other hand, since computing CAD is expensive when the number of variables is larger than 3, a larger dataset demands more computing resources. To make the learned model useful, it is better that the training dataset contains diverse examples. On the other hand, if the data are too diverse, it will be hard to learn. The following table summarizes the information of the dataset we generate using random polynomials as input to IVO. The whole dataset is divided into three datasets, used respectively for training, validation and testing with ratio 9/1/1. The validation dataset is used for tuning the machine learning model while the testing dataset is treated as unseen data used only once for reporting experimental results in the paper and showing the generalization ability of the ML model. The data in Table 2 were generated on a cluster (4 compute nodes, each of which has two Intel E5-2620 CPU (6-core each) and 64 GB memory). On each node, 6 Maple sessions were run in parallel. The time limit is set as 15 min. The total time for generating the dataset is about 1 month. In Table 2 , we only record the number of valid examples. An example is valid if CAD finishes the computation within the time limit for at least one ordering computed by IVO. Note that it is possible that SVO returns an ordering for which CAD times out. Next, we recall the features to represent the polynomials introduced in our earlier work [24] . These features are generated based on a graph structure defined for polynomial systems. For a given variable x i , i = 1, . . . , n, an equivalent description of the features is summarized in the following Table 3 . Let E(i) be the features associated with x i . Then the feature vector E = ∪ n i=1 E(i). {deg(lc(f, xi) )}, where lc denotes for leading coefficient We aim to train a model which can predict variable orders for n = 4, 5, 6. Instead of treating a variable order as a class, which may lead to huge number of classes for a fixed n, we would like to train a multiclass classifier M n , which only predicts the largest variable in an ordering. To achieve this, for each example in the dataset, we will call SVO to return an initial ordering, and then call RVO once to get a hopefully better ordering. Then the first variable in the ordering Fig. 1 . The neural network classifier is set as the label of the example. For each n = 4, 5, 6, we train an artificial neural network classification model implemented in TensorFlow. The structure and parameters of the neural network are illustrated in Fig. 1 . Each M n is a full-connected neural network with one input layer, three hidden layers and one softmax output layer. The activation function used is ReLu. Hyperparameters of the network are hand-tuned to maximize validation accuracy. Suppose that we have obtained the well-trained models M n , n = 4, 5, 6. We then employ the following procedure PVO to predict the variable ordering. -Algorithm PVO -Input: a set of polynomials F ; a sequence of n variables X. -Output: a permutation of X, which defines a descending variable order. The overall training and predicting process is depicted in Fig. 2 . In this section, we report on the experimental results of the iterative method and the machine learning approach for selecting variable orderings. Note that when we call PVO to predict the variable ordering, we have three options. One can use SVO(B) or SVO(C) to get an initial ordering without calling CAD. Or one can use SVO(*) to get the better one between SVO(B) and SVO(C), but this requires calling CAD twice. Nevertheless, for a = B, C, * , we use IVO(a), RVO(a) and PVO(a) to denote the iterative method, the first iteration of the iterative method and the ML-based method for variable ordering selection which uses SVO(a) as an initial ordering. As a result, the testing dataset for a = B, C, * is respectively the set of examples, for which SVO(a) provides the initial ordering in the original testing dataset. Table 4 summarizes the size of the datasets. Note that the dataset for a = C does not contain timeout examples. This is because whenever CAD times out with the ordering given by SVO(C), IVO will use the ordering given by SVO(B). Although the testing datasets and inference procedures for a = B and a = C are different, for a given n, both a = B and a = C use the same classifier trained with the dataset in Table 2 , where the examples are labelled by RVO(*) with an initial variable ordering provided by SVO(*). Table 5 summarizes the average computation times (in seconds) and timeout rates of IVO(*) and RVO(*) for the whole datasets. Note that the datasets only contain examples on which IVO(*) succeeds. Figure 3 summarizes the accuracies of six ordering selecting methods. Here the ground truth for SVO(a) and PVO(a) is given by RVO(a), for a = B, C, * . The accuracy is defined as the percentage of best orderings chosen by each method over the total number of test examples, given in Table 4 . We observe that the accuracy of PVO(a) is higher than SVO(a) for n = 5, 6, for all a = B, C, * . For n = 4, the accuracy of PVO(a) is slightly lower than SVO(a) for a = C, * and higher than SVO(a) for a = B. Figure 4 provides the average running time of CAD with the variable orderings predicted by different methods. If there is a timeout, the time is counted as twice the time limit, that is half an hour. For n = 4, 5, 6 and a = * , B, the average computation time of PVO(a) is considerably less than SVO(a). The average computation time of PVO(C) is less than SVO(C) for n = 4, 6 but greater than SVO(C) for n = 5. In this paper, we propose a machine learning based approach for predicting the best variable ordering for CAD targeting on n > 3. The experiments show that it outperforms traditional heuristic approaches for n = 4, 5, 6 on randomly generated datasets. The CylindricalAlgebebraicDecompose command can compute CAD for even larger n, say n ≤ 10 in reasonable time if there are several equational constraints in the system [7] . It will be interesting to extend the model for n > 6, test it on CAD-QE problems from real applications and finally make the ML-based variable ordering selection method a useful option for Suggest-VariableOrder. The data and code used in this paper is available at http://doi. org/10.5281/zenodo.3818086. Cylindrical algebraic decomposition I: the basic algorithm Truth table invariant cylindrical algebraic decomposition by regular chains Truth table invariant cylindrical algebraic decomposition Tutorial: Cylindrical algebraic decomposition Improved projection for cylindrical algebraic decomposition The complexity of quantifier elimination and cylindrical algebraic decomposition An incremental algorithm for computing cylindrical algebraic decompositions Mapping criteria between nonlocality and steerability in qudit-qubit systems and between steerability and entanglement in qubit-qudit systems Solving semi-algebraic systems with the RegularChains library in Maple Algorithms for computing triangular decomposition of polynomial systems Cylindrical algebraic decomposition in the RegularChains library Quantifier elimination by cylindrical algebraic decomposition based on regular chains Computing cylindrical algebraic decomposition via triangular decomposition Quantifier elimination for real closed fields by cylindrical algebraic decompostion Efficient projection orders for CAD Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition Improved cross-validation for classifiers that make algorithmic choices to minimise runtime without compromising output correctness Using machine learning to improve cylindrical algebraic decomposition An improved projection for cylindrical algebraic decomposition Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation Validity proof of Lazard's method for CAD construction Solving systems of strict polynomial inequalities Cylindrical algebraic decomposition using validated numerics Variable order selection for cylindrical algebraic decomposition based on machine learning Variable ordering selection for cylindrical algebraic decomposition based on a hierarchical neural network Acknowledgments. The authors would like to thank anonymous referees for helpful comments. This research was supported by NSFC (11771421, 11671377, 61572024), CAS "Light of West China" Program, the Key Research Program of Frontier Sciences of CAS (QYZDB-SSW-SYS026), and cstc2018jcyj-yszxX0002 of Chongqing.