The complexity of quantifier elimination and cylindrical algebraic decomposition

ABSTRACT

This paper has two parts. In the first part we give a simple and constructive proof that quantifier elimination in real algebra is doubly exponential, even when there is only one free variable and all polynomials in the quantified input are linear. The general result is not new, but we hope the simple and explicit nature of the proof makes it interesting. The second part of the paper uses the construction of the first part to prove some results on the effects of projection order on CAD construction -- roughly that there are CAD construction problems for which one order produces a constant number of cells and another produces a doubly exponential number of cells, and that there are problems for which all orders produce a doubly exponential number of cells. The second of these results implies that there is a true singly vs. doubly exponential gap between the worst-case running times of several modern quantifier elimination algorithms and CAD-based quantifier elimination when the number of quantifier alternations is constant.

REFERENCES

• 1: Saugata Basu, New results on quantifier elimination over real closed fields and applications to constraint databases, Journal of the ACM (JACM), v.46 n.4, p.537-555, July 1999 [doi>10.1145/320211.320240]
• 2: Saugata Basu , Richard Pollack , Marie-Françoise Roy, On the combinatorial and algebraic complexity of quantifier elimination, Journal of the ACM (JACM), v.43 n.6, p.1002-1045, Nov. 1996 [doi>10.1145/235809.235813]
• 3: James C. Beaumont , Russell J. Bradford , James H. Davenport , Nalina Phisanbut, Adherence is better than adjacency: computing the Riemann index using CAD, Proceedings of the 2005 international symposium on Symbolic and algebraic computation, p.37-44, July 24-27, 2005, Beijing, China [doi>10.1145/1073884.1073892]
• 4: Christopher W. Brown, Guaranteed solution formula construction, Proceedings of the 1999 international symposium on Symbolic and algebraic computation, p.137-144, July 28-31, 1999, Vancouver, British Columbia, Canada [doi>10.1145/309831.309890]
• 5: Christopher W. Brown, Simple CAD construction and its applications, Journal of Symbolic Computation, v.31 n.5, p.521-547, May 2001 [doi>10.1006/jsco.2000.0394]
• 6: James H. Davenport , Joos Heintz, Real quantifier elimination is doubly exponential, Journal of Symbolic Computation, v.5 n.1-2, p.29-35, February/April 1988 [doi>10.1016/S0747-7171(88)80004-X]
• 7: Andreas Dolzmann , Andreas Seidl , Thomas Sturm, Efficient projection orders for CAD, Proceedings of the 2004 international symposium on Symbolic and algebraic computation, p.111-118, July 04-07, 2004, Santander, Spain [doi>10.1145/1005285.1005303]
• 8: Andreas Dolzmann , Thomas Sturm, REDLOG: computer algebra meets computer logic, ACM SIGSAM Bulletin, v.31 n.2, p.2-9, June 1997 [doi>10.1145/261320.261324]
• 9: Andreas Dolzmann , Thomas Sturm , Volker Weispfenning, A New Approach for Automatic Theorem Proving in Real Geometry, Journal of Automated Reasoning, v.21 n.3, p.357-380, December 1998 [doi>10.1023/A:1006031329384]
• 10: Heintz, J. Definability and fast quantifier elimination in algebraically closed fields. Theoretical Computer Science 24 (1983), 239--277.
• 11: Hong, H. Comparison of several decision algorithms for the existential theory of the reals. Tech. Rep. 91--41, Research Institute for Symbolic Computation (RISC-Linz), 1991.
• 12: Hoon Hong, Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination, Papers from the international symposium on Symbolic and algebraic computation, p.177-188, July 27-29, 1992, Berkeley, California, United States [doi>10.1145/143242.143306]
• 13: Oscar H. Ibarra , Brian S. Leininger, The complexity of the equivalence problem for straight-line programs, Proceedings of the twelfth annual ACM symposium on Theory of computing, p.273-280, April 28-30, 1980, Los Angeles, California, United States [doi>10.1145/800141.804675]
• 14: Erich Kaltofen, Greatest common divisors of polynomials given by straight-line programs, Journal of the ACM (JACM), v.35 n.1, p.231-264, Jan. 1988 [doi>10.1145/42267.45069]
• 15: Lazard, D., and Rouillier, F. Solving parametric polynomial systems. Tech. rep., INRIA, October 2004.
• 16: James Renegar, On the computational complexity and geometry of the first-order theory of the reals. Part III: quantifier elimination, Journal of Symbolic Computation, v.13 n.3, p.329-352, March 1992
• 17: Risler, J.-J. Additive complexity and zeros of real polynomials. SIAM J. Comput. 14, 1 (1985), 178--183.
• 18: J. Maurice Rojas, Additive Complexity and Roots of Polynomials over Number Fields and \mathfrak{p} -adic Fields, Proceedings of the 5th International Symposium on Algorithmic Number Theory, p.506-516, July 07-12, 2002
• 19: Andreas Seidl , Thomas Sturm, A generic projection operator for partial cylindrical algebraic decomposition, Proceedings of the 2003 international symposium on Symbolic and algebraic computation, p.240-247, August 03-06, 2003, Philadelphia, PA, USA [doi>10.1145/860854.860903]
• 20: Sturm, T. Real Quantifier Elimination in Geometry. PhD thesis, Department of Mathematics and Computer Science. University of Passau, Germany, D-94030 Passau, Germany, December 1999.
• 21: Volker Weispfenning, The complexity of linear problems in fields, Journal of Symbolic Computation, v.5 n.1-2, p.3-27, February/April 1988 [doi>10.1016/S0747-7171(88)80003-8]

INDEX TERMS

Primary Classification:
  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

General Terms:
Algorithms, Theory

Keywords:
cylindrical algebraic decomposition, quantifier elimination