An efficient quantifier elimination procedure for Presburger arithmetic
Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani, Om Swostik Mishra, Georg Zetzsche
TL;DR
This work proves that a block of existential quantifiers in Presburger arithmetic can be eliminated in singly exponential time by leveraging a parametric integer programming small-model property, refining the longstanding belief in doubly exponential lower bounds. It introduces bounded existential Presburger arithmetic $\exists^{\le}\mathrm{PA}$ and shows how any $\exists\mathrm{PA}$ formula can be efficiently translated to this compact form and then to an exponential-size quantifier-free formula, with constants encoded in unary. The results yield precise complexity outcomes for problems in Ramsey quantifiers, well-quasi-orderings, and monadic decomposability, establishing $\mathrm{NEXP}$- and $\mathrm{coNEXP}$-completeness bounds for existential cases. In addition, the work highlights practical implications: under mild assumptions, NP upper bounds for quantifier-free problems can transfer to existential formulas, broadening the applicability of PA quantifier-elimination in verification and formal reasoning.
Abstract
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.