All known quantifier elimination procedures for Presburger arithmetic require doubly exponential time for eliminating a single block of existentially quantified variables. It has even been claimed in the literature that this upper bound is tight. We observe that this claim is incorrect and develop, as the main result of this paper, a quantifier elimination procedure eliminating a block of existentially quantified variables in singly exponential time. As corollaries, we can establish the precise complexity of numerous problems. Examples include deciding (i) monadic decomposability for existential formulas, (ii) whether an existential formula defines a well-quasi ordering or, more generally, (iii) certain formulas of Presburger arithmetic with Ramsey quantifiers. Moreover, despite the exponential blowup, our procedure shows that under mild assumptions, even NP upper bounds for decision problems about quantifier-free formulas can be transferred to existential formulas. The technical basis of our results is a kind of small model property for parametric integer programming that generalizes the seminal results by von zur Gathen and Sieveking on small integer points in convex polytopes.

翻译：所有已知的普雷斯伯格算术量词消去程序在消除单个存在量化变量块时均需双指数时间。文献中甚至声称该上界是紧的。我们观察到这一论断有误，并作为本文的主要结果，开发了一种在单指数时间内消除存在量化变量块的量词消去程序。作为推论，我们可确定众多问题的精确复杂度。例如，判定(i)存在公式的单调可分解性、(ii)存在公式是否定义良拟序，或更一般地，(iii)带拉姆齐量词的普雷斯伯格算术特定公式。此外，尽管存在指数爆炸，我们的程序表明在温和假设下，关于无量词公式判定问题的NP上界也可转移至存在公式。我们结果的技术基础是一种参数整数规划的小模型性质，该性质推广了von zur Gathen与Sieveking关于凸多胞体中整数点的开创性成果。