Short Presburger Arithmetic Is Hard
Danny Nguyen, Igor Pak · SIAM Journal on Computing · 2019
We study the computational complexity of short sentences in Presburger arithmetic (Short-PA). Here by “short” we mean sentences with a bounded number of variables, quantifiers, inequalities, and Boolean operations; the input consists only of the integer coefficients involved in the linear inequalities. We prove that satisfiability of Short-PA sentences with $m+2$ alternating quantifiers is $\Sigma^{\mathsf{P}}_m$-complete or $\Pi^{\mathsf{P}}_m$-complete when the first quantifier is $\exists$ or $\forall$, respectively. Counting versions and restricted systems are also analyzed. Further applications are given to hardness of two natural problems in integer optimization.