pith. sign in

arxiv: 2305.03037 · v2 · pith:YJCECHJQnew · submitted 2023-05-04 · 💻 cs.LO

The complexity of Presburger arithmetic with power or powers

Michael Benedikt , Dmitry Chistikov , Alessio Mansutti This is my paper

Pith reviewed 2026-05-25 08:45 UTC · model grok-4.3

classification 💻 cs.LO
keywords Presburger arithmeticPresPowerPresExpdecidabilitycomputational complexityexponentiationquantifier eliminationsatisfiability
0
0 comments X

The pith

Presburger arithmetic with a powers-of-two predicate is decidable in triply exponential time.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that PresPower, the expansion of Presburger arithmetic by a predicate for powers of two, admits a decision procedure running in triply exponential time. Earlier methods based on automata or direct analysis of the exponentiation function produced only non-elementary bounds for both PresPower and the related PresExp theory with an actual power function. The new bound matches the best known for ordinary Presburger arithmetic. The proof rests on a single parameterized satisfiability procedure for PresExp that can be specialized to the predicate-only language of PresPower without raising the complexity class.

Core claim

The theory PresPower is decidable in triply exponential time. This bound is obtained by constructing a parameterized satisfiability algorithm for PresExp that specializes directly to PresPower while preserving the triply exponential complexity; the same algorithm also yields an NExpTime upper bound for the existential fragment of PresExp.

What carries the argument

A single parameterized satisfiability algorithm for PresExp that can be specialized to either the predicate-only language of PresPower or the existential fragment of PresExp.

If this is right

  • PresPower has an elementary decision procedure whose complexity matches the best known for plain Presburger arithmetic.
  • The existential fragment of PresExp is decidable in nondeterministic exponential time.
  • The non-elementary blow-ups in earlier automata-based or direct quantifier-elimination methods for these theories can be avoided.
  • Decidability and complexity of PresPower and PresExp can be established through a uniform parameterized reduction rather than separate automata or function-based arguments.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The parameterization technique may apply to other integer predicates while retaining elementary bounds.
  • Similar algorithms could tighten complexity results for additional expansions of Presburger arithmetic beyond powers.
  • Practical decision procedures for PresPower sentences may become viable under the new bound.
  • The approach could clarify which syntactic features of exponentiation cause non-elementary complexity in related theories.

Load-bearing premise

The parameterized satisfiability algorithm for PresExp can be specialized to the predicate-only language of PresPower while preserving the triply exponential time bound.

What would settle it

A concrete sentence in the language of PresPower whose shortest decision procedure or satisfying assignment requires more than triply exponential time in the length of the sentence, or an explicit demonstration that the specialization step exceeds the stated bound.

read the original abstract

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 characterizing 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, 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\"uchi'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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper claims that while previous approaches to PresPower and PresExp yield non-elementary complexity, a single parameterized satisfiability algorithm for PresExp can be specialized to yield a triply exponential decision procedure for PresPower and an NExpTime upper bound for the existential fragment of PresExp.

Significance. If the complexity analysis of the specialization holds, the result supplies the first elementary upper bound for PresPower (matching the best known for plain Presburger arithmetic) and a finer-grained bound for existential PresExp. The unified parameterized construction against external complexity measures is a strength and supplies new intuition about sources of non-elementarity.

major comments (1)
  1. [Section on specialization to PresPower (around the parameterized algorithm description)] The load-bearing step for the PresPower claim is the complexity analysis of the specialization from the full PresExp algorithm to the predicate-only language. The manuscript must explicitly show that the chosen parameter settings eliminate non-elementary blow-ups while preserving correctness and the triply exponential bound; this analysis is referenced in the abstract but requires a self-contained verification in the relevant section.
minor comments (2)
  1. Notation for the parameters in the algorithm could be introduced earlier and used consistently when stating the bounds for each specialization.
  2. A short table comparing the new bounds with Semenov/Büchi results would improve readability.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive evaluation of the significance of our results and for the constructive feedback. We address the single major comment point-by-point below.

