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

TL;DR

This paper investigates the limitations of semidefinite programming in verifying polynomial inequalities, revealing that degeneracy often hampers numerical methods used for unsatisfiability proofs in program verification.

Contribution

The paper identifies the prevalence of degeneracy in semidefinite programming formulations for polynomial inequalities and discusses its impact on numerical resolution methods.

Findings

Degeneracy frequently occurs in SDP formulations for polynomial inequalities.

Numerical methods often struggle with degenerate problems, affecting verification reliability.

The study highlights the need for alternative approaches to handle degeneracy in this context.

Abstract

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.