zbMATH — the first resource for mathematics

Cylindrical algebraic sub-decompositions. (English) Zbl 1309.68232
Summary: Cylindrical algebraic decompositions (CADs) are a key tool in real algebraic geometry, used primarily for eliminating quantifiers over the reals and studying semi-algebraic sets. In this paper we introduce cylindrical algebraic sub-decompositions (sub-CADs), which are subsets of CADs containing all the information needed to specify a solution for a given problem. We define two new types of sub-CAD: variety sub-CADs which are those cells in a CAD lying on a designated variety; and layered sub-CADs which have only those cells of dimension higher than a specified value. We present algorithms to produce these and describe how the two approaches may be combined with each other and the recent theory of truth-table invariant CAD. We give a complexity analysis showing that these techniques can offer substantial theoretical savings, which is supported by experimentation using an implementation in Maple.

68W30 Symbolic computation and algebraic computation
14P10 Semialgebraic sets and related spaces
14Q20 Effectivity, complexity and computational aspects of algebraic geometry
68Q25 Analysis of algorithms and problem complexity
Full Text: DOI arXiv
[1] Arnon, D.; Collins, G.E.; McCallum, S., Cylindrical algebraic decomposition I: the basic algorithm, SIAM J. Comput., 13, 865-877, (1984) · Zbl 0562.14001
[2] Backelin, J.: Square multiples \(n\) give infinitely many cyclic \(n\)-roots. Matematiska Institutionen Reports Series. Stockholms Universitet (1989)
[3] Bradford, R., Davenport, J.H.: Towards better simplification of elementary functions. In: Proceedings of the ISSAC’02, pp. 16-22. ACM (2002) · Zbl 1072.68651
[4] Bradford, R., Davenport, J.H., England, M. McCallum, S., Wilson, D.: Cylindrical algebraic decompositions for boolean combinations. In: Proceedings of the ISSAC’13, pp. 125-132. ACM (2013) · Zbl 1359.68327
[5] Bradford, R., Davenport, J.H., England, M., McCallum, S., Wilson, D.: Truth table invariant cylindrical algebraic decomposition. http://opus.bath.ac.uk/38146/ (2014 submitted, preprint) · Zbl 1351.68314
[6] Bradford, R., Davenport, J.H., England, M., Wilson, D.: Optimising problem formulations for cylindrical algebraic decomposition. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. Intelligent Computer Mathematics. LNCS, vol. 7961, pp. 19-34. Springer, Berlin (2013) · Zbl 1390.68775
[7] Brown, C.W., Improved projection for cylindrical algebraic decomposition, J. Symb. Comput., 32, 447-465, (2001) · Zbl 0981.68186
[8] Brown, C.W., An overview of QEPCAD B: a program for computing with semi-algebraic sets using cads, ACM SIGSAM Bull., 37, 97-108, (2003) · Zbl 1083.68148
[9] Brown, C.W.: The McCallum projection, lifting, and order-invariance. Technical report, US Naval Academy, Computer Science Department (2005) · Zbl 0554.51008
[10] Brown, C.W.: Constructing a single open cell in a cylindrical algebraic decomposition. In: Proceedings of the ISSAC’13, pp. 133-140. ACM (2013) · Zbl 1360.68924
[11] Brown, C.W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings of the ISSAC’07, pp. 54-60. ACM (2007) · Zbl 1190.68028
[12] Brown, C.W.; El Kahoui, M.; Novotni, D.; Weber, A., Algorithmic methods for investigating equilibria in epidemic modelling, J. Symb. Comput., 41, 1157-1173, (2006) · Zbl 1120.92034
[13] Brown, C.W., McCallum, S.: On using bi-equational constraints in CAD construction. In: Proceedings of the ISSAC’05, pp. 76-83. ACM (2005) · Zbl 1360.68925
[14] Burr, M.A.: Applications of continuous amortization to bisection-based root isolation. http://arxiv.org/abs/1309.5991 (2013, preprint) · Zbl 0562.14001
[15] Chen, C., Moreno Maza, M.: An incremental algorithm for computing cylindrical algebraic decompositions. In: Proceedings of the ASCM’12. Springer, Berlin (2012, preprint). arXiv:1210.5543 · Zbl 1352.68291
[16] Chen, C., Moreno Maza, M., Xia, B., Yang, L.: Computing cylindrical algebraic decomposition via triangular decomposition. In: Proceedings of the ISSAC’09, pp. 95-102. ACM (2009) · Zbl 1237.14068
[17] 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. Berlin (1975) · Zbl 1305.68367
[18] Collins, G.E.; Hong, H., Partial cylindrical algebraic decomposition for quantifier elimination, J. Symb. Comput., 12, 299-328, (1991) · Zbl 0754.68063
[19] Davenport, J.H.: Computer algebra for cylindrical algebraic decomposition. Technical Report TRITA-NA-8511, NADA KTH Stockholm. Reissued as Bath Computer Science Technical report 88-10. http://staff.bath.ac.uk/masjhd/TRITA.pdf (1985) · Zbl 1083.68148
[20] Davenport, J.H., A “piano-movers” problem, SIGSAM Bull., 20, 15-17, (1986) · Zbl 0623.68036
[21] Davenport, J.H., Bradford, R., England, M., Wilson, D.: Program verification in the presence of complex numbers, functions with branch cuts etc. In: Proceedings of the SYNASC’12, pp. 83-88. IEEE (2012) · Zbl 0981.68186
[22] Davenport, J.H.; Heintz, J., Real quantifier elimination is doubly exponential, J. Symb. Comput., 5, 29-35, (1988) · Zbl 0663.03015
[23] Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Proceedings of the ISSAC’04, pp. 111-118. ACM (2004) · Zbl 1134.68575
[24] England, M.: An implementation of CAD in Maple utilising McCallum projection. Department of Computer Science Technical Report series 2013-02, University of Bath. http://opus.bath.ac.uk/33180/ (2013) · Zbl 0754.68063
[25] England, M.: An implementation of CAD in Maple utilising problem formulation, equational constraints and truth-table invariance. Department of Computer Science Technical Report series 2013-04, University of Bath. http://opus.bath.ac.uk/35636/(2013)
[26] England, M.; Bradford, R.; Davenport, J.H.; Wilson, D.; Carette, J. (ed.); Aspinall, D. (ed.); Lange, C. (ed.); Sojka, P. (ed.); Windsteiger, W. (ed.), Understanding branch cuts of expressions, 136-151, (2013), Berlin · Zbl 1390.68777
[27] Fotiou, I.A., Parrilo, P.A., Morari, M.: Nonlinear parametric optimization using cylindrical algebraic decomposition. In: Decision and Control, 2005 and 2005 European Control Conference. CDC-ECC ’05, pp. 3735-3740 (2005)
[28] Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: Proceedings of the ISSAC’90, pp. 261-264. ACM (1990)
[29] 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 SNC’09, pp. 55-64 (2009) · Zbl 1356.68282
[30] Malladi, H.K., Dukkipati, A.: A preprocessor based on clause normal forms and virtual substitutions to parallelize cylindrical algebraic decomposition. http://arxiv.org/abs/1112.5352v3 (2013, preprint)
[31] McCallum, S., Solving polynomial strict inequalities using cylindrical algebraic decomposition, Comput. J., 36, 432-438, (1993) · Zbl 0789.68080
[32] McCallum, S.: A computer algebra approach to path finding in the plane. In: Harland J. (ed.) Proceedings of Computing: The Australasian Theory Symposium (CATS), pp. 44-50 (1997)
[33] McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In: Caviness, B., Johnson, J. Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation, pp. 242-268. Springer, Berlin (1998)
[34] McCallum, S.: On projection in CAD-based quantifier elimination with equational constraint. In: Proceedings of the ISSAC’99, pp. 145-149. ACM (1999) · Zbl 0789.68080
[35] McCallum, S.: On propagation of equational constraints in CAD-based quantifier elimination. In: Proceedings of the ISSAC’01, pp. 223-231. ACM (2001) · Zbl 1356.68287
[36] Paulson, L.C.; Beringer, L. (ed.); Felty, A. (ed.), Metitarski: past and future, 1-10, (2012), Berlin · Zbl 1360.68765
[37] Phisanbut, N.; Bradford, R.J.; Davenport, J.H., Geometry of branch cuts, ACM Commun. Comput. Algebra, 44, 132-135, (2010) · Zbl 1305.68367
[38] 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) · Zbl 0554.51008
[39] Seidl, A., Sturm, T.: A generic projection operator for partial cylindrical algebraic decomposition. In: Proceedings of the ISSAC’03, pp. 240-247. ACM (2003) · Zbl 1072.68696
[40] Strzeboński, A., Solving systems of strict polynomial inequalities, J. Symb. Comput., 29, 471-480, (2000) · Zbl 0962.68183
[41] Strzeboński, A., Cylindrical algebraic decomposition using validated numerics, J. Symb. Comput., 41, 1021-1038, (2006) · Zbl 1124.68123
[42] Strzeboński, A.: Computation with semialgebraic sets represented by cylindrical algebraic formulas. In: Proceedings of the ISSAC’10, pp. 61-68. ACM (2010) · Zbl 1321.68543
[43] Strzeboński, A.: Solving polynomial systems over semialgebraic sets represented by cylindrical algebraic formulas. In: Proceedings of the ISSAC’12, pp. 335-342. ACM (2012) · Zbl 1308.68191
[44] Wilson, D., Davenport, J.H., England, M., Bradford, R.: A “Piano Movers” problem reformulated. In: Proceedings of the SYNASC’13. IEEE (2013)
[45] Wilson, D., England, M.: Layered cylindrical algebraic decomposition. Department of Computer Science Technical Report series 2013-05, University of Bath. http://opus.bath.ac.uk/36712/ (2013)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.