Document Open Access Logo

One-Parametric Presburger Arithmetic Has Quantifier Elimination

Authors Alessio Mansutti , Mikhail R. Starchak

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.MFCS.2025.72.pdf
  • Filesize: 0.86 MB
  • 18 pages
HTML5 Logo HTML (experimental)
LIPIcs.MFCS.2025.72.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Computing methodologies → Symbolic and algebraic algorithms
  • Theory of computation → Logic
Keywords
  • decision procedures
  • quantifier elimination
  • non-linear integer arithmetic

Metrics

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

Abstract

We give a quantifier elimination procedure for one-parametric Presburger arithmetic, the extension of Presburger arithmetic with the function x ↦ t ⋅ x, where t is a fixed free variable ranging over the integers. This resolves an open problem proposed in [Bogart et al., Discrete Analysis, 2017]. As conjectured in [Goodrick, Arch. Math. Logic, 2018], quantifier elimination is obtained for the extended structure featuring all integer division functions x ↦ ⌊x/(f(t))⌋, one for each integer polynomial f. 
Our algorithm works by iteratively eliminating blocks of existential quantifiers. The elimination of a block builds on two sub-procedures, both running in non-deterministic polynomial time. The first one is an adaptation of a recently developed and efficient quantifier elimination procedure for Presburger arithmetic, modified to handle formulae with coefficients over the ring ℤ[t] of univariate polynomials. The second is reminiscent of the so-called "base t division method" used by Bogart et al. As a result, we deduce that the satisfiability problem for the existential fragment of one-parametric Presburger arithmetic (which encompasses a broad class of non-linear integer programs) is in NP, and that the smallest solution to a satisfiable formula in this fragment is of polynomial bit size.

Cite As Get BibTex

Alessio Mansutti and Mikhail R. Starchak. One-Parametric Presburger Arithmetic Has Quantifier Elimination. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 72:1-72:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.MFCS.2025.72

Author Details

Alessio Mansutti
  • IMDEA Software Institute, Madrid, Spain
Mikhail R. Starchak
  • St. Petersburg State University, Russia

Funding

  • Mansutti, Alessio: Funded by the Madrid Regional Government (César Nombela grant 2023-T1/COM-29001), and by MCIN/AEI (grant PID2022-138072OB-I00).
  • Starchak, Mikhail R.: Supported by the Russian Science Foundation, project 23-71-01041.

