  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.
