Integer Linear-Exponential Programming in NP by Quantifier Elimination

Authors Dmitry Chistikov , Alessio Mansutti , Mikhail R. Starchak

Thumbnail PDF


  • Filesize: 0.9 MB
  • 20 pages

Document Identifiers

Author Details

Dmitry Chistikov
  • Centre for Discrete Mathematics and its Applications (DIMAP) & Department of Computer Science, University of Warwick, Coventry, UK
Alessio Mansutti
  • IMDEA Software Institute, Madrid, Spain
Mikhail R. Starchak
  • St. Petersburg State University, Russia

Cite AsGet BibTex

Dmitry Chistikov, Alessio Mansutti, and Mikhail R. Starchak. Integer Linear-Exponential Programming in NP by Quantifier Elimination. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 132:1-132:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


This paper provides an NP procedure that decides whether a linear-exponential system of constraints has an integer solution. Linear-exponential systems extend standard integer linear programs with exponential terms 2^x and remainder terms (x mod 2^y). Our result implies that the existential theory of the structure (ℕ,0,1,+,2^(⋅),V_2(⋅,⋅), ≤) has an NP-complete satisfiability problem, thus improving upon a recent EXPSPACE upper bound. This theory extends the existential fragment of Presburger arithmetic with the exponentiation function x ↦ 2^x and the binary predicate V_2(x,y) that is true whenever y ≥ 1 is the largest power of 2 dividing x. Our procedure for solving linear-exponential systems uses the method of quantifier elimination. As a by-product, we modify the classical Gaussian variable elimination into a non-deterministic polynomial-time procedure for integer linear programming (or: existential Presburger arithmetic).

Subject Classification