read point-by-point responses

  1. Referee: [Section on specialization to PresPower (around the parameterized algorithm description)] The load-bearing step for the PresPower claim is the complexity analysis of the specialization from the full PresExp algorithm to the predicate-only language. The manuscript must explicitly show that the chosen parameter settings eliminate non-elementary blow-ups while preserving correctness and the triply exponential bound; this analysis is referenced in the abstract but requires a self-contained verification in the relevant section.

    Authors: We agree that a self-contained verification of the specialization is essential for the PresPower claim. The manuscript already describes the parameterized algorithm and notes that suitable parameter settings (bounding the exponentiation depth and eliminating function-symbol recursion) yield the 3-EXPTIME bound while inheriting correctness from the general case. However, to make the elimination of non-elementary blow-ups fully explicit and verifiable without cross-referencing the abstract, we will add a dedicated paragraph (or short subsection) that instantiates the parameters for the predicate-only language, derives the resulting recurrence for the running time, and confirms that no non-elementary tower arises. This revision will not alter any claims or proofs but will improve readability of the complexity argument. revision: yes

Circularity Check

0 steps flagged

New parameterized algorithm yields independent triply-exponential bound

full rationale

The paper introduces a single parameterized satisfiability procedure for PresExp and derives both the NExpTime bound for its existential fragment and the triply-exponential bound for PresPower by direct complexity analysis of the specialization. No step reduces a claimed result to a fitted parameter, a self-citation chain, or a definitional equivalence; the bounds are obtained from the algorithm's explicit structure measured against external complexity classes. The derivation is therefore self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The result rests on standard axioms of first-order logic and the theory of integers with addition; no new entities or fitted constants are introduced.

axioms (1)
  • standard math Standard axioms of Presburger arithmetic (integers with addition and order) plus the interpretation of the power predicate or function.
    Invoked throughout as the base theory whose expansions are studied.

pith-pipeline@v0.9.0 · 5876 in / 1238 out tokens · 22391 ms · 2026-05-25T08:45:00.496803+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

