Skip to main content
SpringerLink
Log in

Comparing Machine Learning Models to Choose the Variable Ordering for Cylindrical Algebraic Decomposition

  • Conference paper
  • First Online:
Intelligent Computer Mathematics (CICM 2019)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 11617))

Included in the following conference series:

Abstract

There has been recent interest in the use of machine learning (ML) approaches within mathematical software to make choices that impact on the computing performance without affecting the mathematical correctness of the result. We address the problem of selecting the variable ordering for cylindrical algebraic decomposition (CAD), an important algorithm in Symbolic Computation. Prior work to apply ML on this problem implemented a Support Vector Machine (SVM) to select between three existing human-made heuristics, which did better than anyone heuristic alone. Here we extend this result by training ML models to select the variable ordering directly, and by trying out a wider variety of ML techniques.

We experimented with the NLSAT dataset and the Regular Chains Library CAD function for Maple 2018. For each problem, the variable ordering leading to the shortest computing time was selected as the target class for ML. Features were generated from the polynomial input and used to train the following ML models: k-nearest neighbours (KNN) classifier, multi-layer perceptron (MLP), decision tree (DT) and SVM, as implemented in the Python scikit-learn package. We also compared these with the two leading human-made heuristics for the problem: the Brown heuristic and sotd. On this dataset all of the ML approaches outperformed the human-made heuristics, some by a large margin.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Research Data Statement

Data supporting the research in this paper is available at: http://doi.org/10.5281/zenodo.2658626.

Notes

  1. 1.

    E.g. the PoSSo and FRISCO projects in the 90s and the SymbolicData Project [32].

  2. 2.

    However, as discussed by [1] a more custom approach is beneficial.

  3. 3.

    http://cs.nyu.edu/~dejan/nonlinear/.

  4. 4.

    https://www.usna.edu/Users/cs/wcbrown/research/ISSAC04/handout.pdf.

