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.

翻译：本文研究求解半定规划可行性问题（亦称线性矩阵不等式）的算法层面。由于某些半定规划实例的所有可行解均包含无理数项，基于有理数运算的数值求解器仅能获得近似解。我们探讨以下问题：能否利用与某个精确解充分接近的近似解来验证给定半定规划的可行性？现有方法通常假设存在有理可行解（并采用舍入与格基约简等算法技术）。我们提出一种无需此假设的替代方案。具体而言，我们展示了如何构建一个多项式方程组，其确保实数解集中存在孤立正确解（假设目标精确解具有最大秩）。这特别使得能够运用实代数几何中的多项式方程组求解算法，从而形成针对半定规划的混合型（或符号-数值）方法。我们通过实验将其与[Hemrion, Naldi, Safey El Din; SIAM J. Optim., 2016]中的纯符号方法进行对比；混合方法成功验证了许多该文献未能处理的半定规划实例的可行性。我们认为该方法可能具备其他应用价值，例如借助多项式方程组的数值代数几何方法对近似解进行精度提升。