Parametric Presburger arithmetic: complexity of counting and quantifier elimination
Tristram Bogart, John Goodrick, Danny Nguyen, Kevin Woods · Mathematical logic quarterly · 2019
Abstract We consider an expansion of Presburger arithmetic which allows multiplication by k parameters . A formula in this language defines a parametric set as varies in , and we examine the counting function as a function of t. For a single parameter, it is known that can be expressed as an eventual quasi‐polynomial (there is a period m such that, for sufficiently large t, the function is polynomial on each of the residue classes mod m). We show that such a nice expression is impossible with 2 or more parameters. Indeed (assuming ) we construct a parametric set such that is not even polynomial‐time computable on input . In contrast, for parametric sets with arbitrarily many parameters, defined in a similar language without the ordering relation, we show that is always polynomial‐time computable in the size of t, and in fact can be represented using the gcd and similar functions.