2017/10/01 by Danny Nguyen, Igor Pak · 1 citation
Computer Science · #Numerical Methods and Algorithms #Polynomial and algebraic computation #Complexity and Algorithms in Graphs
paper · doi:10.1109/focs.2017.13
openalex publication_date 2017/10/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/29
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 ΣmP-complete or ΠmP-complete, when the first quantifier is ∃ or ∀, respectively. Counting versions and restricted systems are also analyzed.