Fatal Degeneracy in the Semidefinite Programming Approach to the Decision of Polynomial Inequalities

In order to verify programs or hybrid systems, one often needs to prove that certain formulas are unsatisfiable. In this paper, we consider conjunctions of polynomial inequalities over the reals. Classical algorithms for deciding these not only have high complexity, but also provide no simple proof of unsatisfiability. Recently, a reduction of this problem to semidefinite programming and numerical resolution has been proposed. In this article, we show how this reduction generally produces degenerate problems on which numerical methods stumble.