Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition

1. Akbarpour, B., Paulson, L.: MetiTarski: An automatic theorem prover for real-valued special functions. Journal of Automated Reasoning 44(3), 175–205 (2010)

   Article  MathSciNet  MATH  Google Scholar 

2. Alpaydin, E.: Introduction to machine learning. MIT Press (2004)

   Google Scholar 

3. Arnon, D., Collins, G., McCallum, S.: Cylindrical algebraic decomposition I: The basic algorithm. SIAM Journal of Computing 13, 865–877 (1984)

   Article  MathSciNet  MATH  Google Scholar 

4. Baldi, P., Brunak, S., Chauvin, Y., Andersen, C.A., Nielsen, H.: Assessing the accuracy of prediction algorithms for classification: an overview. Bioinformatics 16(5), 412–424 (2000)

   Article  Google Scholar 

5. Basu, S.: Algorithms in real algebraic geometry: A survey (2011), www.math.purdue.edu/~sbasu/raag_survey2011_final.pdf

6. Boyan, J., Freitag, D., Joachims, T.: A machine learning architecture for optimizing web search engines. In: AAAI Workshop on Internet Based Information Systems, pp. 1–8 (1996)

   Google Scholar 

7. Bradford, R., Davenport, J., England, M., McCallum, S., Wilson, D.: Cylindrical algebraic decompositions for boolean combinations. In: Proc. ISSAC 2013, pp. 125–132. ACM (2013)

   Google Scholar 

8. 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)

   Chapter  Google Scholar 

9. Bridge, J.P.: Machine learning and automated theorem proving. University of Cambridge Computer Laboratory Technical Report UCAM-CL-TR-792 (2010), http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-792.pdf

10. Bridge, J., Holden, S., Paulson, L.: Machine learning for first-order theorem proving. Journal of Automated Reasoning, 1–32 (2014)

    Google Scholar 

11. Brown, C.: Improved projection for cylindrical algebraic decomposition. Journal of Symbolic Computation 32(5), 447–465 (2001)

    Article  MathSciNet  MATH  Google Scholar 

12. Brown, C.: QEPCAD B: A program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bulletin 37(4), 97–108 (2003)

    Article  MATH  Google Scholar 

13. Brown, C.: Companion to the Tutorial: Cylindrical algebraic decomposition. Presented at ISSAC 2004 (2004), www.usna.edu/Users/cs/wcbrown/research/ISSAC04/handout.pdf

14. Brown, C., Davenport, J.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proc. ISSAC 2007, pp. 54–60. ACM (2007)

    Google Scholar 

15. Brown, C., Kahoui, M.E., Novotni, D., Weber, A.: Algorithmic methods for investigating equilibria in epidemic modelling. Journal of Symbolic Computation 41, 1157–1173 (2006)

    Article  MathSciNet  MATH  Google Scholar 

16. Carette, J.: Understanding expression simplification. In: Proc. ISSAC 2004, pp. 72–79. ACM (2004)

    Google Scholar 

17. Chen, C., Maza, M.M., Xia, B., Yang, L.: Computing cylindrical algebraic decomposition via triangular decomposition. In: Proc. ISSAC 2009, pp. 95–102. ACM (2009)

    Google Scholar 

18. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)

    Google Scholar 

19. Collins, G.: Quantifier elimination by cylindrical algebraic decomposition – 20 years of progress. In: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts & Monographs in Symbolic Computation, pp. 8–23. Springer (1998)

    Google Scholar 

20. Collins, G., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation 12, 299–328 (1991)

    Article  MathSciNet  MATH  Google Scholar 

21. Cristianini, N., Shawe-Taylor, J.: An introduction to support vector machines and other kernel-based learning methods. Cambridge University Press (2000)

    Google Scholar 

22. Davenport, J., Bradford, R., England, M., Wilson, D.: Program verification in the presence of complex numbers, functions with branch cuts etc. In: Proc. SYNASC 2012, pp. 83–88. IEEE (2012)

    Google Scholar 

23. Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Proc. ISSAC 2004, pp. 111–118. ACM (2004)

    Google Scholar 

24. Dolzmann, A., Sturm, T.: REDLOG: Computer algebra meets computer logic. SIGSAM Bulletin 31(2), 2–9 (1997)

    Article  Google Scholar 

