  Let $f, f_1, \ldots, f_\nV$ be polynomials with rational coefficients in the
indeterminates $\bfX=X_1, \ldots, X_n$ of maximum degree $D$ and $V$ be the set
of common complex solutions of $\F=(f_1,\ldots, f_\nV)$. We give an algorithm
which, up to some regularity assumptions on $\F$, computes an exact
representation of the global infimum $f^\star=\inf_{x\in V\cap\R^n} f\Par{x}$,
i.e. a univariate polynomial vanishing at $f^\star$ and an isolating interval
for $f^\star$. Furthermore, this algorithm decides whether $f^\star$ is reached
and if so, it returns $x^\star\in V\cap\R^n$ such that
$f\Par{x^\star}=f^\star$. This algorithm is probabilistic. It makes use of the
notion of polar varieties. Its complexity is essentially cubic in $\Par{\nV
D}^n$ and linear in the complexity of evaluating the input. This fits within
the best known deterministic complexity class $D^{O(n)}$. We report on some
practical experiments of a first implementation that is available as a Maple
package. It appears that it can tackle global optimization problems that were
unreachable by previous exact algorithms and can manage instances that are hard
to solve with purely numeric techniques. As far as we know, even under the
extra genericity assumptions on the input, it is the first probabilistic
algorithm that combines practical efficiency with good control of complexity
for this problem.
