New results on quantifier elimination over real closed fields and applications to constraint databases

ABSTRACT

In this paper, we give a new algorithm for quantifier elimination in the first order theory of real closed fields that improves the complexity of the best known algorithm for this problem till now. Unlike previously known algorithms [Basu et al. 1996; Renegar 1992; Heintz et al. 1990], the combinatorial part of the complexity (the part depending on the number of polynomials in the input) of this new algorithm is independent of the number of free variables. Moreover, under the assumption that each polynomial in the input depends only on a constant number of the free variables, the algebraic part of the complexity(the part depending on the degrees of the input polynomials) can also be made independent of the number of free variables. This new feature of our algorithm allow us to obtain a new algorithm for a variant of the quantifier elimination problem. We give an almost optimal algorithm for this new problem, which we call the uniform quantifier elimination problem.Using tthe uniform quantifier elimination algorithm, we give an algorithm for solving a problem arising in the field of constraint databases with real polynomial constraints. We give an algorithm for converting a query with natural domain semantics to an equivalent one with active domain semantics. A nonconstructive version of this result was proved in Benedikt et al. [1998]. Very recently, a constructive proof was also given independently in Benedikt and Libkin [1997]. However, complexity issues were not considered and no algorithm with a reasonable complexity bound was known for this latter problem till now.We also point out interesting logical consequences of this algorithmic result, concerning the expressive power of a constraint query language over the reals. This leads to simpler and constructive proofs for these inexpressibility results than the ones known before.Moreover, our improved algorithm for performing quantifier elimination immediately leads to improved algorithms for several problems for which quantifier elimination is a basic step, for example, the problem of computing the closure of a given semi-algebraic set.

REFERENCES

• 1: AGARWAL, P. K., AND MATOUSEK, J. 1994. On range searching with semi-algebraic sets. Disc. Computat. Geom. 11, 393-418.
• 2: Saugata Basu, Uniform quantifier elimination and constraint query processing, Proceedings of the 1997 international symposium on Symbolic and algebraic computation, p.21-27, July 21-23, 1997, Kihei, Maui, Hawaii, United States [doi>10.1145/258726.258739]
• 3: 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]
• 4: Saugata Basu , Richard Pollack , Marie-Françoise Roy, Complexity of computing semi-algebraic descriptions of the connected components of a semi-algebraic set, Proceedings of the 1998 international symposium on Symbolic and algebraic computation, p.25-29, August 13-15, 1998, Rostock, Germany [doi>10.1145/281508.281533]
• 5: S. Basu, On the Combinatorial and Topological Complexity of a Single Cell, Proceedings of the 39th Annual Symposium on Foundations of Computer Science, p.606, November 08-11, 1998
• 6: Michael Benedikt , Guozhu Dong , Leonid Libkin , Limsoon Wong, Relational expressive power of constraint query languages, Journal of the ACM (JACM), v.45 n.1, p.1-34, Jan. 1998 [doi>10.1145/273865.273870]
• 7: Michael Benedikt , Leonid Libkin, On the Structure of Queries in Constraint Query Languages, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.25, July 27-30, 1996
• 8: Michael Benedikt , Leonid Libkin, Languages for relational databases over interpreted structures, Proceedings of the sixteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.87-98, May 11-15, 1997, Tucson, Arizona, United States [doi>10.1145/263661.263672]
• 9: BOCHNAK, J., COSTE, M., AND ROY, M.-F. 1987. Gdomdtric algdbrique rOeile. Springer-Verlag, New York.
• 10: Bernard Chazelle, Computational geometry: a retrospective, Proceedings of the twenty-sixth annual ACM symposium on Theory of computing, p.75-94, May 23-25, 1994, Montreal, Quebec, Canada [doi>10.1145/195058.195110]
• 11: COLLINS, G.E. 1975. Quantifier elimination for real closed fields by cylindrical algebraic decom-position. In Lecture Notes in Computer Science, vol. 33. Springer-Verlag, New York, pp. 515-532.
• 12: 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]
• 13: EHRENFEUCHT, A. 1961. An application of games to the completeness problem for formalized theories. Fund. Math 49, 129-141.
• 14: Ronald Fagin, Finite-model theory—a personal perspective, Theoretical Computer Science, v.116 n.1, p.3-31, Aug. 2, 1993
• 15: GAIFMAN, H. 1981. On local and non-local properties. In Proceedings of the Herbrand Symposium Logic Colloquium. North-Holland, Amsterdam, The Netherlands, pp. 105-135.
• 16: Stéphane Grumbach , Jianwen Su, Queries with arithmetical constraints, Theoretical Computer Science, v.173 n.1, p.151-181, Feb. 1997 [doi>10.1016/S0304-3975(96)00194-6]
• 17: Stéphane Grumbach , Jianwen Su, Finitely representable databases (extended abstract), Proceedings of the thirteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.289-300, May 24-27, 1994, Minneapolis, Minnesota, United States [doi>10.1145/182591.182654]
• 18: Stéphane Grumbach , Jianwen Su, Dense-order constraint databases (extended abstract), Proceedings of the fourteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.66-77, May 22-25, 1995, San Jose, California, United States [doi>10.1145/212433.212453]
• 19: 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]
• 20: GUREVICH, Y. 1988. Logic and the challenge of computer science. In Current Trends in Theoretical Computer Science. Computer Science Press, Rockville, Md., pp. 1-57.
• 21: HALPERIN, D., AND SHARIR, M. 1994. New bounds for lower envelopes in three dimensions, with applications to visibility in terrains. Disc. Computat. Geom. 12, 313-326.
• 22: HALPERIN, D., AND SHARIR, M. 1995. Almost tight upper bounds for the single cell and zone problems in three dimensions. Disc. Computat. Geom. 14, 385-410.
• 23: HEINTZ, J., ROY, M. F., AND SOLERNO, P. 1990. Sur la complexit6 du principe de Tarski- Seidenberg. Bull. Soc. Math France 118, 101-126.
• 24: HEINTZ, J., ROY, M.-F., AND SOLERNO, P. 1994. Description of the connected components of a semialgebraic set in single exponential time. Disc. Computat. Geom. 11, 121-140.
• 25: Paris C. Kanellakis , Dina Q. Goldin, Constraint Programming and Database Query Languages, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.96-120, April 19-22, 1994
• 26: Paris C. Kanellakis , Gabriel M. Kuper , Peter Z. Revesz, Constraint query languages (preliminary report), Proceedings of the ninth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.299-313, April 02-04, 1990, Nashville, Tennessee, United States [doi>10.1145/298514.298582]
• 27: 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
• 28: SEIDENBERG, A. 1954. A new decision method for elementary algebra. Ann. Math. 60, 365-374.
• 29: SHARIR, M. 1994. Almost tight upper bounds for lower envelopes in higher dimensions. Disc. Computat. Geom. 12, 327-345.
• 30: TARSKI, A. 1951. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley, Calif.
• 31: Jeffrey D. Ullman, Principles of Database Systems, W. H. Freeman & Co., New York, NY, 1983
• 32: 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]
• 33: ZIEGLER, G.M. 1994. Lectures on Polytopes. Springer-Verlag, New York.

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:
  H. Information Systems
  H.2 DATABASE MANAGEMENT
      H.2.3 Languages
          Subjects: Query languages

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.2 Algorithms
          Subjects: Algebraic algorithms

General Terms:
Algorithms, Theory