ACM Subject Classification
  • Computing methodologies → Symbolic and algebraic algorithms
  • Theory of computation → Logic
  • decision procedures
  • integer programming
  • quantifier elimination


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Erwin H. Bareiss. Sylvester’s identity and multistep integer-preserving Gaussian elimination. Math. Comput., 22:565-578, 1968. URL:
  2. Michael Benedikt, Dmitry Chistikov, and Alessio Mansutti. The complexity of Presburger arithmetic with power or powers. In ICALP, pages 112:1-112:18, 2023. URL:
  3. Itshak Borosh and Leon Bruce Treybig. Bounds on positive integral solutions of linear Diophantine equations. Proc. Am. Math. Soc., 55(2):299-304, 1976. URL:
  4. Véronique Bruyère, Georges Hansel, Christian Michaux, and Roger Villemaire. Logic and p-recognizable sets of integers. Bull. Belgian Math. Soc., 1(2):191-238, 1994. Corrigendum: Bull. Belgian Math. Soc., 1, 1994, 577. URL:
  5. J. Richard Büchi. Weak second-order arithmetic and finite automata. Math. Logic Quart., 6(1-6):66-92, 1960. URL:
  6. Gregory Cherlin and Françoise Point. On extensions of Presburger arithmetic. In 4th Easter Conference on Model Theory, volume 86 of Humboldt-Univ. Berlin Seminarberichte, pages 17-34, 1986. URL:
  7. Dmitry Chistikov, Christoph Haase, and Alessio Mansutti. Geometric decision procedures and the VC dimension of linear arithmetic theories. In LICS, pages 59:1-59:13, 2022. URL:
  8. Kevin J. Compton and C. Ward Henson. A uniform method for proving lower bounds on the computational complexity of logical theories. Ann. Pure Appl. Log., 48(1):1-79, 1990. URL:
  9. David C. Cooper. Theorem proving in arithmetic without multiplication. Machine Intelligence, 7(91-99):300, 1972. Google Scholar
  10. Charles L. Dodgson. Condensation of determinants, being a new and brief method for computing their arithmetical values. Proc. R. Soc. Lond., 15:150-155, 1867. URL:
  11. Andrei Draghici, Christoph Haase, and Florin Manea. Semënov arithmetic, affine VASS, and string constraints. In STACS, pages 29:1-29:19, 2024. URL:
  12. Florian Frohn and Jürgen Giesl. Satisfiability modulo exponential integer arithmetic, 2024. To appear in IJCAR. URL:
  13. Florent Guépin, Christoph Haase, and James Worrell. On the existential theories of Büchi arithmetic and linear p-adic fields. In LICS, pages 1-10, 2019. URL:
  14. Christoph Haase. Approaching arithmetic theories with finite-state automata. In LATA, pages 33-43, 2020. URL:
  15. Christoph Haase and Jakub Różycki. On the expressiveness of Büchi arithmetic. In FoSSaCS, pages 310-323, 2021. URL:
  16. Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. Monadic decomposition in integer linear arithmetic. In IJCAR, pages 122-140, 2020. URL:
  17. Philipp Hieronymi and Christian Schulz. A strong version of Cobham’s theorem. In STOC, pages 1-21, 2022. URL:
  18. Antoine Joux, Andrew Odlyzko, and Cécile Pierrot. The past, evolving present, and future of the discrete logarithm. In Open Problems in Mathematics and Computational Science, pages 5-36. Springer, 2014. URL:
  19. Hendrik W. Lenstra Jr. Integer programming with a fixed number of variables. Math. Oper. Res., 8(4):538-548, 1983. URL:
  20. Michael Jünger, Thomas M. Liebling, Denis Naddef, George L. Nemhauser, William R. Pulleyblank, Gerhard Reinelt, Giovanni Rinaldi, and Laurence A. Wolsey. 50 years of integer programming 1958-2008: From the early years to the state-of-the-art. Springer, 2009. Google Scholar
  21. Anna Karapiperi, Michela Redivo-Zaglia, and Maria Rosaria Russo. Generalizations of Sylvester’s determinantal identity, 2015. URL:
  22. Dexter Kozen. Lower bounds for natural proof systems. In FOCS, pages 254-266, 1977. URL:
  23. Aless Lasaruk and Thomas Sturm. Weak integer quantifier elimination beyond the linear case. In CASC, pages 275-294, 2007. URL:
  24. Leonid Libkin. Variable independence for first-order definable constraints. ACM Trans. Comput. Log., 4(4):431-451, 2003. URL:
  25. Angus Macintyre and Alex J. Wilkie. On the decidability of the real exponential field. In Piergiorgio Odifreddi, editor, Kreiseliana. About and Around Georg Kreisel, pages 441-467. A K Peters, 1996. Google Scholar
  26. Derek C. Oppen. Elementary bounds for Presburger arithmetic. In STOC, pages 34-37, 1973. URL:
  27. Christos H. Papadimitriou. On the complexity of integer programming. J. ACM, 28(4):765-768, 1981. URL:
  28. Françoise Point. On decidable extensions of Presburger arithmetic: from A. Bertrand numeration sytems to Pisot numbers. J. Symb. Log., 65(3):1347-1374, 2000. URL:
  29. Françoise Point. On the expansion (ℕ;+,2^x) of Presburger arithmetic, 2007. Preprint. URL:
  30. Mojżesz Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Comptes Rendus du I Congrès des Mathématiciens des Pays Slaves, pages 92-101. Warsaw, 1929. Google Scholar
  31. Sylvain Schmitz. Complexity hierarchies beyond Elementary. ACM Trans. Comput. Theory, 8(1):3:1-3:36, 2016. URL:
  32. Alexander Schrijver. Theory of linear and integer programming. Wiley-Interscience series in discrete mathematics and optimization. Wiley, 1999. Google Scholar
  33. Aleksei L. Semenov. On certain extensions of the arithmetic of addition of natural numbers. Math. USSR Izv., 15(2):401-418, 1980. URL:
  34. Aleksei L. Semenov. Logical theories of one-place functions on the set of natural numbers. Math. USSR Izv., 22(3):587-618, 1984. URL:
  35. Jeffrey Shallit. The Logical Approach to Automatic Sequences: Exploring Combinatorics on Words with Walnut. Cambridge University Press, 2022. URL:
  36. Larry J. Stockmeyer and Albert R. Meyer. Word problems requiring exponential time: Preliminary report. In STOC, pages 1-9, 1973. URL:
  37. Joachim von zur Gathen and Malte Sieveking. A bound on solutions of linear integer equalities and inequalities. P. Am. Math. Soc., 72(1):155-158, 1978. URL:
  38. Volker Weispfenning. The complexity of almost linear Diophantine problems. J. Symb. Comput., 10(5):395-404, 1990. URL:
  39. Volker Weispfenning. Complexity and uniformity of elimination in Presburger arithmetic. In ISSAC, pages 48-53, 1997. URL:
  40. Volker Weispfenning. Deciding linear-exponential problems. SIGSAM Bull., 34(1):30-31, 2000. URL:
  41. Hao Wu, Yu-Fang Chen, Zhilin Wu, Bican Xia, and Naijun Zhan. A decision procedure for string constraints with string-integer conversion and flat regular constraints. Acta Inform., 2023. URL: