On the combinatorial and algebraic complexity of quantifier elimination

ABSTRACT

In this paper, a new algorithm for performing quantifier elimination from first order formulas over real closed fields in given. This algorithm improves the complexity of the asymptotically fastest algorithm for this problem, known to this data. A new feature of this algorithm is that the role of the algebraic part (the dependence on the degrees of the imput polynomials) and the combinatorial part (the dependence on the number of polynomials) are sparated. Another new feature is that the degrees of the polynomials in the equivalent quantifier-free formula that is output, are independent of the number of input polynomials. As special cases of this algorithm new and improved algorithms for deciding a sentence in the first order theory over real closed fields, and also for solving the existential problem in the first order theory over real closed fields, are obtained.

REFERENCES

• 1: M. E. Alonso , E. Becker , M.-F. Roy , T. Wörmann, Zeros, multiplicities, and idempotents for zero-dimensional systems, Algorithms in algebraic geometry and applications, Birkhauser Verlag, Basel, Switzerland, 1996
• 2: ~ATIYAH, M. F., AND MACONALD, I.G. 1969. Introduction to Commutative Algebra. Addison-Wesley, ~Reading, Pa.
• 3: ~BASU, S., POLLACK, R., AND ROY, M.-F. A new algorithm to find a point in every cell defined by a ~family of polynomials. In Quantifier Elimination and Cylindrical Algebraic Decomposition. B. ~Caviness and J. Johnson, eds. Springer-Verlag, New York, to appear.
• 4: Saugata Basu , Richard Pollack , Marie-Françoise Roy, Computing a set of points meeting every cell defined by a family of polynomials on a variety, Proceedings of the workshop on Algorithmic foundations of robotics, p.537-555, May 1995, San Francisco, California, United States
• 5: ~BASU, S., POLLACK, R., AND ROY, M. F. 1996. On the number of cells defined by a family of ~polynomials on a variety. Mathematika 43, 120-126.
• 6: ~BAsu, S., POLLACK, R., AND ROY, M.F. 1994. On the combinatorial and algebraic complexity of ~quantifier elimination. In Proceedings of the 35th IEEE Symposium on Foundations of Computer ~Science. IEEE, New York, pp. 632-641.
• 7: Michael Ben-Or , Dexter Kozen , John Reif, The complexity of elementary algebra and geometry, Journal of Computer and System Sciences, v.32 n.2, p.251-264, April 1986 [doi>10.1016/0022-0000(86)90029-2]
• 8: Stuart J. Berkowitz, On computing the determinant in small parallel time using a small number of processors, Information Processing Letters, v.18 n.3, p.147-150, March 1984 [doi>10.1016/0020-0190(84)90018-8]
• 9: ~BOCHNAK, J., COSTE, M., AND ROY, M.F. 1987. G~om~trie alg~btique r~elle. Springer-Verlag, New ~York.
• 10: ~BUCHBEROER, B. 1985. Gr6bner bases: An algorithmic method in polynomial ideal theory. In ~Recent Trends in Multidimensional Systems Theory. Reider, ed. Bose.
• 11: John Canny, Some algebraic and geometric computations in PSPACE, Proceedings of the twentieth annual ACM symposium on Theory of computing, p.460-469, May 02-04, 1988, Chicago, Illinois, United States [doi>10.1145/62212.62257]
• 12: ~CANNY, J. 1993a. Some practical tools for algebraic geometry. Tech. rep. Spring school on robot ~motion planning at Rodez, France. PROMOTION ESPRIT, pp. 39-52.
• 13: John F. Canny, An Improved Sign Determination Algorithm, Proceedings of the 9th International Symposium, on Applied Algebra, Algebraic Algorithms and Error-Correcting Codes, p.108-117, October 07-11, 1991
• 14: ~CANNY, J. 1993b. Improved algorithms for sign determination and existential quantifier elimina- ~tion. Comput. J. 36, 409-418.
• 15: ~COLLINS, G.E. 1975. Quantifier elimination for real closed fields by cylindrical algebraic decom- ~position. In Springer Lecture Notes in Computer Science 33, 515-532.
• 16: M. Coste, Thoms's lemma, the coding of real algebraic numbers and the computation of the topology of semi-algebraic sets, Journal of Symbolic Computation, v.5 n.1-2, p.121-129, February/April 1988 [doi>10.1016/S0747-7171(88)80008-7]
• 17: ~GIusTI, M., AND HEINTZ, J. 1991. La d6termination des points isol6s d'une vari6t6 alg6brique peut ~se faire en temps polynomial. In Proceedings of the International Meeting on Commutative Algebra. ~Cortona.
• 18: D. Yu. Grigor'ev, Complexity of deciding Tarski algebra, Journal of Symbolic Computation, v.5 n.1-2, p.65-108, February/April 1988 [doi>10.1016/S0747-7171(88)80006-3]
• 19: D. Yu. Grigor'ev , N. N. Vorobjov, Solving systems of polynomial inequalities in subexponential time, Journal of Symbolic Computation, v.5 n.1-2, p.37-64, February/April 1988 [doi>10.1016/S0747-7171(88)80005-1]
• 20: D. Yu. Grigor'ev , N. N. Vorobjov, Jr., Counting connected components of a semialgebraic set in subexponential time, Computational Complexity, v.2 n.2, p.133-186, 1992 [doi>10.1007/BF01202001]
• 21: ~HEINTZ, J., RoY, M.-F., AND SOLERN6, P. 1990. Sur la complexit6 du principe de Tarski- ~Seidenberg. Bull. Soc. Math. France 118, 101-126.
• 22: ~HEINTZ, J., RoY, M.-F., AND SOLERN0, P. 1989. On the Complexity of Semi-Algebraic Sets. In ~Proceedings oflFIP '89 (San Francisco, Calif.). North-Holland, Amsterdam, The Netherlands, pp. ~293-298.
• 23: ~KOIRAN, P. 1993. A weak version of the Blum, Shub & Smale model. In Proceedings of the 34th ~IEEE Symposium on Foundations of Computer Science. IEEE, New York, pp. 486-495.
• 24: T. Krick , L. M. Pardo, A computational method for diophantine approximation, Algorithms in algebraic geometry and applications, Birkhauser Verlag, Basel, Switzerland, 1996
• 25: Maurice Mignotte, Mathematics for computer algebra, Springer-Verlag New York, Inc., New York, NY, 1992
• 26: Bhubaneswar Mishra, Algorithmic algebra, Springer-Verlag New York, Inc., New York, NY, 1993
• 27: ~POLLACK, R., AND ROY, M.-F. 1993. On the number of cells defined by a set of polynomials. C. R. ~Acad. Sci. Paris 316, 573-577.
• 28: ~PEDERSEN, P., RoY, M.-F., AND SZPIRGLAS, A. 1993. Counting real zeros in the multivariate case. ~In Computational algebraic geometry, Eyssette et Galligo, eds. Progress in Mathematics, vol. 109. ~Birkhauser, pp. 203-224.
• 29: ~RENEOAR, J. 1991. Recent progress on the complexity of the decision problem for the reals. In ~Discrete and Computational Geometry: Papers from the DIMACS Special Year. DIMACS series in ~Discrete Mathematics and Theoretical Computer Science, vol. 6. AMS-ACM, New York, pp. 287-308.
• 30: James Renegar, On the computational complexity and geometry of the first-order theory of the reals. Par I: Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals, Journal of Symbolic Computation, v.13 n.3, p.255-299, March 1992
• 31: ~RoY, M.-F. Basic algorithms in real algebraic geometry: From Sturm theorem to the existential ~theory of reals. Lectures on real geometry in memoriam of Mario Raimondo. In de Gruyter ~Expositions in Mathematics, to appear.
• 32: Marie-Françoise Roy , Aviva Szpirglas, Complexity of computation on real algebraic numbers, Journal of Symbolic Computation, v.10 n.1, p.39-51, July 1990 [doi>10.1016/S0747-7171(08)80035-1]
• 33: Marie-Françoise Roy , Nicolai Vorobjov, Finding irreducible components of some real transcendental varieties, Computational Complexity, v.4 n.2, p.107-132, April 1994 [doi>10.1007/BF01202285]
• 34: ~SEIDENBERG, A. 1954. A new decision method for elementary algebra. Ann. Math. 60, 365-374.
• 35: ~TARSKI, A. 1951. A decision method for elementary algebra and geometry. University of Califor- ~nia Press.
• 36: VAN DER WAERDEN, B.L. 1950. Modern Algebra, Volume II. F. Ungar Publishing Co.
• 37: VOROBJOV, N. 1984. Bounds of real roots of a system of algebraic equations. In Notes of Science ~Seminars of Leningrad Department of Math, Vol. 137. (St. Petersburg, Fla.). Steklov Institute, 7-19.
• 38: ~WALKER, R.J. 1950. Algebraic curves. Princeton University Press, Princeton, NJ.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Decision problems

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.1 Numerical Algorithms and Problems
          Subjects: Computations on polynomials

General Terms:
Algorithms, Theory

Keywords:
Tarski-Seidenberg principle, quantifier elimination, real closed fields