# zbMATH — the first resource for mathematics

An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination. (English) Zbl 1291.68433
Summary: With many applications in engineering and scientific fields, quantifier elimination (QE) has received increasing attention. Cylindrical algebraic decomposition (CAD) is used as a basis for a general QE algorithm. In this paper we present an effective symbolic-numeric cylindrical algebraic decomposition (SNCAD) algorithm for QE incorporating several new devices, which we call “quick tests”. The simple quick tests are run beforehand to detect an unnecessary procedure that might be skipped without violating the correctness of results and they thus considerably reduce the computing time. The effectiveness of the SNCAD algorithm is examined in a number of experiments including practical engineering problems, which also reveal the quality of the implementation. Experimental results show that our implementation has significantly improved efficiency compared with our previous work.

##### MSC:
 68W30 Symbolic computation and algebraic computation 03C10 Quantifier elimination, model completeness and related topics
##### Software:
 [1] H. Anai, S. Hara, Fixed-structure robust controller synthesis based on sign definite condition by a special quantifier elimination, in: Proceedings of American Control Conference, 2000, vol. 2, 2000, pp. 1312-1316. [2] H. Anai, P. Parrilo, Convex quantifier elimination for semidefinite programming, in: Proceedings of the International Workshop on Computer Algebra in Scientific Computing, CASC 2003, Sept. 2003, pp. 3-11. [3] H. Anai, H. Yanami, S. Hara, K. Sakabe, Fixed-structure robust controller synthesis based on symbolic-numeric computation: design algorithms with a CACSD toolbox, in: Proceedings of CCA/ISIC/CACSD 2004 (Taipei, Taiwan), vol. 2 (9) 2004, pp. 1540-1545,. [4] Anai, H.; Yokoyama, K., Cylindrical algebraic decomposition via numerical computation with validated symbolic reconstruction, (Dolzman, A.; Seidl, A.; Sturm, T., Algorithmic Algebra and Logic, (2005)), 25-30 [5] Basu, S.; Pollack, R.; Roy, M.-F., Algorithms in real algebraic geometry (algorithms and computation in mathematics), (2006), Springer-Verlag New York, Inc. Secaucus, NJ, USA [6] C.W. Brown, Solution formula construction for truth invariant cad’s. Ph.D. Thesis, University of Delaware Newark, 1999. [7] Brown, C. W., Improved projection for CAD’s of $$\mathbb{R}^3$$, (Proceedings of the 2000 International Symposium on Symbolic and Algebraic Computation, ISSAC’00, (2000), ACM New York, NY, USA), 48-53 · Zbl 1326.68345 [8] Brown, C. W., Improved projection for cylindrical algebraic decomposition, Journal of Symbolic Computation, 32, 5, 447-465, (2001) · Zbl 0981.68186 [9] Brown, C. W., QEPCAD B: a program for computing with semi-algebraic sets using cads, SIGSAM BULLETIN, 37, 97-108, (2003) · Zbl 1083.68148 [10] Quantifier elimination and cylindrical algebraic decomposition, (Caviness, B. F.; Johnson, J. R., Texts and Monographs in Symbolic Computation, (1998), Springer) · Zbl 0906.03033 [11] Collins, G. E., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, (LNCS, vol. 32, (1975), Springer Verla) · Zbl 0318.02051 [12] Collins, G. E.; Hong, H., Partial cylindrical algebraic decomposition for quantifier elimination, Journal of Symbolic Computation, 12, 3, 299-328, (1991) · Zbl 0754.68063 [13] Collins, G. E.; Johnson, J. R.; Krandick, W., Interval arithmetic in cylindrical algebraic decomposition, Journal of Symbolic Computation, 34, 2, 145-157, (2002) · Zbl 1007.68210 [14] Davenport, J. H.; Heintz, J., Real quantifier elimination is doubly exponential, Journal of Symbolic Computation, 5, 1/2, 29-35, (1988) · Zbl 0663.03015 [15] Deb, K., (Multi-Objective Optimization using Evolutionary Algorithms, Wiley-Interscience Series in Systems and Optimization, (2001), John Wiley & Sons Chichester) [16] Della Dora, J.; Dicrescenzo, C.; Duval, D., About a new method for computing in algebraic number fields, (Research Contributions from the European Conference on Computer Algebra, vol. 2, EUROCAL’85, (1985), Springer-Verlag London, UK), 289-290 [17] Dolzmann, A.; Sturm, T.; Weispfenning, V., Real quantifier elimination in practice, (Algorithmic Algebra and Number Theory, (1998), Springer), 221-247 · Zbl 0934.68130 [18] Duval, D., Algebraic numbers: an example of dynamic evaluation, Journal of Symbolic Computation, 18, 5, 429-445, (1994) · Zbl 0827.68061 [19] González-Vega, L., Applying quantifier elimination to the Birkhoff interpolation problem, Journal of Symbolic Computation, 22, July, 83-103, (1996) · Zbl 0870.65007 [20] L. González-Vega, A combinatorial algorithm solving some quantifier elimination problems, in: Caviness and Johnson [10], 1998, pp. 365-375. · Zbl 0900.68277 [21] Guo, F.; Safey, M.; Din, El; Zhi, L., Global optimization of polynomials using generalized critical values and sums of squares, (Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation, ISSAC’10, (2010), ACM New York, NY, USA), 107-114 · Zbl 1321.90127 [22] Hong, H., An improvement of the projection operator in cylindrical algebraic decomposition, (Proceedings of the International Symposium on Symbolic and Algebraic Computation, (1990), ACM. New York, NY, USA), 261-264 [23] Hong, H., Quantifier elimination for formulas constrained by quadratic equations, (Proceedings of the 1993 International Symposium on Symbolic and Algebraic Computation, ISSAC’93, (1993), ACM New York, NY, USA), 264-274 · Zbl 0964.68596 [24] Hong, H., An efficient method for analyzing the topology of plane real algebraic curves, (Selected Papers Presented at the International IMACS Symposium on Symbolic Computation, New Trends and Developments, (1996), Elsevier Science Publishers B. V Amsterdam, The Netherlands, The Netherlands), 571-582 · Zbl 1037.14503 [25] Hong, H.; Safey El Din, M., Variant quantifier elimination, Journal of Symbolic Computation, 47, 7, 883-901, (2011) · Zbl 1238.14001 [26] H. Iwane, H. Yanami, H. Anai, An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for optimization problems, in: Proceedings of the 2011 International Workshop on Symbolic-Numeric Computation, vol. 1, 2011, pp. 168-177. · Zbl 1346.68289 [27] H. Iwane, H. Yanami, H. Anai, K. Yokoyama, An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier elimination, in: Proceedings of the 2009 International Workshop on Symbolic-Numeric Computation, vol. 1, 2009, pp. 55-64. · Zbl 1356.68282 [28] Kaltofen, E.; Li, B.; Yang, Z.; Zhi, L., Exact certification of global optimality of approximate factorizations via rationalizing sums-of-squares with floating point scalars, (Proceedings of the Twenty-first International Symposium on Symbolic and Algebraic Computation, ISSAC’08, (2008), ACM New York, NY, USA), 155-164 [29] Krawczyk, R., Newton-algorithmen zur bestimmung von nullstellen mit fehlerschranken, Computing, 187-201, (1969) · Zbl 0187.10001 [30] Lampinen, J., Multiobjective nonlinear Pareto-optimization, (2000), Laboratory of Information Processing [31] Lasserre, J. B., Global optimization with polynomials and the problem of moments, SIAM Journal on Optimization, 11, 3, 796-817, (2001) · Zbl 1010.90061 [32] Loos, R.; Weispfenning, V., Applying linear quantifier elimination, The Computer Journal, 36, 5, 450-462, (1993) · Zbl 0787.03021 [33] McCallum, S., Solving polynomial strict inequalities using cylindrical algebraic decomposition, The Computer Journal, 432-438, (1993) · Zbl 0789.68080 [34] S. McCallum, An improved projection operator for cylindrical algebraic decomposition, in: Caviness and Johnson [10], pp. 242-268. · Zbl 0900.68279 [35] McCallum, S., On projection in CAD-based quantifier elimination with equational constraint, (Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation, ISSAC’99, (1999), ACM New York, NY, USA), 145-149 [36] McCallum, S., On propagation of equational constraints in CAD-based quantifier elimination, (Proceedings of the 2001 International Symposium on Symbolic and Algebraic Computation, ISSAC’01, (2001), ACM New York, NY, USA), 223-231 · Zbl 1356.68287 [37] P.A. Parrilo, S. Lall, Semidefinite programming relaxations and algebraic optimization in control, Mini-course on Polynomial Equations and Inequalities I and II, 2006. [38] Parrilo, P. A.; Sturmfels, B., Minimizing polynomial functions, (Algorithmic and Quantitative Aspects of Real Algebraic Geometry in Mathematics and Computer Science, vol. 60, (2001), ACM), 83-99 · Zbl 1099.13516 [39] Pistikopoulos, E.; Georgiadis, M.; Dua, V., Multi-parametric programming: theory, algorithms, and applications, (Multi-Parametric Programming, vol. 1, (2007), Wiley-VCH) [40] Ratschan, S., Approximate quantified constraint solving by cylindrical box decomposition, Reliable Computing, 8, 1, 21-42, (2002) · Zbl 0997.65077 [41] Rump, S. M., Algebraic computation, numerical computation and verified inclusions, (Janßen, R., Trends in Computer Algebra, Lecture Notes in Computer Science, vol. 296, (1988), Springer Berlin, Heidelberg), 177-197 · Zbl 0663.65043 [42] Rump, S. M., Computer-assisted proofs and self-validating methods, vol. 18 (chapter 10), pp. 195-240, (2005), Society for Industrial and Applied Mathematics Philadephia, PA [43] Safey El Din, M., Computing the global optimum of a multivariate polynomial over the reals, (Proceedings of the Twenty-first International Symposium on Symbolic and Algebraic Computation, ISSAC’08, (2008), ACM New York, NY, USA), 71-78 [44] Schattman, J., Portfolio optimization under nonconvex transaction costs with the global optimization toolbox [45] Schweighofer, M., Global optimization of polynomials using gradient tentacles and sums of squares, SIAM J. on Optimization, 17, September, 920-942, (2006) · Zbl 1118.13026 [46] Strzeboński, A. W., A real polynomial decision algorithm using arbitrary-precision floating point arithmetic, Reliable Computing, 5, 3, 337-346, (1999) · Zbl 1097.65526 [47] Strzeboński, A. W., Solving systems of strict polynomial inequalities, Journal of Symbolic Computation, 29, March, 471-480, (2000) · Zbl 0962.68183 [48] Strzeboński, A. W., Cylindrical algebraic decomposition using validated numerics, Journal of Symbolic Computation, 41, 9, 1021-1038, (2006) · Zbl 1124.68123 [49] T. Sturm, V. Weispfenning, Rounding and blending of solids by a real elimination method, in: Proceedings of the 15th IMACS World Congress on Scientific Computation, Modelling, and Applied Mathematics, IMACS 97, 1997, pp. 727-732. [50] Weispfenning, V., The complexity of linear problems in fields, Journal of Symbolic Computation, 5, February, 3-27, (1988) · Zbl 0646.03005 [51] Weispfenning, V., Quantifier elimination for real algebra — the quadratic case and beyond, AAECC, 8, 85-101, (1993) · Zbl 0867.03003 [52] Weispfenning, V., Simulation and optimization by quantifier elimination, Journal of Symbolic Computation, 24, August, 189-208, (1997) · Zbl 0883.68075 [53] Wilson, B.; Cappelleri, D.; Simpson, T. W.; Frecker, M., Efficient Pareto frontier exploration using surrogate approximations, Optimization and Engineering, 2, 31-50, (2001) · Zbl 1078.90574 [54] Winkler, F., (Polynomial Algorithms in Computer Algebra, Texts and Monographs in Symbolic Computation, (1996), Springer)