Verifying feasibility of degenerate semidefinite programs

This paper deals with the algorithmic aspects of solving feasibility problems of semidefinite programming (SDP), aka linear matrix inequalities (LMI). Since in some SDP instances all feasible solutions have irrational entries, numerical solvers that work with rational numbers can only find an approximate solution. We study the following question: is it possible to certify feasibility of a given SDP using an approximate solution that is sufficiently close to some exact solution? Existing approaches make the assumption that there exist rational feasible solutions (and use techniques such as rounding and lattice reduction algorithms). We propose an alternative approach that does not need this assumption. More specifically, we show how to construct a system of polynomial equations whose set of real solutions is guaranteed to have an isolated correct solution (assuming that the target exact solution is maximum-rank). This allows, in particular, to use algorithms from real algebraic geometry for solving systems of polynomial equations, yielding a hybrid (or symbolic-numerical) method for SDPs. We experimentally compare it with a pure symbolic method in Henrion, Naldi, Safey El Din; SIAM J. Optim., 2016; the hybrid method was able to certify feasibility of many SDP instances on which Henrion, Naldi, Safey El Din; SIAM J. Optim., 2016 failed. We argue that our approach may have other uses, such as refining an approximate solution using methods of numerical algebraic geometry for systems of polynomial equations.