Dear Joseph:

I do not have an answer to your question, just a somewhat involved comment, I hope you won't mind me putting it in the list of answers.

The quantifier elimination approach you describe seems reasonable, but it might be that you cannot solve the problem this way, and the reason why I think that is by comparison to another decision problem, that of **connectedness** of semialgebraic sets.

Early in the theory of semialgebraic sets, one notices that such a set is connected if and only if there is a semialgebraic path between any two points. Moreover, it is fairly clear that the (quantifier-free) description complexity (number of equations/inequalities, degrees etc) of such paths is bounded for any given connected component. So if we can bound the description complexity of these paths in terms of the description complexity of the original sets, we can then write a quantified formula that says "the set is connected", and, using quantifier elimination, we have our decision algorithm.

**Problem: I do not know of any way of giving such an a priori bound.**

There is an algorithm to solve the decision problem, the *roadmap* algorithm (see e.g. Ch. 15 in the book by Basu, Pollack and Roy. Note that, from the roadmap algorithm, it is possible to deduce *a posteriori* bounds on the description complexity of the semialgebraic paths, but only once the problem is already solved.

The moral of the story is that, even though quantifier elimination is a wonderful tool (a hammer in this case), it makes us want to look for nails that are not necessarily there: sometimes it's easier to just go ahead and solve the problem "by hand" (and if you've looked at roadmap stuff, it gets very subtle) than to spend a lot of time looking for a complexity bound that will let you bring down the hammer.