Variant quantifier elimination. (English) Zbl 1238.14001
Summary: We describe an algorithm (VQE) for a variant of the real quantifier elimination problem (QE). The variant problem requires the input to satisfy a certain extra condition, and allows the output to be almost equivalent to the input. The motivation/rationale for studying such a variant QE problem is that many quantified formulas arising in applications do satisfy the extra conditions. Furthermore, in most applications, it is sufficient that the output formula is almost equivalent to the input formula. The main idea underlying the algorithm is to substitute the repeated projection step of CAD by a single projection without carrying out a parametric existential decision over the reals. We find that the algorithm can tackle important and challenging problems, such as numerical stability analysis of the widely-used MacCormack’s scheme. The problem has been practically out of reach for standard QE algorithms in spite of many attempts to tackle it. However, the current implementation of VQE can solve it in about 12 hours. This paper extends the results reported at the conference ISSAC 2009 [in: Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation, Seoul, July 28–31, 2009. New York, NY: Association for Computing Machinery (ACM). 183–190 (2009; Zbl 1237.14005)].
MSC:
| 14-04 | Software, source code, etc. for problems pertaining to algebraic geometry |
| 14Q15 | Computational aspects of higher-dimensional varieties |
| 68W30 | Symbolic computation and algebraic computation |
| 14P99 | Real algebraic and real-analytic geometry |
Citations:
Zbl 1237.14005References:
| [1] | Anai, H., Weispfenning, V., 2001. Reach set computations using real quantifier elimination. In: HSCC. pp. 63-76.; Anai, H., Weispfenning, V., 2001. Reach set computations using real quantifier elimination. In: HSCC. pp. 63-76. · Zbl 0991.93008 |
| [2] | Atiyah, M.; MacDonald, I., (Introduction to Commutative Algebra. Introduction to Commutative Algebra, Addison-Wesley Series in Mathematics (1969), Addison-Wesley) · Zbl 0175.03601 |
| [3] | Bank, B.; Giusti, M.; Heintz, J.; Pardo, L.-M., Generalized polar varieties and efficient real elimination procedure, Kybernetika, 40, 5, 519-550 (2004) · Zbl 1249.14019 |
| [4] | Bank, B.; Giusti, M.; Heintz, J.; Safey El Din, M.; Schost, E., On the geometry of polar varieties, Applicable Algebra in Engineering, Communication and Computing, 21, 1, 33-83 (2010) · Zbl 1186.14060 |
| [5] | Basu, S.; Pollack, R.; Roy, M.-F., On the combinatorial and algebraic complexity of quantifier elimination, Journal of ACM, 43, 6, 1002-1045 (1996) · Zbl 0885.68070 |
| [6] | Basu, S.; Pollack, R.; Roy, M.-F., Computing roadmaps of semi-algebraic sets on a variety, Journal of the AMS, 3, 1, 55-82 (1999) · Zbl 0933.14037 |
| [7] | Basu, S.; Pollack, R.; Roy, M.-F., Algorithms in Real Algebraic Geometry (2006), Springer-Verlag · Zbl 1102.14041 |
| [8] | Brown, C., Improved projection for cylindrical algebraic decomposition, Journal of Symbolic Computation, 32, 5, 447-465 (2001) · Zbl 0981.68186 |
| [9] | Brown, C., QEPCAD B: a program for computing with semi-algebraic sets using CADs, ACM SIGSAM Bulletin, 37, 4, 97-108 (2003) · Zbl 1083.68148 |
| [10] | Brown, C., 2009. Private communication.; Brown, C., 2009. Private communication. |
| [11] | Canny, J., Computing roadmaps in general semi-algebraic sets, The Computer Journal (1993) · Zbl 0798.14031 |
| [12] | Chen, C., Lemaire, F., Liyun, L., Moreno Maza, M., Pan, W., Xie, Y., 2009. Computing with constructible sets in maple. Journal of Symbolic Computation (submitted for publication).; Chen, C., Lemaire, F., Liyun, L., Moreno Maza, M., Pan, W., Xie, Y., 2009. Computing with constructible sets in maple. Journal of Symbolic Computation (submitted for publication). |
| [13] | Collins, G. E., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, (Lecture notes in computer science, vol. 33 (1975)), 515-532 |
| [14] | Collins, G. E., (Quantifier Elimination and Cylindrical Algebraic Decomposition. Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts and Monographs in Symbolic Computation (1998), Springer-Verlag), Ch. Quantifier elimination by cylindrical algebraic decomposition - 20 years of progress · Zbl 0900.03053 |
| [15] | Collins, G. E.; Hong, H., Partial cylindrical algebraic decomposition for quantifier elimination, Journal of Symbolic Computation, 12, 3, 299-328 (1991) · Zbl 0754.68063 |
| [16] | Coste, M.; Shiota, M., Nash triviality in families of nash manifolds, Inventiones Mathematicae, 108, 1, 349-368 (1992) · Zbl 0801.14017 |
| [17] | Eisenbud, D., Commutative Algebra with a View Toward Algebraic Geometry (1995), Springer-Verlag · Zbl 0819.13001 |
| [18] | Faugère, J.-C., 2011. FGb. http://www-salsa.lip6.fr/jcf; Faugère, J.-C., 2011. FGb. http://www-salsa.lip6.fr/jcf |
| [19] | Faugère, J.-C., A new efficient algorithm for computing Gröbner bases \((F_4)\), Journal of Pure and Applied Algebra, 139, 1-3, 61-88 (1999), effective methods in algebraic geometry (Saint-Malo, 1998) · Zbl 0930.68174 |
| [20] | Faugère, J.-C., A new efficient algorithm for computing Gröbner without reduction to zero (F5), (Proceedings of ISSAC 2002 (2002), ACM Press), 75-83 · Zbl 1072.68664 |
| [21] | Faugère, J.-C., Moroz, G., Rouillier, F., Safey El Din, M., 2008. Classification of the perspective-three-point problem, discriminant variety and real solving polynomial systems of inequalities. In: Proc. ISSAC. pp. 79-86.; Faugère, J.-C., Moroz, G., Rouillier, F., Safey El Din, M., 2008. Classification of the perspective-three-point problem, discriminant variety and real solving polynomial systems of inequalities. In: Proc. ISSAC. pp. 79-86. · Zbl 1487.68235 |
| [22] | Giusti, M.; Lecerf, G.; Salvy, B., A Gröbner free alternative for polynomial system solving, Journal of Complexity, 17, 1, 154-211 (2001) · Zbl 1003.12005 |
| [23] | Greuel, G.; Pfister, G., A Singular Introduction to Commutative Algebra (2007), Springer-Verlag · Zbl 1133.13001 |
| [24] | Grigoriev, D., Complexity of deciding tarski algebra, Journal of Symbolic Computation, 5, 1/2, 65-108 (1988) · Zbl 0689.03021 |
| [25] | Heintz, J., 1979. Definability bounds of first order theories of algebraically closed fields. In: Budach, L. (Eds.), Proceedings of Fundamentals of Computation Theory. pp. 160-166.; Heintz, J., 1979. Definability bounds of first order theories of algebraically closed fields. In: Budach, L. (Eds.), Proceedings of Fundamentals of Computation Theory. pp. 160-166. · Zbl 0439.03003 |
| [26] | Heintz, J.; Schnorr, C. P., Testing polynomials which are easy to compute (extended abstract), (STOC (1980), ACM), 262-272 · Zbl 0483.68043 |
| [27] | Hong, H., An improvement of the projection operator in cylindrical algebraic decomposition, (International Symposium of Symbolic and Algebraic Computation. International Symposium of Symbolic and Algebraic Computation, ISSAC-90 (1990), ACM), 261-264 |
| [28] | Hong, H., 1992. Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination. In: International Conference on Symbolic and Algebraic Computation ISSAC-92. pp. 177-188.; Hong, H., 1992. Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination. In: International Conference on Symbolic and Algebraic Computation ISSAC-92. pp. 177-188. · Zbl 0919.03029 |
| [29] | Hong, H., The exact region of stability for maccormack scheme, Computing, 56, 4, 371-384 (1996) · Zbl 0860.65083 |
| [30] | Hong, H.; Liska, R.; Steinberg, S., Testing stability by quantifier elimination, Journal of Symbolic Computation, 24, 2, 161-187 (1997) · Zbl 0886.65087 |
| [31] | Hong, H.; Safey El Din, M., Variant real quantifier elimination: algorithm and application, (ISSAC ’09: Proceedings of the 2009 international symposium on Symbolic and algebraic computation (2009), ACM: ACM New York, NY, USA), 183-190 · Zbl 1237.14005 |
| [32] | Hubert, E., 2003. Symbolic and Numerical Scientific Computation. Lecture Notes in Computer Science. Springer-Verlag, Ch. Notes on Triangular Sets and Triangulation-Decomposition Algorithms I: Polynomial Systems, pp. 143-158.; Hubert, E., 2003. Symbolic and Numerical Scientific Computation. Lecture Notes in Computer Science. Springer-Verlag, Ch. Notes on Triangular Sets and Triangulation-Decomposition Algorithms I: Polynomial Systems, pp. 143-158. |
| [33] | Jirstrand, M., Nonlinear control system design by quantifier elimination, Journal of Symbolic Computation, 24, 2, 137-152 (1997) · Zbl 0882.93022 |
| [34] | Kreiss, H.-O.; Lorenz, J., Initial-Boundary value problems and the Navier-Stokes equations, (Pure and Applied Mathematics, vol. 136 (1989), Academic Press, Inc. (London) Ltd) · Zbl 0728.76084 |
| [35] | Lax, P.; Wendroff, B., Systems of conservation laws, Commun. Pure Appl Math., 13, 217-237 (1960) · Zbl 0152.44802 |
| [36] | Lecerf, G., Computing the equidimensional decomposition of an algebraic closed set by means of lifting fibers, Journal of Complexity, 19, 4, 564-596 (2003) · Zbl 1230.68222 |
| [37] | LeVeque, R. J., High-resolution conservative algorithms for advection in incompressible flow, SIAM Journal of Numerical Analysis, 33, 2, 627-665 (1996) · Zbl 0852.76057 |
| [38] | Liska, R.; Steinberg, S., Applying quantifier elimination to stability analysis of difference schemes, The Computer Journal, 36, 5, 497-503 (1993) · Zbl 0780.68075 |
| [39] | MacCormack, R.W., 1969. The effect of viscosity in hypervelocity impact cratering. In: Proceedings of AIAA Hypervelocity Impact Conference. AIAA paper, pp. 69-354.; MacCormack, R.W., 1969. The effect of viscosity in hypervelocity impact cratering. In: Proceedings of AIAA Hypervelocity Impact Conference. AIAA paper, pp. 69-354. |
| [40] | McCallum, S., 1984. An improved projection operator for Cylindrical Algebraic Decomposition. Ph.D. Thesis, University of Wisconsin-Madison.; McCallum, S., 1984. An improved projection operator for Cylindrical Algebraic Decomposition. Ph.D. Thesis, University of Wisconsin-Madison. |
| [41] | McCallum, S., 1999. On projection in cad-based quantifier elimination with equational constraint. In: Proc. ISSAC. pp. 145-149.; McCallum, S., 1999. On projection in cad-based quantifier elimination with equational constraint. In: Proc. ISSAC. pp. 145-149. |
| [42] | Moroz, G., Rouillier, F., 2007. OpenCAD. package.; Moroz, G., Rouillier, F., 2007. OpenCAD. package. |
| [43] | Renegar, J., On the computational complexity and geometry of the first order theory of the reals, Journal of Symbolic Computation, 13, 3, 255-352 (1992) · Zbl 0798.68073 |
| [44] | Rouillier, F., 2011. RS, RealSolving. http://fgbrs.lip6.fr; Rouillier, F., 2011. RS, RealSolving. http://fgbrs.lip6.fr |
| [45] | Safey El Din, M., 2007a. RAGLib (Real Algebraic Geometry Library), Maple package. http://www-salsa.lip6.fr/ safey/RAGLib; Safey El Din, M., 2007a. RAGLib (Real Algebraic Geometry Library), Maple package. http://www-salsa.lip6.fr/ safey/RAGLib |
| [46] | Safey El Din, M., Testing sign conditions on a multivariate polynomial and applications, Mathematics in Computer Science, 1, 1, 177-207 (2007) · Zbl 1126.14068 |
| [47] | Safey El Din, M.; Schost, E., Polar varieties and computation of one point in each connected compon ent of a smooth real algebraic set, (Sendra, J., International Symposium on Symbolic and Algebraic Computation 2003 — ISSAC’2003. International Symposium on Symbolic and Algebraic Computation 2003 — ISSAC’2003, Philadelphie, USA (2003), ACM Press), 224-231 · Zbl 1072.68693 |
| [48] | Safey El Din, M.; Schost, E., A baby steps/giant steps monte carlo algorithm for computing roadmaps in smooth compact real hypersurfaces, Discrete and Computational Geometry, 45, 1, 181-220 (2011) · Zbl 1213.14110 |
| [49] | Shafarevich, I., Basic Algebraic Geometry 1 (1977), Springer Verlag · Zbl 0362.14001 |
| [50] | Strikwerda, J.C., 1976. Initial boundary value problems for incompletely parabolic systems. Stanford Univ Calif Dept of Computer Science.; Strikwerda, J.C., 1976. Initial boundary value problems for incompletely parabolic systems. Stanford Univ Calif Dept of Computer Science. · Zbl 0351.35051 |
| [51] | Strzebonski, A., Cylindrical algebraic decomposition using validated numerics, Journal of Symbolic Computation, 41, 9, 1021-1038 (2006) · Zbl 1124.68123 |
| [52] | Sturm, T., Weispfenning, V., 1996. Computational geometry problems in redlog. In: ADG. pp. 58-96.; Sturm, T., Weispfenning, V., 1996. Computational geometry problems in redlog. In: ADG. pp. 58-96. · Zbl 0904.65151 |
| [53] | Tarski, A., A Decision Method for Elementary Algebra and Geometry (1951), University of California Press · Zbl 0044.25102 |
| [54] | Yanami, H.; Anai, H., The maple package synrac and its application to robust control design, Future Generation Computer Systems, 23, 5, 721-726 (2007) |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
