The complexity of Presburger arithmetic with power or powers
share
We investigate expansions of Presburger arithmetic, i.e., the theory of the integers with addition and order, with additional structure related to exponentiation: either a function that takes a number to the power of 2, or a predicate for the powers of 2. The latter theory, denoted PresPower, was introduced by Büchi as a first attempt at characterising the sets of tuples of numbers that can be expressed using finite automata; Büchi's method does not give an elementary upper bound, and the complexity of this theory has been open. The former theory, denoted as PresExp, was shown decidable by Semenov; while the decision procedure for this theory differs radically from the automata-based method proposed by Büchi, the method is also non-elementary. And in fact, the theory with the power function has a non-elementary lower bound. In this paper, we show that while Semenov's and Büchi's approaches yield non-elementary blow-ups for PresPower, the theory is in fact decidable in triply exponential time, similar to the best known quantifier-elimination algorithm for Presburger arithmetic. We also provide a NExpTime upper bound for the existential fragment of PresExp, a step towards a finer-grained analysis of its complexity. Both these results are established by analysing a single parameterized satisfiability algorithm for PresExp, which can be specialized to either the setting of PresPower or the existential theory of PresExp. Besides the new upper bounds for the existential theory of PresExp and PresPower, we believe our algorithm provides new intuition for the decidability of these theories, and for the features that lead to non-elementary blow-ups.
READ FULL TEXT