多项式不等式判定中的半定规划方法的致命退化
Fatal Degeneracy in the Semidefinite Programming Approach to the Decision of Polynomial Inequalities
AI总结：
本文揭示了将多项式不等式不可满足性判定问题转化为半定规划求解时，通常会导致数值方法难以处理的退化问题。
摘要：
为了验证程序或混合系统，通常需要证明某些公式是不可满足的。本文考虑实数域上多项式不等式的合取。经典判定算法不仅复杂度高，而且无法提供简单的不可满足性证明。最近，有人提出了将该问题归约为半定规划并进行数值求解的方法。本文展示了这种归约通常会产生退化问题，使得数值方法难以处理。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
