An effective algorithm for quantifier elimination over algebraically closed fields using straight line programs

AbstractIn this paper we obtain an effective algorithm for quantifier elimination over algebraically closed fields: For every effective infinite integral domain k, closed under the extraction of pth roots when the characteristic p of k is positive, and every prenex formula ϑ with r blocks of quantifiers involving s polynomials F1, h., Fs ϵ k[X1, h.,Xn] encoded in dense form, there exists a well-parallelizable algorithm without divisions whose output is a quantifier-free formula equivalent to ϑ. The sequential complexity of this algorithm is bounded by O(¦ϑ¦) + D(O(n))r, where ¦ϑ¦ is the length of ϑ and D ≥ n is an upper bound for 1 + bEi = 1s deg Fi, and the polynomials in the output are encoded by means of a straight line program. The complexity bound obtained is better than the bounds of the known elimination algorithms, which are of the type ¦ϑ¦.Dncr, where c ≥ 2 is a constant. This becomes notorious when r = 1 (i.e., when there is only one block of quantifiers): the complexity bounds known up to now are not less than Dn2, while our bound is DO(n). Moreover, in the particular case that there is only one block of existential quantifiers and the input polynomials are given by a straight line program, we construct an elimination algorithm with even better bounds which depend on the length of this straight line program: Given a formula of the type ∃Xn−m+…,∃Xn:F1(X1,…,Xn=0 ∧ … ∧ Fs(X1,…,Xn)=0 ∧G1(X1,…,Xn)≠0 ∧ … ∧ Gs′(X1,…,Xn)≠0, where F1,h., Fs ϵ k[X1,h., Xn] are polynomials whose degrees in the m variables X − m + 1,h., Xn are bounded by an integer d ≥ m and G1,h.,Gs′ ϵ k[X1,h., Xn] are polynomials whose degrees in the same variables are bounded by an integer δ, this algorithm eliminates quantifiers in time L2.(s.s′.δ)O(1).dO(m), where L is the length of the straight line program that encodes F1,h., Fs, G1,h., Gs′.Finally, we construct a fast algorithm to compute the Chow Form of an irreducible projective variety.The construction of all the algorithms mentioned above relies on a preprocessing whose cost exceedes the complexity classes considered (they are based on the construction of correct test sequences). In this sense, our algorithms are non-uniform but may be considered uniform as randomized algorithms (choosing the correct test sequences randomly)