Christopher W. Brown
James H. Davenport
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.
- Basu, S. New results on quantifier elimination over real closed fields and applications to constraint databases. Journal of the ACM 46, 4 (1999), 537--555. Google Scholar
Digital Library
- Basu, S., Pollack, R., and Roy, M.-F. On the combinatorial and algebraic complexity of quantifier elimination. J. ACM 43, 6 (1996), 1002--1045. Google ScholarDigital Library
- Beaumont, J., Bradford, R., Davenport, J., and Phisanbut, N. Adherence is better than adjacency. In Proceedings ISSAC 2005 (2005), M. Kauers, Ed., pp. 37--44. Google ScholarDigital Library
- Brown, C. W. Guaranteed solution formula construction. In Proc. International Symposium on Symbolic and Algebraic Computation (1999), pp. 137--144. Google ScholarDigital Library
- Brown, C. W. Simple CAD construction and its applications. Journal of Symbolic Computation 31, 5 (May 2001), 521--547. Google ScholarDigital Library
- Davenport, J. H., and Heintz, J. Real quantifier elimination is doubly exponential. Journal of Symbolic Computation 5 (1988), 29--35. Google ScholarDigital Library
- Dolzmann, A., Seidl, A., and Sturm, T. Efficient projection orders for CAD. In Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation (ISSAC 2004) (Santander, Spain, July 2004), J. Gutierrez, Ed., ACM. Google ScholarDigital Library
- Dolzmann, A., and Sturm, T. Redlog: Computer algebra meets computer logic. ACM SIGSAM Bulletin 31, 2 (June 1997), 2--9. Google ScholarDigital Library
- Dolzmann, A., Sturm, T., and Weispfenning, V. A new approach for automatic theorem proving in real geometry. Journal of Automated Reasoning 21, 3 (1998), 357--380. Google ScholarDigital Library
- Heintz, J. Definability and fast quantifier elimination in algebraically closed fields. Theoretical Computer Science 24 (1983), 239--277.Google ScholarCross Ref
- 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.Google Scholar
- Hong, H. Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination. In Proc. International Symposium on Symbolic and Algebraic Computation (1992), pp. 177--188. Google ScholarDigital Library
- Ibarra, O. H., and Leininger, B. S. The complexity of the equivalence problem for straight-line programs. In STOC '80: Proceedings of the twelfth annual ACM symposium on Theory of computing (New York, NY, USA, 1980), ACM Press, pp. 273--280. Google ScholarDigital Library
- Kaltofen, E. Greatest common divisors of polynomials given by straight-line programs. J. ACM 35, 1 (1988), 231--264. Google ScholarDigital Library
- Lazard, D., and Rouillier, F. Solving parametric polynomial systems. Tech. rep., INRIA, October 2004.Google Scholar
- Renegar, J. On the computational complexity and geometry of the first-order theory of the reals, parts I-III. Journal of Symbolic Computation 13 (1992), 255--352. Google ScholarDigital Library
- Risler, J.-J. Additive complexity and zeros of real polynomials. SIAM J. Comput. 14, 1 (1985), 178--183.Google ScholarCross Ref
- Rojas, J. M. Additive complexity and roots of polynomials over number fields and p-adic fields. In ANTS (2002), pp. 506--516. Google ScholarDigital Library
- Seidl, A., and Sturm, T. A generic projection operator for partial cylindrical algebraic decomposition. In Proc. International Symposium on Symbolic and Algebraic Computation (2003), R. Sendra, Ed., pp. 240--247. Google ScholarDigital Library
- 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.Google Scholar
- Weispfenning, V. The complexity of linear problems in fields. J. Symb. Comput. 5, 1--2 (1988), 3--27. Google ScholarDigital Library
Index Terms
- The complexity of quantifier elimination and cylindrical algebraic decomposition
Recommendations
On the combinatorial and algebraic complexity of quantifier elimination
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 ...
Tree-depth, quantifier elimination, and quantifier rank
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer ScienceFor a class K of finite graphs we consider the following three statements. (i) K has bounded tree-depth. (ii) First-order logic FO has an effective generalized quantifier elimination on K. (iii) The parameterized model checking for FO on K is in para-...
Some Complete and Intermediate Polynomials in Algebraic Complexity Theory
CSR 2016: Proceedings of the 11th International Computer Science Symposium on Computer Science --- Theory and Applications - Volume 9691We provide a list of new natural $$\mathsf {VNP}$$-Intermediate polynomial families, based on basic combinatorial $$\mathsf {NP}$$-Complete problems that are complete under parsimonious reductions. Over finite fields, these families are in $$\mathsf {...
Comments