# Software for rigorous optimization of real polynomials

I am looking for software that can find a global minimum of a polynomial function over a polyhedral domain (given by, say, some linear inequalities) in $\mathbb R^n$. The number of variables, $n$, is not more than a dozen. I know it can be done in theory (by Tarski's elimination of quantifiers in real closed fields), and I know that the time complexity is awful. However, if there is a decent implementation that can handle a dozen variables with a clean interface, it would be great. I have tried builtin implementations in Mathematica and Maple, and they do not appear terminate on 4-5 variable instances.

If the software can produce some kind of concise "certificate" of its answer, it would be even better, but I am not sure how such a certificate should look like even in theory.

Edit: Convergence to the optimum is nice, but what I am really looking for is ability to answer questions of the form "Is minimum equal to 5?" where 5 is what I believe on a priori grounds to be the answer to optimization to be (in particular, it is a rational number). That also explains why I want a certificate/proof of the inequality, or a counterexample if it is false.

I used QEPCAD once for this sort of problem, with reasonable success, although I think my problem was a bit smaller than yours.

First off, check out gloptipoly.

Also, there are general-purpose optimization packages which might work for you; they may be sufficiently fast to work even though they don't explicitly utilize the fact that the optimized function is a polynomial. Some of them require that you calculate the gradient, which in your case is easy. This a typical example; there are many such packages for R, say.

How complex are your polyhedra? Can you explicitly cover them with cubes, say? This may help you utilize those packages that only allow for simple lower and upper bounds on the variables. If you need a generic solution that may not be helpful, but if your polyhedron is fixed and relatively simple, this may be a workable approach.

I see Gloptipoly has already been mentioned. This is an implementation of the general sum-of-squares/Positivstellensatz methods which allow one to relax polynomial problems into convex optimization problems and in many cases produce certificates of optimality. Some related tools include SOSTOOLS and yalmip.

If you're interested in the theory you could search for papers by Parrilo, Lasserre, Nie, Putinar, etc. This paper by Peyrl and Parrilo in particular focuses on extracting exact (i.e. in terms of rational data) proofs of optimality, and I believe has an accompanying Macaulay2 package. Much of the general theory in this area is summarized well in the lecture notes for Parrilo's course at MIT OCW.

P.S. Can you tell from the post that Parrilo is one of my thesis advisors?

There are several methods for global optimization of general functions using interval methods and other methods. See http://www.mat.univie.ac.at/~neum/glopt.html#contents