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 $\mathrm{PresPower}$, was introduced by B\"uchi as a first attempt at characterising the sets of tuples of numbers that can be expressed using finite automata; B\"uchi's method does not give an elementary upper bound, and the complexity of this theory has been open. The former theory, denoted as $\mathrm{PresExp}$, was shown decidable by Semenov; while the decision procedure for this theory differs radically from the automata-based method proposed by B\"uchi, 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\"uchi's approaches yield non-elementary blow-ups for $\mathrm{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 $\mathrm{NExpTime}$ upper bound for the existential fragment of $\mathrm{PresExp}$, a step towards a finer-grained analysis of its complexity. Both these results are established by analysing a single parameterized satisfiability algorithm for $\mathrm{PresExp}$, which can be specialized to either the setting of $\mathrm{PresPower}$ or the existential theory of $\mathrm{PresExp}$. Besides the new upper bounds for the existential theory of $\mathrm{PresExp}$ and $\mathrm{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.

翻译：我们研究了Presburger算术（即带加法与次序的整数理论）在指数运算相关附加结构下的扩张：一种是取给定数的$2$次幂的函数，另一种是$2$的幂谓词。后者理论（记为$\mathrm{PresPower}$）由Büchi首次提出，旨在刻画可用有限自动机表示的数元组集合；但Büchi的方法未能给出初等上界，且该理论的复杂性至今悬而未决。前者理论（记为$\mathrm{PresExp}$）由Semenov证明为可判定的；尽管该理论的判定过程与Büchi提出的基于自动机的方法截然不同，但同样是非初等的。事实上，带幂函数理论存在非初等下界。本文表明，虽然Semenov和Büchi的方法对$\mathrm{PresPower}$均导致非初等爆炸，但该理论实际可在三指数时间内判定——这与Presburger算术最优的量词消去算法复杂度相当。此外，我们给出了$\mathrm{PresExp}$存在性片段的$\mathrm{NExpTime}$上界，这为其复杂性更精细的分析迈出了关键一步。这两个结果均通过分析$\mathrm{PresExp}$的一个参数化可满足性算法得到，该算法可分别适配至$\mathrm{PresPower}$或$\mathrm{PresExp}$存在性理论的情形。除了为$\mathrm{PresExp}$存在性理论与$\mathrm{PresPower}$提供新的上界外，我们认为该算法还为理解这些理论的可判定性以及导致非初等爆炸的特征提供了新视角。