Abstract
Recently there has been a lot of activity in algorithms that work over real closed fields, and that perform such calculations as quantifier elimination or computing connected components of semi-algebraic sets. A cornerstone of this work is a symbolic sign determination algorithm due to Ben-Or, Kozen and Reif [2]. In this paper we describe a new sign determination method based on the earlier algorithm, but with two advantages: (i) It is faster in the univariate case, and (ii) In the general case, it allows purely symbolic quantifier elimination in pseudo-polynomial time. By purely symbolic, we mean that it is possible to eliminate a quantified variable from a system of polynomials no matter what the coefficient values are. The previous methods required the coefficients to be themselves polynomials in other variables. Our new method allows transcendental functions or derivatives to appear in the coefficients. Another corollary of the new sign-determination algorithm is a very simple, practical algorithm for deciding existentially-quantified formulae of the theory of the reals. We present an algorithm that has a bit complexity of n(k+1)dO(k) (c log n) (1+∈) randomized, or nn+1)dO(k2) c(1+∈) deterministic, for any ∈>0, where n is the number of polynomial constraints in the defining formula, k is the number of variables, d is a bound on the degree, c bounds the bit length of the coefficient. The algorithm makes no general position assumptions, and its constants are much smaller than other recent quantifier elimination methods.