Recently several theoretical single exponential time algorithms (in the number of variables) have been proposed for deciding the existential theory of reals. These algorithms have from a complexity analysis point of view a much better behaviour than CAD which was doubly exponential in the number of variables, but an efficient implementation based on these new ideas has never been performed yet. This paper is devote to the development of the following idea “it is possible to implement efficiently slight variants of single exponential methods well adapted to important particular cases of the decision problem”. We explain the main ideas, propose more efficient versions of the methods and make concrete propositions for future experiments*.

We exploit the fact that the set of all polynomials Pε@@@@[x1,..,xn] of degree ≤d which can be evaluated with ≤v nonscalar steps can be embedded into a Zariski-closed affine set W(d,n,v),dim W(d,n,v)≤(v+1 +n)2 and deg W(d,n,v)≤(2vd)(v+1+n)2. As a consequence we prove that for u:= 2v(d+1)2 and s:= 6(v+1+n)2 there exist a1,..,asε [u]n = {1,2,..,u}n such that for all polynomials PεW(d,n,v):P(a1) = p(a2) =...= p(as) = O implies PΞO. This means that a1,...,as is a correct test sequence for a zero test on all polynomials in W(d,n,v). Moreover, “almost every” sequence a1,..,asε[u]n is such a correct test sequence for W(d,n,v). The existence of correct test sequences a1,..,asε [u]n is established by a counting argument without constructing a correct test sequence. We even show that it is beyond the known methods to establish (i.e. to construct and to prove correctness) of such a short correct test sequence for W(d,n,v). We prove that given such a short, correct test sequence for W(d,n,v) we can efficiently construct a multivariate polynomial Pε@@@@[x1,..,xn] with deg(P) = d and small integer coefficients such that [email protected]@@@ W(d,n,v). For v>n log d lower bounds of this type are beyond our present methods in algebraic complexity theory.