References

  1. Ábrahám, E., et al.: \({\sf SC^ 2}\): satisfiability checking meets symbolic computation. In: Kohlhase, M., Johansson, M., Miller, B., de de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 28–43. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-42547-4_3

    Chapter  Google Scholar 

  2. Alemi, A., Chollet, F., Een, N., Irving, G., Szegedy, C., Urban, J.: DeepMath-deep sequence models for premise selection. In: Proceedings of the 30th International Conference on Neural Information Processing Systems, NIPS 2016, pp. 2243–2251, Curran Associates Inc. (2016). https://papers.nips.cc/paper/6280-deepmath-deep-sequence-models-for-premise-selection.pdf

  3. Arnon, D., Collins, G., McCallum, S.: Cylindrical algebraic decomposition I: the basic algorithm. SIAM J. Comput. 13, 865–877 (1984). https://doi.org/10.1137/0213054

    Article  MathSciNet  MATH  Google Scholar 

  4. Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, Chap. 26, vol. 185 pp. 825–885. IOS Press (2009)

    Google Scholar 

  5. Bishop, C.: Pattern Recognition and Machine Learning. Springer, New York (2006)

    MATH  Google Scholar 

  6. Bradford, R., Chen, C., Davenport, J.H., England, M., Moreno Maza, M., Wilson, D.: Truth table invariant cylindrical algebraic decomposition by regular chains. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2014. LNCS, vol. 8660, pp. 44–58. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10515-4_4

    Chapter  Google Scholar 

  7. Bradford, R., et al.: A case study on the parametric occurrence of multiple steady states. In: Proceedings of the 42nd International Symposium on Symbolic and Algebraic Computation, ISSAC 2017, pp. 45–52. ACM (2017). https://doi.org/10.1145/3087604.3087622

  8. Bradford, R., Davenport, J., England, M., McCallum, S., Wilson, D.: Cylindrical algebraic decompositions for Boolean combinations. In: Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation, ISSAC 2013, pp. 125–132. ACM (2013). https://doi.org/10.1145/2465506.2465516

  9. Bradford, R., Davenport, J., England, M., McCallum, S., Wilson, D.: Truth table invariant cylindrical algebraic decomposition. J. Symb. Comput. 76, 1–35 (2016). https://doi.org/10.1016/j.jsc.2015.11.002

    Article  MathSciNet  MATH  Google Scholar 

  10. Bradford, R., Davenport, J.H., England, M., Wilson, D.: Optimising problem formulation for cylindrical algebraic decomposition. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 19–34. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39320-4_2

    Chapter  Google Scholar 

  11. Bridge, J., Holden, S., Paulson, L.: Machine learning for first-order theorem proving. J. Autom. Reason. 53, 141–172 (2014). 10.1007/s10817-014-9301-5

    Article  Google Scholar 

  12. Brown, C.: Improved projection for cylindrical algebraic decomposition. J. Symb. Comput. 32(5), 447–465 (2001). https://doi.org/10.1006/jsco.2001.0463

    Article  MathSciNet  MATH  Google Scholar 

  13. Brown, C.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bull. 37(4), 97–108 (2003). https://doi.org/10.1145/968708.968710

    Article  MATH  Google Scholar 

  14. Brown, C., Davenport, J.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings of the 32nd International Symposium on Symbolic and Algebraic Computation, ISSAC 2007, pp. 54–60. ACM (2007). https://doi.org/10.1145/1277548.1277557

  15. Brown, C., Kosta, M.: Constructing a single cell in cylindrical algebraic decomposition. J. Symb. Comput. 70, 14–48 (2015). https://doi.org/10.1016/j.jsc.2014.09.024

    Article  MathSciNet  MATH  Google Scholar 

  16. Caviness, B., Johnson, J.: Quantifier Elimination and Cylindrical Algebraic Decomposition. TEXTSMONOGR. Springer, Vienna (1998). https://doi.org/10.1007/978-3-7091-9459-1

    Book  MATH  Google Scholar 

  17. Chen, C., Moreno Maza, M.: An incremental algorithm for computing cylindrical algebraic decompositions. In: Feng, R., Lee, W., Sato, Y. (eds.) Computer Mathematics. LNCS (LNAI), pp. 199–221. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43799-5_17

    Chapter  Google Scholar 

  18. Chen, C., Moreno Maza, M., Xia, B., Yang, L.: Computing cylindrical algebraic decomposition via triangular decomposition. In: Proceedings of the 34th International Symposium on Symbolic and Algebraic Computation, ISSAC 2009, pp. 95–102. ACM (2009). https://doi.org/10.1145/1576702.1576718

  19. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975). https://doi.org/10.1007/3-540-07407-4_17

    Chapter  Google Scholar 

  20. Collins, G., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12, 299–328 (1991). https://doi.org/10.1016/S0747-7171(08)80152-6

    Article  MathSciNet  MATH  Google Scholar 

  21. Davenport, J., Bradford, R., England, M., Wilson, D.: Program verification in the presence of complex numbers, functions with branch cuts etc. In: 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2012, pp. 83–88. IEEE (2012). https://doi.org/10.1109/SYNASC.2012.68

  22. Davenport, J., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1–2), 29–35 (1988). https://doi.org/10.1016/S0747-7171(88)80004-X

    Article  MathSciNet  MATH  Google Scholar 

  23. Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Proceedings of the 29th International Symposium on Symbolic and Algebraic Computation, ISSAC 2004, pp. 111–118. ACM (2004). https://doi.org/10.1145/1005285.1005303

  24. Dolzmann, A., Sturm, T.: REDLOG: computer algebra meets computer logic. SIGSAM Bull. 31(2), 2–9 (1997). https://doi.org/10.1145/261320.261324

    Article  Google Scholar 

  25. England, M.: Machine learning for mathematical software. In: Davenport, J.H., Kauers, M., Labahn, G., Urban, J. (eds.) ICMS 2018. LNCS, vol. 10931, pp. 165–174. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96418-8_20

    Chapter  MATH  Google Scholar 

  26. England, M., Bradford, R., Chen, C., Davenport, J.H., Maza, M.M., Wilson, D.: Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 45–60. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08434-3_5

    Chapter  Google Scholar 

  27. England, M., Bradford, R., Davenport, J.: Improving the use of equational constraints in cylindrical algebraic decomposition. In: Proceedings of the 40th International Symposium on Symbolic and Algebraic Computation, ISSAC 2015, pp. 165–172. ACM (2015). https://doi.org/10.1145/2755996.2756678

  28. 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.) ICMS 2014. LNCS, vol. 8592, pp. 450–457. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44199-2_68

    Chapter  Google Scholar 

  29. England, M., Errami, H., Grigoriev, D., Radulescu, O., Sturm, T., Weber, A.: Symbolic versus numerical computation and visualization of parameter regions for multistationarity of biological networks. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2017. LNCS, vol. 10490, pp. 93–108. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66320-3_8

    Chapter  Google Scholar 

  30. England, M., Wilson, D., Bradford, R., Davenport, J.H.: Using the regular chains library to build cylindrical algebraic decompositions by projecting and lifting. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 458–465. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44199-2_69

    Chapter  Google Scholar 

  31. Erascu, M., Hong, H.: Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation). J. Symb. Comput. 75, 110–126 (2016). https://doi.org/10.1016/j.jsc.2015.11.010

    Article  MathSciNet  MATH  Google Scholar 

  32. Graebe, H., Nareike, A., Johanning, S.: The SymbolicData project: towards a computer algebra social network. In: England, M., et al. (eds.) Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress track at CICM. CEUR Workshop Proceedings, vol. 1186 (2014). http://ceur-ws.org/Vol-1186/#paper-21

  33. Heinle, A., Levandovskyy, V.: The SDEval benchmarking toolkit. ACM Commun. Comput. Algebra 49(1), 1–9 (2015). https://doi.org/10.1145/2768577.2768578

    Article  MathSciNet  MATH  Google Scholar 

  34. Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: Proceedings of the 15th International Symposium on Symbolic and Algebraic Computation, ISSAC 1990, pp. 261–264. ACM (1990), https://doi.org/10.1145/96877.96943

  35. Huang, Z., England, M., Davenport, J., Paulson, L.: Using machine learning to decide when to precondition cylindrical algebraic decomposition with Groebner bases. In: 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2016), pp. 45–52. IEEE (2016). https://doi.org/10.1109/SYNASC.2016.020

  36. Huang, Z., England, M., Wilson, D., Bridge, J., Davenport, J.H., Paulson, L.: Using machine learning to improve cylindrical algebraic decomposition. Math. Comput. Sci. (2019). https://doi.org/10.1007/s11786-019-00394-8

  37. Huang, Z., England, M., Wilson, D., Davenport, J.H., Paulson, L.C., 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.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 92–107. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08434-3_8

    Chapter  Google Scholar 

  38. Iwane, H., Yanami, H., Anai, H., Yokoyama, K.: An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier elimination. In: Proceedings of the 2009 Conference on Symbolic Numeric Computation, SNC 2009, pp. 55–64 (2009). https://doi.org/10.1145/1577190.1577203

  39. Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339–354. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_27

    Chapter  Google Scholar 

  40. Kobayashi, M., Iwane, H., Matsuzaki, T., Anai, H.: Efficient subformula orders for real quantifier elimination of non-prenex formulas. In: Kotsireas, I.S., Rump, S.M., Yap, C.K. (eds.) MACIS 2015. LNCS, vol. 9582, pp. 236–251. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-32859-1_21

    Chapter  MATH  Google Scholar 

  41. Kühlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: machine learning for sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 35–50. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39634-2_6

    Chapter  Google Scholar 

  42. Liang, J.H., Hari Govind, V.K., Poupart, P., Czarnecki, K., Ganesh, V.: An empirical study of branching heuristics through the lens of global learning rate. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 119–135. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_8

    Chapter  MATH  Google Scholar 

  43. McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. TEXTSMONOGR, pp. 242–268. Springer, Vienna (1998). https://doi.org/10.1007/978-3-7091-9459-1_12

    Chapter  MATH  Google Scholar 

  44. McCallum, S., Parusińiski, A., Paunescu, L.: Validity proof of Lazard’s method for CAD construction. J. Symb. Comput. 92, 52–69 (2019). https://doi.org/10.1016/j.jsc.2017.12.002

    Article  MathSciNet  Google Scholar 

  45. Mulligan, C., Bradford, R., Davenport, J., England, M., Tonks, Z.: Non-linear real arithmetic benchmarks derived from automated reasoning in economics. In: Bigatti, A., Brain, M. (eds.) Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation (\({{\sf SC}}^2\) 2018). CEUR Workshop Proceedings, vol. 2189, pp. 48–60 (2018). http://ceur-ws.org/Vol-2189/

  46. Mulligan, C.B., Davenport, J.H., England, M.: TheoryGuru: a mathematica package to apply quantifier elimination technology to economics. In: Davenport, J.H., Kauers, M., Labahn, G., Urban, J. (eds.) ICMS 2018. LNCS, vol. 10931, pp. 369–378. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96418-8_44

    Chapter  Google Scholar 

  47. Paulson, L.C.: MetiTarski: past and future. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 1–10. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32347-8_1

    Chapter  Google Scholar 

  48. Pedregosa, F., et al.: Scikit-learn: machine learning in Python. J. Mach. Learn. Res. 12, 2825–2830 (2011). http://www.jmlr.org/papers/v12/pedregosa11a.html

    MathSciNet  MATH  Google Scholar 

  49. Platzer, A., Quesel, J.-D., Rümmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 485–501. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_35

    Chapter  Google Scholar 

  50. Strzeboński, A.: Cylindrical algebraic decomposition using validated numerics. J. Symb. Comput. 41(9), 1021–1038 (2006). https://doi.org/10.1016/j.jsc.2006.06.004

    Article  MathSciNet  MATH  Google Scholar 

  51. Strzeboński, A.: Cylindrical algebraic decomposition using local projections. J. Symb. Comput. 76, 36–64 (2016). https://doi.org/10.1016/j.jsc.2015.11.018

    Article  MathSciNet  MATH  Google Scholar 

  52. Sturm, T.: New domains for applied quantifier elimination. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) CASC 2006. LNCS, vol. 4194, pp. 295–301. Springer, Heidelberg (2006). https://doi.org/10.1007/11870814_25

    Chapter  Google Scholar 

  53. Tarski, A.: A decision method for elementary algebra and geometry. RAND Corporation, Santa Monica, CA (reprinted in the collection [16]) (1948)

    Google Scholar 

  54. Urban, J.: MaLARea: a metasystem for automated reasoning in large theories. In: Empirically Successful Automated Reasoning in Large Theories (ESARLT 2007). CEUR Workshop Proceedings, vol. 257, p. 14 (2007). http://ceur-ws.org/Vol-257/

  55. Wilson, D., Bradford, R., Davenport, J., England, M.: Cylindrical algebraic subdecompositions. Math. Comput. Sci. 8, 263–288 (2014). https://doi.org/10.1007/s11786-014-0191-z

    Article  MathSciNet  MATH  Google Scholar 

  56. Wilson, D., Davenport, J., England, M., Bradford, R.: A “piano movers” problem reformulated. In: 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013, pp. 53–60. IEEE (2013). https://doi.org/10.1109/SYNASC.2013.14

  57. Wilson, D., England, M., Davenport, J., Bradford, R.: Using the distribution of cells by dimension in a cylindrical algebraic decomposition. In: 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2014, pp. 53–60. IEEE (2014). https://doi.org/10.1109/SYNASC.2014.15

  58. Wilson, D., Bradford, R., Davenport, J.: A repository for CAD examples. ACM Commun. Comput. Algebra 46(3), 67–69 (2012). https://doi.org/10.1145/2429135.2429137

    Article  MATH  Google Scholar 

  59. Xu, L., Hutter, F., Hoos, H., Leyton-Brown, K.: SATzilla: portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. 32, 565–606 (2008). https://doi.org/10.1613/jair.2490

    Article  MATH  Google Scholar 

Download references

Acknowledgments

The authors are supported by EPSRC Project EP/R019622/1: Embedding Machine Learning within Quantifier Elimination Procedures.

Author information

Authors and Affiliations

  1. Faculty of Engineering, Environment and Computing, Coventry University, Coventry, CV1 5FB, UK

    Matthew England & Dorian Florescu

Authors
  1. Matthew England
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dorian Florescu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Matthew England .

Editor information

Editors and Affiliations

  1. University of Innsbruck, Innsbruck, Austria

    Cezary Kaliszyk

  2. University of St. Andrews, St. Andrews, UK

    Edwin Brady

  3. University of Applied Sciences, Neu-Ulm, Germany

    Andrea Kohlhase

  4. University of Bologna, Bologna, Italy

    Claudio Sacerdoti Coen

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

England, M., Florescu, D. (2019). Comparing Machine Learning Models to Choose the Variable Ordering for Cylindrical Algebraic Decomposition. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds) Intelligent Computer Mathematics. CICM 2019. Lecture Notes in Computer Science(), vol 11617. Springer, Cham. https://doi.org/10.1007/978-3-030-23250-4_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-23250-4_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-23249-8

  • Online ISBN: 978-3-030-23250-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation