短 Presburger 算术是困难的

我们研究了 Presburger 算术中短句子 (Short-PA) 的计算复杂性。这里的“短”是指具有有界数目的变量、量词、不等式和布尔运算的句子；输入仅包含线性不等式中涉及的整数系数。我们证明，当第一个量词分别为 $\exists$ 或 $\forall$ 时，具有 $m+2$ 个交替量词的 Short-PA 句子的可满足性是 $\Sigma_{P}^m$-完全的或 $\Pi_{P}^m$-完全的。还分析了计数版本和受限系统。进一步的应用给出了整数优化中两个自然问题的困难性。