IMPROVED ALGORITHMS FOR SIGN DETERMINATION AND EXISTENTIAL QUANTIFIERELIMINATION

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 sig n determination method based on the earlier algorithm, but with two ad vantages: (i) It is faster in the univariate case, and (ii) In the gen eral case, it allows purely symbolic quantifier elimination in pseudo- polynomial time. By purely symbolic, we mean that it is possible to el iminate a quantified variable from a system of polynomials no matter w hat the coefficient values are. The previous methods required the coef ficients to be themselves polynomials in other variables. Our new meth od allows transcendental functions or derivatives to appear in the coe fficients. Another corollary of the new sign-determination algorithm i s a very simple, practical algorithm for deciding existentially-quanti fied formulae of the theory of the reals. We present an algorithm that has a bit complexity of n(k+1)d(O)(k)(c log n)(1+epsilon) randomized, or n(k+1)d(O)(k2)c(1+epsilon) deterministic, for any epsilon > 0, whe re 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 coefficients. The algorithm makes no general positi on assumptions, and its constants are much smaller than other recent q uantifier elimination methods.