SHORT PRESBURGER ARITHMETIC IS HARD

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(P)(m)-complete or Pi(P)(m)-complete when the first quantifier is there exists or for all, respectively. Counting versions and restricted systems are also analyzed. Further applications are given to hardness of two natural problems in integer optimization.