  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.
