IMPROVED ALGORITHMS FOR SIGN DETERMINATION AND EXISTENTIAL QUANTIFIERELIMINATION

Authors
Citation
J. Canny, IMPROVED ALGORITHMS FOR SIGN DETERMINATION AND EXISTENTIAL QUANTIFIERELIMINATION, Computer journal, 36(5), 1993, pp. 409-418
Citations number
24
Categorie Soggetti
Computer Sciences","Computer Applications & Cybernetics
Journal title
ISSN journal
00104620
Volume
36
Issue
5
Year of publication
1993
Pages
409 - 418
Database
ISI
SICI code
0010-4620(1993)36:5<409:IAFSDA>2.0.ZU;2-U
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 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.