25. Dolzmann, A., Sturm, T., Weispfenning, V.: Real quantifier elimination in practice. In: Algorithmic Algebra and Number Theory, pp. 221–247. Springer (1998)

    Google Scholar 

26. England, M.: An implementation of CAD in Maple utilising problem formulation, equational constraints and truth-table invariance. University of Bath Department of Computer Science Technical Report 2013-04 (2013), http://opus.bath.ac.uk/35636/

27. Forsyth, R., Rada, R.: Machine learning: Applications in expert systems and information retrieval. Halsted Press (1986)

    Google Scholar 

28. Fotiou, I., Parrilo, P., Morari, M.: Nonlinear parametric optimization using cylindrical algebraic decomposition. In: 2005 European Control Conference on Decision and Control, CDC-ECC 2005, pp. 3735–3740 (2005)

    Google Scholar 

29. Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: Proc. ISSAC 1990, pp. 261–264. ACM (1990)

    Google Scholar 

30. Hornik, K., Stinchcombe, M., White, H.: Multilayer feedforward networks are universal approximators. Neural Networks 2(5), 359–366 (1989)

    Article  Google Scholar 

31. Huang, Z., Paulson, L.: An application of machine learning to rcf decision procedures. In: Proc. 20th Automated Reasoning Workshop (2013)

    Google Scholar 

32. Hsu, C., Chang, C., Lin, C.: A practical guide to support vector classification (2003)

    Google Scholar 

33. Iwane, H., Yanami, H., Anai, H., Yokoyama, K.: An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier elimination. In: Proc. SNC 2009, pp. 55–64 (2009)

    Google Scholar 

34. Joachims, T.: Making large-scale SVM learning practical. In: Advances in Kernel Methods - Support Vector Learning, pp. 169–184. MIT Press (1999)

    Google Scholar 

35. Joachims, T.: A support vector method for multivariate performance measures. In: Proc. 22nd Intl. Conf. on Machine Learning, pp. 377–384. ACM (2005)

    Google Scholar 

36. Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 339–354. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

37. McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts & Monographs in Symbolic Computation, pp. 242–268. Springer (1998)

    Google Scholar 

38. McCallum, S.: On projection in CAD-based quantifier elimination with equational constraint. In: Proc. ISSAC 1999, pp. 145–149. ACM (1999)

    Google Scholar 

39. McCulloch, W.S., Pitts, W.: A logical calculus of the ideas immanent in nervous activity. The Bulletin of Mathematical Biophysics 5(4), 115–133 (1943)

    Article  MathSciNet  MATH  Google Scholar 

40. Rosenblatt, F.: The perceptron: a probabilistic model for information storage and organization in the brain. Psychological Review 65(6), 386 (1958)

    Article  Google Scholar 

41. Schölkopf, B., Tsuda, K., Vert, J.-P.: Kernel methods in computational biology. MIT Press (2004)

    Google Scholar 

42. Sebastiani, F.: Machine learning in automated text categorization. ACM Computing Surveys (CSUR) 34(1), 1–47 (2002)

    Article  Google Scholar 

43. Shawe-Taylor, J., Cristianini, N.: Kernel methods for pattern analysis. Cambridge University Press (2004)

    Google Scholar 

44. Stone, P., Veloso, M.: Multiagent systems: A survey from a machine learning perspective. Autonomous Robots 8(3), 345–383 (2000)

    Article  Google Scholar 

45. Strzeboński, A.: Cylindrical algebraic decomposition using validated numerics. Journal of Symbolic Computation 41(9), 1021–1038 (2006)

    Article  MathSciNet  MATH  Google Scholar 

46. Strzeboński, A.: Solving polynomial systems over semialgebraic sets represented by cylindrical algebraic formulas. In: Proc. ISSAC 2012, pp. 335–342. ACM (2012)

    Google Scholar 

47. Tarski, A.: A decision method for elementary algebra and geometry. In: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation, pp. 24–84. Springer (1998)

    Google Scholar 

48. Wilson, D., Bradford, R., Davenport, J.: A repository for CAD examples. ACM Communications in Computer Algebra 46(3), 67–69 (2012)

    MATH  Google Scholar 

49. Wilson, D., Davenport, J., England, M., Bradford, R.: A “piano movers” problem reformulated. In: Proc. SYNASC 2013. IEEE (2013)

    Google Scholar 

50. The benchmarks used in solving nonlinear arithmetic. New York University (2012), http://cs.nyu.edu/~dejan/nonlinear/

Download references