References

  1. Erwin H. Bareiss. Sylvester’s identity and multistep integer-preserving Gaussian elimination. Math. Comput., 1968. URL: https://doi.org/10.1090/S0025-5718-1968-0226829-0.
  2. Clark W. Barrett and Cesare Tinelli. Satisfiability modulo theories. In Handbook of Model Checking. 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_11.
  3. Michael Benedikt, Dmitry Chistikov, and Alessio Mansutti. The complexity of Presburger arithmetic with power or powers. In ICALP, 2023. URL: https://doi.org/10.4230/LIPICS.ICALP.2023.112.
  4. Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, and Georg Zetzsche. Ramsey quantifiers in linear arithmetics. In POPL, 2024. URL: https://doi.org/10.1145/3632843.
  5. Tristram Bogart, John Goodrick, Danny Nguyen, and Kevin Woods. Parametric Presburger arithmetic: complexity of counting and quantifier elimination. Math. Logic Quart., 2019. URL: https://doi.org/10.1002/malq.201800068.
  6. Tristram Bogart, John Goodrick, and Kevin Woods. Parametric Presburger arithmetic: logic, combinatorics, and quasi-polynomial behavior. Discrete Analysis, 2017. URL: https://doi.org/10.19086/da.1254.
  7. Itshak Borosh and Leon B. Treybig. Bounds on positive integral solutions of linear Diophantine equations. Proc. Am. Math. Soc., 55(2):299-304, 1976. URL: https://doi.org/10.2307/2041711.
  8. Sheng Chen, Nan Li, and Steven V. Sam. Generalized Ehrhart polynomials. Trans. Amer. Math. Soc., 2012. URL: https://doi.org/10.1090/S0002-9947-2011-05494-2.
  9. Dmitry Chistikov. An introduction to the theory of linear integer arithmetic. In FSTTCS, 2024. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2024.1.
  10. Dmitry Chistikov, Christoph Haase, and Alessio Mansutti. Quantifier elimination for counting extensions of Presburger arithmetic. In FoSSaCS, 2022. URL: https://doi.org/10.1007/978-3-030-99253-8_12.
  11. Dmitry Chistikov, Alessio Mansutti, and Mikhail R. Starchak. Integer linear-exponential programming in NP by quantifier elimination. In ICALP, 2024. (Full version of this paper: https://arxiv.org/abs/2407.07083). URL: https://doi.org/10.4230/LIPICS.ICALP.2024.132.
  12. David C. Cooper. Theorem proving in arithmetic without multiplication. Machine Intelligence, 1972. Google Scholar
  13. Felipe Cucker, Pascal Koiran, and Steve Smale. A polynomial time algorithm for diophantine equations in one variable. J. Symb. Comput., 1999. URL: https://doi.org/10.1006/jsco.1998.0242.
  14. Florian Frohn and Jürgen Giesl. Satisfiability modulo exponential integer arithmetic. In IJCAR, 2024. URL: https://doi.org/10.1007/978-3-031-63498-7_21.
  15. John Goodrick. Bounding quantification in parametric expansions of Presburger arithmetic. Arch. Math. Logic, 2018. URL: https://doi.org/10.1007/s00153-017-0593-0.
  16. Erich Grädel. Dominoes and the complexity of subclasses of logical theories. Ann. Pure Appl. Log., 1989. URL: https://doi.org/10.1016/0168-0072(89)90023-7.
  17. Eitan M. Gurari and Oscar H. Ibarra. An NP-complete number-theoretic problem. J. ACM, 26(3):567-581, 1979. URL: https://doi.org/10.1145/322139.322152.
  18. Christoph Haase. Subclasses of Presburger arithmetic and the weak EXP hierarchy. In CSL-LICS, pages 47:1-47:10, 2014. URL: https://doi.org/10.1145/2603088.2603092.
  19. Christoph Haase. A survival guide to Presburger arithmetic. ACM SIGLOG News, 2018. URL: https://doi.org/10.1145/3242953.3242964.
  20. Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani, Om Swostik Mishra, and Georg Zetzsche. An efficient quantifier elimination procedure for Presburger arithmetic. In ICALP, 2024. URL: https://doi.org/10.4230/LIPIcs.ICALP.2024.142.
  21. Peter Habermehl and Dietrich Kuske. On Presburger arithmetic extended with non-unary counting quantifiers. Log. Methods Comput. Sci., 2023. URL: https://doi.org/10.46298/lmcs-19(3:4)2023.
  22. Toghrul Karimov, Florian Luca, Joris Nieuwveld, Joël Ouaknine, and James Worrell. On the decidability of presburger arithmetic expanded with powers. In SODA, 2025. URL: https://doi.org/10.1137/1.9781611978322.89.
  23. Aless Lasaruk and Thomas Sturm. Effective quantifier elimination for Presburger arithmetic with infinity. In CASC, 2009. URL: https://doi.org/10.1007/978-3-642-04103-7_18.
  24. Kenneth L. Manders and Leonard Adleman. NP-complete decision problems for binary quadratics. Journal of Computer and System Sciences, 16(2):168-184, 1978. URL: https://doi.org/10.1016/0022-0000(78)90044-2.
  25. Derek C. Oppen. A 2^2^2^pn upper bound on the complexity of Presburger arithmetic. J. Comput. Syst. Sci., 1978. URL: https://doi.org/10.1016/0022-0000(78)90021-1.
  26. 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. 1929. Google Scholar
  27. Cattamanchi R. Reddy and Donald W. Loveland. Presburger arithmetic with bounded quantifier alternation. In STOC, 1978. URL: https://doi.org/10.1145/800133.804361.
  28. Mikhail R. Starchak. Positive existential definability with unit, addition and coprimeness. In ISSAC, 2021. URL: https://doi.org/10.1145/3452143.3465515.
  29. Joachim von zur Gathen and Malte Sieveking. A bound on solutions of linear integer equalities and inequalities. Proc. Am. Math. Soc., 1978. URL: https://doi.org/10.1090/S0002-9939-1978-0500555-0.
  30. Volker Weispfenning. The complexity of almost linear Diophantine problems. J. Symb. Comput., 1990. URL: https://doi.org/10.1016/S0747-7171(08)80051-X.
  31. Volker Weispfenning. Complexity and uniformity of elimination in Presburger arithmetic. In ISSAC, pages 48-53, 1997. URL: https://doi.org/10.1145/258726.258746.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact