Abstract
Cylindrical algebraic decomposition (CAD) is an important tool for the study of real algebraic geometry with many applications both within mathematics and elsewhere. It is known to have doubly exponential complexity in the number of variables in the worst case, but the actual computation time can vary greatly. It is possible to offer different formulations for a given problem leading to great differences in tractability. In this paper we suggest a new measure for CAD complexity which takes into account the real geometry of the problem. This leads to new heuristics for choosing: the variable ordering for a CAD problem, a designated equational constraint, and formulations for truth-table invariant CADs (TTICADs). We then consider the possibility of using Gröbner bases to precondition TTICAD and when such formulations constitute the creation of a new problem.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Akbarpour, B., Paulson, L.C.: MetiTarski: An Automatic Prover for the Elementary Functions. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC/Calculemus/MKM 2008. LNCS (LNAI), vol. 5144, pp. 217–231. Springer, Heidelberg (2008)
Akbarpour, B., Paulson, L.C.: MetiTarski: An automatic theorem prover for real-valued special functions. Journal of Automated Reasoning 44(3), 175–205 (2010)
Bradford, R., Davenport, J.H., England, M., McCallum, S., Wilson, D.: Cylindrical algebraic decompositions for boolean combinations. In Press: Proc. ISSAC 2013 (2013), Preprint at http://opus.bath.ac.uk/33926/
Brown, C.W.: QEPCAD B: A program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bulletin 37(4), 97–108 (2003)
Brown, C.W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proc. ISSAC 2007, pp. 54–60. ACM (2007)
Brown, C.W., McCallum, S.: On using bi-equational constraints in CAD construction. In: Proc. ISSAC 2005, pp. 76–83. ACM (2005)
Buchberger, B., Hong, H.: Speeding up quantifier elimination by Gröbner bases. Technical report, 91-06. RISC, Johannes Kepler University (1991)
Chen, C., Moreno Maza, M., Xia, B., Yang, L.: Computing cylindrical algebraic decomposition via triangular decomposition. In: Proc. ISSAC 2009, pp. 95–102. ACM (2009)
Cohen, C., Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. LMCS 8(1:02), 1–40 (2012)
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)
Collins, G.E.: Quantifier elimination by cylindrical algebraic decomposition – 20 years of progress. In: Caviness, B., Johnson, J. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts & Monographs in Symbolic Computation, pp. 8–23. Springer (1998)
Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12, 299–328 (1991)
Davenport, J.H., Bradford, R., England, M., Wilson, D.: Program verification in the presence of complex numbers, functions with branch cuts etc. In: Proc. SYNASC 2012 (2012)
Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Proc. ISSAC 2004, pp. 111–118. ACM (2004)
Dolzmann, A., Sturm, T., Weispfenning, V.: A New Approach for Automatic Theorem Proving in Real Geometry. Journal of Automated Reasoning 21(3), 357–380 (1998)
England, M.: An implementation of CAD in Maple utilising McCallum projection. Department of Computer Science Technical Report series 2013-02, University of Bath (2013), http://opus.bath.ac.uk/33180/
England, M., Bradford, R., Davenport, J.H., Wilson, D.: Understanding branch cuts of expressions. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 136–151. Springer, Heidelberg (2013)
Lazard, D.: Quantifier elimination: Optimal solution for two classical examples. J. Symb. Comput. 5(1-2), 261–266 (1988)
McCallum, S.: An improved projection operation for cylindrical algebraic decomposition of three-dimensional space. J. Symb. Comput. 5(1-2), 141–161 (1988)
McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In: Caviness, B., Johnson, J. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts & Monographs in Symbolic Computation, pp. 242–268. Springer (1998)
McCallum, S.: On projection in CAD-based quantifier elimination with equational constraint. In: Proc. ISSAC 1999, pp. 145–149. ACM (1999)
Mahboubi, A.: Implementing the cylindrical algebraic decomposition within the Coq system. Math. Struct. in Comp. Science 17(1), 99–127 (2007)
Passmore, G.O., Paulson, L.C., de Moura, L.: Real Algebraic Strategies for MetiTarski Proofs. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol. 7362, pp. 358–370. Springer, Heidelberg (2012)
Phisanbut, N.: Practical Simplification of Elementary Functions using Cylindrical Algebraic Decomposition. PhD thesis, University of Bath (2011)
Schwartz, J.T., Sharir, M.: On the “Piano-Movers” Problem: II. General techniques for computing topological properties of real algebraic manifolds. Adv. Appl. Math. 4, 298–351 (1983)
Wilson, D.J., Bradford, R.J., Davenport, J.H.: A repository for CAD examples. ACM Communications in Computer Algebra 46(3), 67–69 (2012)
Wilson, D.J., Bradford, R.J., Davenport, J.H.: Speeding up cylindrical algebraic decomposition by Gröbner bases. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol. 7362, pp. 280–294. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bradford, R., Davenport, J.H., England, M., Wilson, D. (2013). Optimising Problem Formulation for Cylindrical Algebraic Decomposition. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds) Intelligent Computer Mathematics. CICM 2013. Lecture Notes in Computer Science(), vol 7961. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39320-4_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-39320-4_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39319-8
Online ISBN: 978-3-642-39320-4
eBook Packages: Computer ScienceComputer Science (R0)