Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Is there a way to determine exactly (without the use of approximation methods) whether $p\in \mathbb{R}[x_1,\dots,x_n]$ has real-valued solutions.

Algorithms based on Sturm's theorem seem to be applicable to univariate polynomials only.

share|improve this question
2  
There are also multivariate versions of Sturm's theorem. –  J.C. Ottem Dec 15 '11 at 12:58

2 Answers 2

up vote 6 down vote accepted

Tarski's theorem on the decidability of the theory of real-closed fields provides a general algorithm that decides any question expressible in the first order language of real-closed fields. His algorithm can therefore determine, for any statement, whether it is true in the structure $\langle\mathbb{R},+,\cdot,0,1,\lt\rangle$. Thus, not only are the purely existential assertions (solvability of systems of equations) decidable in this context, but also more complex assertions involving iterated quantifiers, which would not seem without this result to be decidable even by approximation.

The way Tarski's argument proceeds is by elimination of quantifiers: every assertion in this language is equivalent to a quantifier-free assertion. In particular, the existence of a solution to $p(\vec x)=0$ is equivalent by Tarski's reduction to a quantifier-free assertion about the coefficients of the polynomial. That is, the algorithm reduces the question to a mere calculation involving the coefficients.

But if you are interested in actually using the algorithm in specific instances, rather than the theoretical question about whether in principal there is such an algorithm, then Tarski's algorithm may not actually be helpful. Although it has been implemented on computers, the algorithm takes something like a tower of exponential time in the size of the input, and evidently it has been proved that every quantifier-elimination algorithm must be at least double-exponential.

share|improve this answer
    
Thank you. My Question was motivated by developing Collision avoidance Strategies. I am interested in an algorithm Checking whether two (possibly n-dimensional) Ellipsoids overlap. Using a polynomial Representation of ellipsoids one could check if at least one real valued solution exist in order to prove a collision. For a proper performance Comparison with other algorithms (which might be based on numeric methods) I was interested in how computational complexity behaves, when the dimension of the problem grows. –  ostap bender Dec 15 '11 at 14:27
1  
I would expect that, for the specific problem of checking whether two ellipsoids overlap, there are more efficient algorithms than the relevant special case of Tarski's general algorithm. Unfortunately, this is far from my expertise, so I don't actually know any such algorithms. For conceptual purposes (if not for algorithmic ones), it might help to arrange, by an affine transformation, that one of your two ellipsoids is the unit ball. –  Andreas Blass Dec 15 '11 at 15:17
    
Yes, there are indeed more efficient Algorithms. As far as I know all of them use numerical approximation (in higher dimensions) either to calculate roots or to calculate a minimum / maximum. So I was curious whether there is an exact Algorithm, having a runtime bounded by the dimension (ideally with polynomial complexity). As far as I understood the Discussion at mathoverflow.net/questions/43979/… , there is no such algorithm yet (at least not for the more general case of counting roots of fewnomials) –  ostap bender Dec 20 '11 at 12:43

This problem is solved in so-called Semi-algebraic Geometry. Here are some books:

Basu S. Algorithms in Semi-algebraic Geometry

Basu S., Pollack R., Roy M.-F. Algorithms in Real Algebraic Geometry

Bochnak J., Coste M., Roy M-F. Real algebraic geometry

Coste M. An introduction to semialgebraic geometry

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.