Subclasses of presburger arithmetic and the polynomial-time hierarchy

AbstractWe investigate the complexity of subclasses of Presburger arithmetic, i.e., the first-order theory of natural numbers with addition. The subclasses are defined by restricting the quantifier prefix to finite lists Q1…Qs. For allm⩾ 2 we find formula classes, defined by prefixes with m+1 alternations and m+5 quantifiers, which are Σpm- respectively Πpm-complete. For m=1, the class of ∃∀∀-formulas is shown to be NP-complete. For m=0 and for all natural numbers t, the class of ∃t-formulas is known to be in P. Thus we have a nice characterisation of the polynomial-time hierarchy by classes of Presburger formulas. Finally, the NP-completeness of the ∃∀∀-class is used to prove that for certain formulas there exist no equivalent quantifier-free formulas of polynomial length