We present a hybrid symbolicnumeric algorithm for
certifying a polynomial or rational function with rational coefficients
to be nonnegative for all real values of the variables by computing a
representation for it as a fraction of two polynomial sumofsquares
(SOS) with rational coefficients. Our new approach turns the earlier
methods by Peyrl and Parrilo at SNC'07 and ours at ISSAC'08 both based
on polynomial SOS, which do not always exist, into a universal algorithm
for all inputs via Artin's theorem.
Furthermore, we scrutinize the allimportant process of converting the
numerical SOS numerators and denominators produced by block semidefinite
programming into an exact rational identity. We improve on our own
Newton iterationbased high precision refinement algorithm by
compressing the initial Gram matrices and by deploying rational vector
recovery aside from orthogonal projection. We successfully demonstrate
our algorithm on 1. various exceptional SOS problems with necessary
polynomial denominators from the literature, 2. very large (thousands of
variables) SOS lower bound certificates for Rump's model problem (up to
n = 17, factor degree = 16) and 3. for proving the Monotone Column
Permanent Conjecture for dimension 4.
This is joint work with Bin Li, Zhengfeng Yang and Lihong Zhi.
