We investigate expansions of Presburger arithmetic (Pa), 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 2^ℕ for the powers of 2. The latter theory, denoted Pa(2^ℕ(·)), 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 Pa(λx.2^|x|), 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 Pa(2^ℕ(·)), the theory is in fact decidable in triply exponential time, similarly to the best known quantifier-elimination algorithm for Pa. We also provide a NExpTime upper bound for the existential fragment of Pa(λx.2^|x|), a step towards a finer-grained analysis of its complexity. Both these results are established by analyzing a single parameterized satisfiability algorithm for Pa(λx.2^|x|), which can be specialized to either the setting of Pa(2^ℕ(·)) or the existential theory of Pa(λx.2^|x|). Besides the new upper bounds for the existential theory of Pa(λx.2^|x|) and Pa(2^ℕ(·)), we believe our algorithm provides new intuition for the decidability of these theories, and for the features that lead to non-elementary blow-ups.
@InProceedings{benedikt_et_al:LIPIcs.ICALP.2023.112, author = {Benedikt, Michael and Chistikov, Dmitry and Mansutti, Alessio}, title = {{The Complexity of Presburger Arithmetic with Power or Powers}}, booktitle = {50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)}, pages = {112:1--112:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-278-5}, ISSN = {1868-8969}, year = {2023}, volume = {261}, editor = {Etessami, Kousha and Feige, Uriel and Puppis, Gabriele}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.112}, URN = {urn:nbn:de:0030-drops-181641}, doi = {10.4230/LIPIcs.ICALP.2023.112}, annote = {Keywords: arithmetic theories, exponentiation, decision procedures} }
Feedback for Dagstuhl Publishing