25 extracted references · 25 canonical work pages

  1. [1]

    write newline

    " write newline "" before.all 'output.state := FUNCTION fin.entry.original add.period write newline FUNCTION new.block output.state before.all = 'skip after.block 'output.state := if FUNCTION new.sentence output.state after.block = 'skip output.state before.all = 'skip after.sentence 'output.state := if if FUNCTION not #0 #1 if FUNCTION and 'skip pop #0 i...

    work page

  2. [2]

    The complexity of logical theories

    Leonard Berman. The complexity of logical theories. Theor. Comput. Sci. , 11(1):71--77, 1980

    work page 1980

  3. [3]

    A survey of arithmetic definability

    Alexis B\`es. A survey of arithmetic definability. Soc. Math. Belgique , pages 1--54, 2002

    work page 2002

  4. [4]

    o rger, Erich Gr \

    Egon B \" o rger, Erich Gr \" a del, and Yuri Gurevich. The Classical Decision Problem . Springer, 1997

    work page 1997

  5. [5]

    On extensions of Presburger arithmetic, 1986

    Gregory Cherlin and Francoise Point. On extensions of Presburger arithmetic, 1986. URL: https://webusers.imj-prg.fr/ francoise.point/papiers/cherlin_point86.pdf

    work page 1986

  6. [6]

    Geometric decision procedures and the VC dimension of linear arithmetic theories

    Dmitry Chistikov, Christoph Haase, and Alessio Mansutti. Geometric decision procedures and the VC dimension of linear arithmetic theories. In LICS , 2022

    work page 2022

  7. [7]

    Compton and C

    Kevin J. Compton and C. Ward Henson . A uniform method for proving lower bounds on the computational complexity of logical theories. APAL , 48(1):1--79, 1990

    work page 1990

  8. [8]

    On the use of non-deterministic automata for Presburger arithmetic

    Antoine Durand - Gasselin and Peter Habermehl. On the use of non-deterministic automata for Presburger arithmetic. In CONCUR , 2010

    work page 2010

  9. [9]

    A decision procedure for the first order theory of real addition with order

    Jeanne Ferrante and Charles Rackoff. A decision procedure for the first order theory of real addition with order. SIAM J. Comput. , 4(1):69--76, 1975

    work page 1975

  10. [10]

    On the existential theories of B \" u chi arithmetic and linear p -adic fields

    Florent Gu \' e pin, Christoph Haase, and James Worrell. On the existential theories of B \" u chi arithmetic and linear p -adic fields. In LICS , 2019

    work page 2019

  11. [11]

    Geometric quantifier elimination heuristics for automatically generating octagonal and max-plus invariants

    Deepak Kapur, Zhihai Zhang, Matthias Horbach, Hengjun Zhao, Qi Lu, and ThanhVu Nguyen. Geometric quantifier elimination heuristics for automatically generating octagonal and max-plus invariants. In Automated Reasoning and Mathematics - Essays in Memory of William W. McCune , volume 7788 of LNCS , pages 189--228. Springer, 2013

    work page 2013

  12. [12]

    Bounds on the automata size for Presburger arithmetic

    Felix Klaedtke. Bounds on the automata size for Presburger arithmetic. ACM Trans. Comput. Log. , 9(2):11:1--11:34, 2008

    work page 2008

  13. [13]

    On the complexity of linear arithmetic with divisibility

    Antonia Lechner, Jo \" e l Ouaknine, and James Worrell. On the complexity of linear arithmetic with divisibility. In LICS , 2015

    work page 2015

  14. [14]

    The octagon abstract domain

    Antoine Min \' e . The octagon abstract domain. High. Order Symb. Comput. , 19(1):31--100, 2006

    work page 2006

  15. [15]

    Derek C. Oppen. A 2^ 2^ 2^ pn upper bound on the complexity of P resburger arithmetic. JCSS , 16(3):323--332, 1978

    work page 1978

  16. [16]

    On decidable extensions of Presburger arithmetic: from A.\ Bertrand numeration systems to Pisot numbers

    Françoise Point. On decidable extensions of Presburger arithmetic: from A.\ Bertrand numeration systems to Pisot numbers. JSL , 65(3):1347--1374, 2000

    work page 2000

  17. [17]

    Uber die Vollst\

    Moj\. z esz Presburger. \"Uber die Vollst\"andigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt . In Comptes Rendus du I Congr\`es des Math\'ematiciens des Pays Slaves , pages 92--101. 1929

    work page 1929

  18. [18]

    NP decision procedure for monomial and linear integer constraints

    Rodrigo Raya, Jad Hamza, and Viktor Kun c ak. NP decision procedure for monomial and linear integer constraints. CoRR , 2022. https://doi.org/10.48550/arXiv.2208.02713 doi:10.48550/arXiv.2208.02713

    work page doi:10.48550/arxiv.2208.02713 2022

  19. [19]

    C. R. Reddy and D. W. Loveland. Presburger arithmetic with bounded quantifier alternation. In STOC , 1978

    work page 1978

  20. [20]

    Aleksei L. Semenov. On certain extensions of the arithmetic of addition of natural numbers. Math. USSR Izv. , 15(2):401--418, 1980

    work page 1980

  21. [21]

    Aleksei L. Semenov. Logical theories of one-place functions on the set of natural numbers. Math. USSR Izv. , 22(3):587--618, 1984

    work page 1984

  22. [22]

    The Complexity of Almost Linear Diophantine Problems

    Volker Weispfenning. The Complexity of Almost Linear Diophantine Problems . J. Symb. Comput. , 10(5):395--404, 1990

    work page 1990

  23. [23]

    write newline

    " write newline "" before.all 'output.state := FUNCTION fin.entry write newline FUNCTION new.block output.state before.all = 'skip after.block 'output.state := if FUNCTION stupid.colon after.authors 'output.state := FUNCTION insert.comma output.state before.all = 'skip between.elements 'output.state := if FUNCTION new.sentence output.state after.block = '...

    work page

  24. [24]

    , " * write output.state after.block = add.period write

    ENTRY address author booktitle chapter doi edition editor eid howpublished institution journal key month note number organization pages publisher school series title type url volume year label INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.all := #1 'mid.sentence := #2 'after.sentence := #3 '...

    work page

  25. [25]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize ":" * " " *...

    work page