Presburger arithmetic with threshold counting quantifiers is easy

TL;DR

This paper introduces a novel quantifier-elimination method for Presburger arithmetic extended with threshold counting quantifiers, significantly improving the decision complexity to match that of standard Presburger arithmetic.

Contribution

It develops a new quantifier-elimination procedure for extended Presburger arithmetic with counting quantifiers, reducing the decision complexity from 4ExpTime to 3ExpTime.

Findings

Decidable in 3ExpTime for the extended theory

Improved quantifier elimination for counting quantifiers

Equivalent complexity to standard Presburger arithmetic

Abstract

We give a quantifier elimination procedures for the extension of Presburger arithmetic with a unary threshold counting quantifier $\exists^{\ge c} y$ that determines whether the number of different $y$ satisfying some formula is at least $c \in \mathbb N$, where $c$ is given in binary. Using a standard quantifier elimination procedure for Presburger arithmetic, the resulting theory is easily seen to be decidable in 4ExpTime. Our main contribution is to develop a novel quantifier-elimination procedure for a more general counting quantifier that decides this theory in 3ExpTime, meaning that it is no harder to decide than standard Presburger arithmetic. As a side result, we obtain an improved quantifier elimination procedure for Presburger arithmetic with counting quantifiers as studied by Schweikardt [ACM Trans. Comput. Log., 6(3), pp. 634-671, 2005], and a 3ExpTime quantifier-elimination procedure for Presburger arithmetic extended with a generalised modulo counting quantifier.