半定规划方法判定多项式不等式中的致命退化
数值分析
2009-02-02 v1 代数几何
最优化与控制
摘要
为了验证程序或混合系统，通常需要证明某些公式是不可满足的。在本文中，我们考虑实数域上多项式不等式的合取式。判定这些合取式的经典算法不仅复杂度高，而且无法提供简单的不可满足性证明。最近，有人提出将此问题转化为半定规划问题并进行数值求解。在本文中，我们展示了这种转化通常如何产生退化问题，而数值方法在这些退化问题上往往会陷入困境。
引用
@article{arxiv.0901.4907,
title = {Fatal Degeneracy in the Semidefinite Programming Approach to the Decision of Polynomial Inequalities},
author = {David Monniaux},
journal= {arXiv preprint arXiv:0901.4907},
year = {2009}
}