Short Presburger arithmetic is hard

TL;DR

This paper demonstrates that the satisfiability problem for short Presburger arithmetic sentences with bounded variables and quantifiers is computationally hard, specifically $ ext{Sigma}_P^m$-complete or $ ext{Pi}_P^m$-complete, depending on the quantifier structure.

Contribution

It establishes the precise complexity classification of short Presburger arithmetic sentences with multiple quantifier alternations, extending understanding of their computational hardness.

Findings

Satisfiability of Short-PA with $m+2$ quantifiers is $ ext{Sigma}_P^m$-complete or $ ext{Pi}_P^m$-complete.

Counting and restricted systems of Short-PA are also computationally hard.

Applications include proving hardness results in Integer Optimization problems.

Abstract

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 $\exists$ or $\forall$, respectively. Counting versions and restricted systems are also analyzed. Further application are given to hardness of two natural problems in Integer Optimizations.