The algorithms employed by our communities are often underspecified, and thus have multiple implementation choices, which do not efect the correctness of the output, but do impact the eficiency or even tractability of its production. In this extended abstract, to accompany a keynote talk at the 2021 SC-Square Workshop, we survey recent work (both the author's and from the literature) on the use of Machine Learning technology to improve algorithms of interest to SC-Square.
A Cylindrical Algebraic Decomposition (CAD) is a decomposition of ordered R space into cells arranged cylindrically, meaning the projections of cells are all arranged within cylinders. The cells are (semi)-algebraic meaning each may be described by a finite sequence of polynomial constraints. A CAD is usually produced for a set of polynomials such that each polynomial has constant sign on each cell. This allows us to query a finite set of sample points to understand the behaviour of the polynomials (or logical formula involving them) everywhere.
The most important application of CAD is to perform Quantifier Elimination (QE) over the
reals: given a quantified formula, find an equivalent quantifier-free formula. E.g., QE would
transform ∃, 2 + + = 0 ∧ ̸= 0 into the equivalent 2 − 4 ≥ 0. Although CAD
emerged in the Symbolic Computation community, since SAT is a sub-problem of QE, it can
be used to tackle problems in the NRA and QF_NRA logics of the SMT-LIB. Adaptations of the
original CAD algorithm have been designed for use in SMT [25], [27], [
CAD was introduced in 1975 [11] and is still an active area of research: for a deeper introduction see, for example, the background section of [15].
CAD requires a variable ordering. For QE the ordering must match the quantification, but
variables in blocks of the same quantifier and the free variables can be swapped. So in the
example above we must decompose (, , , )-space with last, but the other variables can
be in any order. The ordering can have a great efect on the time / memory use of CAD, the
number of cells, and even the underlying complexity [
The 2014 work choose between existing heuristics, in order to fix the number of classes. However,
there were many problems in the dataset where none of those heuristics gave an optimal choice.
So we revisited these experiments for CICM 2019 [17] this time allowing ML to predict the
optimal ordering directly (fixing the number of variables and thus classes). We explored a
variety of ML classification methods available in Python’s sklearn library [34]: K-nearest
neighbour classifiers, multi-layer perceptions, decision trees, and support vector machines.
We used the CAD implementation in Maple’s Regular Chains Library [
The first step to use such an ML classification model is to represent the input (in our case a
set of polynomials) as a vector of floating point numbers: the features. In [24] and [17] we
used measures of degree and frequency of occurrence for each variable, inspired by [
Metrics for judging a CAD variable ordering choice should correspond to CAD runtime1. The prior work trained ML classifiers to pick the ordering with minimal runtime for a problem, with selections deemed accurate only if that optimal ordering was chosen. However, this meant that ML training does not distinguish between diferent non-optimal orderings, even though the diferences are often huge. For MACIS 2019 [ 19] we used an alternative definition of an accurate choice: one leading to a runtime within % of the minimum. We then wrote a new version of the sklearn cross-validation procedure to select model hyper-parameters to minimise CAD runtime of the choices, rather than maximising the number of times the ordering that gives the minimal time for a problem is taken. This improved the performance of all ML models. Note that the new accuracy definition and procedure are suitable for any classification where we are seeking to have ML make a choice to minimise computation time.
For ICMS 2020 [20] we presented a software pipeline that implements our work described in the previous sub-sections. Given two datasets (training and testing) the pipeline automates: generation of CAD runtimes for each set of polynomials under each admissible variable ordering; using the runtimes from the training dataset to select the hyper-parameters with cross-validation and tune the parameters of the ML models; and evaluating the performance of those classifiers on the testing dataset. The pipeline could be used to pick the variable ordering for other algorithms which take sets of polynomials as input by changing the calls to Maple’s CAD procedure with those of another implementation / algorithm. The code is freely available at: https://doi.org/10.5281/zenodo.3731703.
We experimented on the SMT-LIB benchmarks2 which are mostly real-world applications and extracted two datasets of 3 and 4 variable problems that could be tackled by CAD. On our 3-variable dataset human-made heuristics achieved runtimes 27% above the minimum and ML achieved runtimes 6% above. So here, the ML classifiers ofer close to optimal performance.
However, on the 4-variable dataset ML achieved runtime 67% above the minimum (compared to 98% above for human-made heuristics) and so there is room for improvement. Of course, with 4 variables this is a much harder classification problem (24 orderings rather than 6).
To inspire further progress we next consider related work in the literature.
The methodology of [24] was applied later to decide the order of sub-formulae solving in [26] and whether to precondition CAD input in [23].
Two more recent works with alternative methodologies are [10] to choose CAD variable
ordering and [
Applications of ML elsewhere in Computer Algebra are fairly rare3 but the following recent one may ofer a blueprint for progress.
Buchbergers’ Algorithm to produce a Gröbner Basis [
In [35] the authors described how an Agent could be trained to make this decision using reinforcement learning: where instead of having a labelled dataset an Agent makes a decision and receives a reward that informs future decisions. In [35] the Agent chooses an -Pair and received a reward based on the number of polynomial additions required4.
The study ensures a constant size of polynomial by studying only binomials (so no term swell) and working in a modular coeficient field (so no coeficient swell). They can then represent polynomials to a neural network via consistently sized exponent vectors. Similar to our work in Section 2, this allows the network to judge sparsity and degree but not the actual coeficients (to avoid over-fitting). 3We note the early example in [29] which uses a Monte-Carlo tree search to find the representation of polynomials that are most eficient to evaluate. 4Actually, the reward is based on the number of polynomial additions required to complete a full run of Buchberger’s algorithm after selecting that -Pair and continuing with a an existing heuristic. The rationale for this given is to reduce variability but it seems equally compelling for allowing the Agent to judge the efects of a choice not just on the next step but on the remainder of the algorithm. This does however greatly increase the training cost.
The experiments in [35] are run on separate distributions of random polynomials based on the number of variables, generators, and degree. The Agent significantly outperformed the established strategies on such data, but the performance on real problems remains to be observed.
Most interestingly, some simple components of the Agent’s strategy were observed such as a preference for pairs whose -polynomials are monomials and a preference for pairs whose -polynomials are low degree. Such strategies had never been studied5 and when used alone outperform the established heuristics.
There has been recent work on the use of ML to predict the outcome of algebraic computations directly. Most notably, in [30] the authors predict the output of symbolic integration and the symbolic solutions to first and second order ordinary diferential equations using neural networks6. Their experiments outperform various CASs, in the sense that the model predicts correct outcomes for examples where the CAS times out. However, we note that from the viewpoint of a CAS developer the cases where the model predicts the wrong model would be more critical than the timeouts7. We also note the recent preprint [28] which repeats the study to make the argument that better generalisability will be achieved with a learning model based on the relative positions of mathematical symbols rather than the absolute positions. These are very diferent applications of ML to the algorithm optimisation we are interested in, but lessons on how best to represent symbolic data to ML tools may well be transferable.
An early use of ML in Satisfiability Checking was the development of the portfolio solver SATZilla [39]. There is rarely a single dominant SAT solver for all problems, so SATZilla uses ML to predict which solver to use for a given instance. This inspired the recent MachSMT which selects algorithms for SMT-solvers [36] using Principal Component Analysis for dimensionality reduction.
The core algorithm of Satisfiability Checking, CDCL [ 33], allows us to proceed through the exponential search space in an intelligent manner: generalising from the conflicts uncovered at a specific sample to rule out additional branches. However, even with this conflict learning, there are decisions in the search that must be taken without guidance and poor luck can lead a search to an unproductive area, motivating for example the use of restarts.
Thus CDCL itself has potential to be guided by ML. For example: • [38] makes the choice of initial value to variable allocation to begin the search using a regression model that predicted satisfiability of formulae after fixing the values of a certain fraction of the variables. 5Perhaps because -polynomials are rarely examined before being reduced. 6Specifically seq2seq models more typically used in natural language processing: for example they view integration as translating from integrands to integrals 7The review [12] ofer some other qualifications on the claim of superiority over CASs.
• [32] uses machine learning to determine a policy for restarts in SAT-solvers: ML is used to predict the quality of the next learnt clause based on previously learnt clauses; restarting when the quality is predicted below a threshold. • NeuroSAT [37] can predict unsatisfiable cores (subsets of the constraints that cannot be satisfied together) to inform variable selection in the search.
The MapleSAT solver introduced and utilises the learning rate, the propensity for variables to generate learnt clauses, as a key metric for making decisions and the rfist to outperform the previously dominant VSIDS heuristic.
In [31] they view the question of branching in SAT-solving (selecting the next variable in the search) as an optimisation problem to maximize this metric. In particular, they apply reinforcement learning, where the learning rate informs the reward function. Variable selection is modelled in the multi-armed bandit (MAB) framework and tackled using a well known MAB algorithm. This led MapleSAT to victory in the annual SAT competition8.
Finally, we note also the use of supervised ML to predict mathematical properties elsewhere in mathematics, where the primary motivation is the formation of new conjectures. We refer to the survey [22] which includes examples in algebraic geometry, representation theory, combinatorics and number theory, in which most applications are expressed as ML classification problems.
There is huge potential to apply ML to algorithms of interest to SC-Square. The author’s own experience in Section 2 shows the potential benefits.
However, our experience using ML classification has clear limits. Such supervised learning requires labelled datasets. Although in theory infinite symbolic data could be manufactured, in practice it would be computationally infeasible to label all that data. A reinforcement learning approach such as for the examples in Sections 3.2 and 3.5 looks far more promising.
Still unclear is the optimal way to represent symbolic data for ML tools, and how best to generate training data so maximise generalisation onto the problems of interest in the real world. Such questions deserve more focussed study. 8https://baldur.iti.kit.edu/sat-competition-2016/index.php?cat=results The author’s work surveyed in Sections 2.3− 2.7 was joint with Dorian Florescu, and funded by EPSRC Project EP/R019622/1: Embedding Machine Learning within Quantifier Elimination Procedures. The author is now supported by EPSRC Project EP/T015748/1: Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition.
We thank the reviewer of this paper, and the reviewers of the author’s surveyed work, for
useful comments. We thank the DEWCAD Journal Club for interesting discussions on some of
the other papers.
based on regular chains. Journal of Symbolic Computation 75, 74–93 (2016), https://doi.
org/10.1016/j.jsc.2015.11.008
[10] Chen, C., Zhu, Z., Chi, H.: Variable ordering selection for cylindrical algebraic
decomposition with artificial neural networks. In: Bigatti, A., Carette, J., Davenport, J.H.,
Joswig, M., de Wolf, T. (eds.) Mathematical Software – ICMS 2020. Lecture Notes in
Computer Science, vol. 12097, pp. 281–291. Springer International Publishing (2020),
https://doi.org/10.1007/978-3-030-52200-1_28
[11] Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic
decomposition. In: Proceedings of the 2nd GI Conference on Automata Theory and
Formal Languages. pp. 134–183. Springer-Verlag (reprinted in the collection [
ISSAC ’04, ACM (2004), https://doi.org/10.1145/1005285.1005303 [15] England, M., Bradford, R., Davenport, J.H.: Cylindrical algebraic decomposition with equational constraints. Journal of Symbolic Computation 100, 38–71 (2020), https://doi. org/10.1016/j.jsc.2019.07.019 [16] England, M., Bradford, R., Davenport, J.H., Wilson, D.: Choosing a variable ordering for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition. In: Hong, H., Yap, C. (eds.) Mathematical Software – ICMS 2014. Lecture Notes in Computer Science, vol. 8592, pp. 450–457. Springer Heidelberg (2014), http: //dx.doi.org/10.1007/978-3-662-44199-2_68 [17] England, M., Florescu, D.: Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti, C.C. (eds.) Intelligent Computer Mathematics. Lecture Notes in Computer Science, vol. 11617, pp. 93–108. Springer International Publishing (2019), https://doi.org/ 10.1007/978-3-030-23250-4_7 [18] Florescu, D., England, M.: Algorithmically generating new algebraic features of polynomial systems for machine learning. In: Abbott, J., Griggio, A. (eds.) Proceedings of the 4th Workshop on Satisfiability Checking and Symbolic Computation ( SC2 2019). No. 2460 in CEUR Workshop Proceedings (2019), http://ceur-ws.org/Vol-2460/ [19] Florescu, D., England, M.: Improved cross-validation for classifiers that make algorithmic choices to minimise runtime without compromising output correctness. In: Slamanig, D., Tsigaridas, E., Zafeirakopoulos, Z. (eds.) Mathematical Aspects of Computer and Information Sciences (Proc. MACIS ’19). Lecture Notes in Computer Science, vol. 11989, pp. 341–356.
Springer International Publishing (2020), https://doi.org/10.1007/978-3-030-43120-4_27 [20] Florescu, D., England, M.: A machine learning based software pipeline to pick the variable ordering for algorithms with polynomial inputs. In: Bigatti, A., Carette, J., Davenport, J.H., Joswig, M., de Wolf, T. (eds.) Mathematical Software – ICMS 2020. Lecture Notes in Computer Science, vol. 12097, pp. 302–322. Springer International Publishing (2020), https://doi.org/10.1007/978-3-030-52200-1_30 [21] Giovini, A., Mora, T., Niesi, G., Robbiano, L., Traverso, C.: One sugar cube, please; or selection strategies in the Buchberger algorithm. In: Proceedings of the 1991 International Symposium on Symbolic and Algebraic Computation. pp. 49–54. ISSAC ’91, ACM (1991), https://doi.org/10.1145/120694.120701 [22] He, Y.H.: Machine-learning mathematical structures. International Journal of Data Science in the Mathematical Sciences 1(1), 1–25 (2022), https://doi.org/10.1142/S2810939222500010 [23] Huang, Z., England, M., Wilson, D., Bridge, J., Davenport, J.H., Paulson, L.: Using machine learning to improve cylindrical algebraic decomposition. Mathematics in Computer Science 13(4), 461–488 (2019), https://doi.org/10.1007/s11786-019-00394-8 [24] Huang, Z., England, M., Wilson, D., Davenport, J.H., Paulson, L., Bridge, J.: Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) Intelligent Computer Mathematics, Lecture Notes in Artificial Intelligence, vol. 8543, pp. 92–107. Springer International (2014), http://dx.doi.org/10.1007/ 978-3-319-08434-3_8 [25] Jovanovic, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning: 6th International Joint Conference (IJCAR), Lecture Notes in Computer Science, vol. 7364, pp. 339–354. Springer (2012), https://doi.org/10.1007/ 978-3-642-31365-3_27 [26] Kobayashi, M., Iwane, H., Matsuzaki, T., Anai, H.: Eficient subformula orders for real quantifier elimination of non-prenex formulas. In: Kotsireas, S.I., Rump, M.S., Yap, K.C. (eds.) Mathematical Aspects of Computer and Information Sciences (MACIS ’15). Lecture Notes in Computer Science, vol. 9582, pp. 236–251. Springer International Publishing (2016), https://doi.org/10.1007/978-3-319-32859-1_21 [27] Kremer, G., Ábrahám, E.: Fully incremental CAD. Journal of Symbolic Computation 100, 11–37 (2020), https://doi.org/10.1016/j.jsc.2019.07.018 [28] Kubota, H., Tokuoka, Y., Yamada, T.G., Funahashi, A.: Symbolic integration by integrating learning models with diferent strengths and weaknesses. IEEE Access 10, 47000–47010 (2022), https://doi.org/10.1109/ACCESS.2022.3171329 [29] Kuipers, J., Ueda, T., Vermaseren, J.A.M.: Code optimization in FORM. Computer Physics
Communications 189, 1–19 (2015), https://doi.org/10.1016/j.cpc.2014.08.008 [30] Lample, G., Charton, D.: Deep learning for symbolic mathematics. In: Mohamed, S., White, M., Cho, K., Song, D. (eds.) Eighth International Conference on Learning Representations (ICLR 2020) (2020), https://iclr.cc/virtual_2020/poster_S1eZYeHFDS.html [31] Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Creignou, N., Le Berre, D. (eds.) Theory and Applications of Satisfiability Testing – SAT 2016, Lecture Notes in Computer Science, vol. 9710, pp. 123–140. Springer International Publishing (2016), https://doi.org/10.1007/978-3-319-40970-2_9 [32] Liang, J.H., Oh, C., Mathew, M., Thomas, C., Li, C., Ganesh, V.: Machine learning-based restart policy for CDCL SAT solvers. In: Beyersdorf, O., Wintersteiger, C.M. (eds.) Theory and Applications of Satisfiability Testing – SAT 2018, Lecture Notes in Computer Science, vol. 10929, pp. 94–110. Springer International Publishing (2018), https://doi.org/10.1007/ 978-3-319-94144-8_6 [33] Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. Computers, IEEE Transactions on 48(5), 506–521 (1999), https://doi.org/10.1109/12. 769433 [34] Pedregosa, F., Varoquaux, G., Gramfort, A., Michel, V., Thirion, B., Grisel, O., Blondel, M., Prettenhofer, P., Weiss, R., Dubourg, V., Vanderplas, J., Passos, A., Cournapeau, D., Brucher, M., Perrot, M., Duchesnay, E.: Scikit-learn: Machine learning in Python. Journal of Machine Learning Research 12, 2825–2830 (2011), http://www.jmlr.org/papers/v12/ pedregosa11a.html [35] Peifer, D., Stillman, M., Halpern-Leistner, D.: Learning selection strategies in Buchberger’s algorithm. In: Daumé III, H., Singh, A. (eds.) Proceedings of the 37th International Conference on Machine Learning (ICML 2020). Proceedings of Machine Learning Research, vol. 119, pp. 7575–7585. PMLR (2020), https://proceedings.mlr.press/v119/peifer20a.html [36] Scott, J., Niemetz, A., Preiner, M., Nejati, S., Ganesh, V.: MachSMT: A machine learningbased algorithm selector for SMT solvers. In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 12652, pp. 303–325. Springer International Publishing (2021), https://doi.org/ 10.1007/978-3-030-72013-1_16 [37] Selsam, D., Bjørner, N.: Guiding high-performance SAT solvers with unsat-core predictions.
In: Janota, M., Lynce, I. (eds.) Theory and Applications of Satisfiability Testing – SAT 2019. Lecture Notes in Computer Science, vol. 11628, pp. 336–353. Springer International Publishing (2019), https://doi.org/10.1007/978-3-030-24258-9_24 [38] Wu, H.: Improving SAT-solving with machine learning. In: Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education. pp. 787–788. SIGCSE ’17, ACM (2017), https://doi.org/10.1145/3017680.3022464 [39] Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: SATzilla: Portfolio-based algorithm selection for SAT. Journal Of Artificial Intelligence Research 32, 565–606 (2008), https: //doi.org/10.1613/jair.2490