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üchi as a first attempt at characterizing 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 $\mathrm{PresExp}$, was shown decidable by Semenov; while the decision procedure for this theory differs radically from the automata-based method proposed by Büchi, Semenov's 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 $\mathrm{PresPower}$, the theory is in fact decidable in triply exponential time, similarly 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 analyzing 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的方法同样是非初等的。事实上，带幂函数的理论具有非初等下界。本文证明：尽管Semenov和Büchi的方法均显示$\mathrm{PresPower}$存在非初等爆炸，该理论实际可在三重指数时间内判定，其复杂度与已知最优的Presburger算术消去量词算法相当。此外，我们为$\mathrm{PresExp}$的存在性片段给出$\mathrm{NExpTime}$上界，这是迈向其复杂度精细分析的一步。这两个结果均通过分析$\mathrm{PresExp}$的参数化可满足性算法得出，该算法可分别适配$\mathrm{PresPower}$场景或$\mathrm{PresExp}$存在性理论。除获得$\mathrm{PresExp}$存在性理论与$\mathrm{PresPower}$的新上界外，我们认为本算法为这些理论的可判定性以及导致非初等爆炸的特征提供了新见解。