An improved sign determination algorithm

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 [BOKR86]. 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 compares very well with numerical approaches, 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 and the number of arithmetic operations over the coefficient field increases with the degree of the coefficients. Our new method allows transcendental functions or derivatives to appear in the coefficients, and the number of arithmetic operations is completely independent of the coefficients.