Document Open Access Logo

An Efficient Quantifier Elimination Procedure for Presburger Arithmetic

Authors Christoph Haase , Shankara Narayanan Krishna , Khushraj Madnani , Om Swostik Mishra , Georg Zetzsche

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2024.142.pdf
  • Filesize: 0.9 MB
  • 17 pages

Document Identifiers

Author Details

Christoph Haase
  • Department of Computer Science, University of Oxford, UK
Shankara Narayanan Krishna
  • Department of Computer Science & Engineering, IIT Bombay, India
Khushraj Madnani
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Om Swostik Mishra
  • Department of Mathematics, IIT Bombay, India
Georg Zetzsche
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany

Funding

Funded by the European Union (ERC, FINABIS, 101077902). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council Executive Agency. Neither the European Union nor the granting authority can be held responsible for them.
  • Haase, Christoph: Supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 852769, ARiAT).
  • Madnani, Khushraj: Supported in part by the Deutsche Forschungsgemeinschaft (DFG) project 389792660 TRR 248--CPEC.

Acknowledgements

We are grateful to (i) Pascal Bergsträßer, Moses Ganardi, and Anthony W. Lin for discussions about Weispfenning’s lower bound, (ii) Pascal Baumann, Eren Keskin, Roland Meyer for discussions on polyhedra, (iii) Anthony W. Lin and Matthew Hague for explaining some aspects of their results on monadic decomposability, and (iv) Gaëtan Regaud for proofreading.

Cite AsGet BibTex

Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani, Om Swostik Mishra, and Georg Zetzsche. An Efficient Quantifier Elimination Procedure for Presburger Arithmetic. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 142:1-142:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ICALP.2024.142

Abstract

All known quantifier elimination procedures for Presburger arithmetic require doubly exponential time for eliminating a single block of existentially quantified variables. It has even been claimed in the literature that this upper bound is tight. We observe that this claim is incorrect and develop, as the main result of this paper, a quantifier elimination procedure eliminating a block of existentially quantified variables in singly exponential time. As corollaries, we can establish the precise complexity of numerous problems. Examples include deciding (i) monadic decomposability for existential formulas, (ii) whether an existential formula defines a well-quasi ordering or, more generally, (iii) certain formulas of Presburger arithmetic with Ramsey quantifiers. Moreover, despite the exponential blowup, our procedure shows that under mild assumptions, even NP upper bounds for decision problems about quantifier-free formulas can be transferred to existential formulas. The technical basis of our results is a kind of small model property for parametric integer programming that generalizes the seminal results by von zur Gathen and Sieveking on small integer points in convex polytopes.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • Presburger arithmetic
  • quantifier elimination
  • parametric integer programming
  • convex geometry

Metrics

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

References

  1. Parosh A. Abdulla, Karlis Čerāns, Bengt Jonsson, and Yih-Kuen Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Inform. and Comput., 160(1-2):109-127, 2000. URL: https://doi.org/10.1006/inco.1999.2843.
  2. Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, and Georg Zetzsche. Ramsey quantifiers in linear arithmetics. In Proc. POPL 2024, pages 1-32, 2024. URL: https://doi.org/10.1145/3632843.
  3. Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, and Georg Zetzsche. Ramsey quantifiers in linear arithmetics, 2023. URL: https://doi.org/10.48550/arXiv.2311.04031.
  4. Itshak Borosh and Leon B. Treybig. Bounds on positive integral solutions of linear Diophantine equations. P. Am. Math. Soc., 55:299-304, 1976. URL: https://doi.org/10.1090/S0002-9939-1976-0396605-3.
  5. W. Cook, A. M. H. Gerards, A. Schrijver, and É. Tardos. Sensitivity theorems in integer linear programming. Math. Program., 34:251-264, 1986. URL: https://doi.org/10.1007/BF01582230.
  6. D. C. Cooper. Theorem proving in arithmetic without multiplication. In Bernard Meltzer and Donald Michie, editors, Proceedings of the Seventh Annual Machine Intelligence Workshop, Edinburgh, 1971, volume 7, pages 91-99. Edinburgh University Press, 1972. Google Scholar
  7. Alain Finkel. A generalization of the procedure of Karp and Miller to well structured transition systems. In Proc. ICALP 1987, volume 267 of Lecture Notes in Computer Science, pages 499-508. Springer, 1987. URL: https://doi.org/10.1007/3-540-18088-5_43.
  8. Alain Finkel and Ekanshdeep Gupta. The well structured problem for Presburger counter machines. In Proc. FSTTCS 2019, volume 150 of LIPIcs, pages 41:1-41:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2019.41.
  9. Alain Finkel and Ekanshdeep Gupta. The well structured problem for Presburger counter machines. CoRR, abs/1910.02736, 2019. URL: https://doi.org/10.48550/arXiv.1910.02736.
  10. Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1-2):63-92, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00102-X.
  11. Michael J. Fischer and Michael O. Rabin. Super-exponential complexity of Presburger arithmetic. In Bob F. Caviness and Jeremy R. Johnson, editors, Quantifier Elimination and Cylindrical Algebraic Decomposition, pages 122-135, Vienna, 1998. Springer Vienna. URL: https://doi.org/10.1007/978-3-7091-9459-1_5.
  12. Martin Fürer. The complexity of Presburger arithmetic with bounded quantifier alternation depth. Theor. Comput. Sci., 18:105-111, 1982. URL: https://doi.org/10.1016/0304-3975(82)90115-3.
  13. Seymour Ginsburg and Edwin H Spanier. Bounded regular sets. P. Am. Math. Soc., 17(5):1043-1049, 1966. URL: https://doi.org/10.1090/S0002-9939-1966-0201310-3.
  14. Erich Grädel. Dominoes and the complexity of subclasses of logical theories. Ann. Pure Appl. Log., 43(1):1-30, 1989. URL: https://doi.org/10.1016/0168-0072(89)90023-7.
  15. Stéphane Grumbach, Philippe Rigaux, and Luc Segoufin. Spatio-temporal data handling with constraints. GeoInformatica, 5(1):95-115, 2001. URL: https://doi.org/10.1023/A:1011464022461.
  16. Florent Guépin, Christoph Haase, and James Worrell. On the existential theories of Büchi arithmetic and linear p-adic fields. In Proc. LICS 2019, pages 1-10. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785681.
  17. Christoph Haase. Subclasses of Presburger arithmetic and the weak EXP hierarchy. In Proc. CSL-LICS 2014, pages 47:1-47:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603092.
  18. Christoph Haase and Georg Zetzsche. Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests. In Proc. LICS 2019, pages 1-14. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785850.
  19. Jacques Hadamard. Rèsolution d'une question relative aux dèterminants. B. Sci. Math., 2(17):240-246, 1893. Google Scholar
  20. Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. Monadic decomposition in integer linear arithmetic. In Proc. IJCAR 2020, volume 12166 of Lecture Notes in Computer Science, pages 122-140. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51074-9_8.
  21. Gabriel Kuper, Leonid Libkin, and Jan Paredaens. Constraint Databases. Springer, 2000. Google Scholar
  22. Mohan Nair. On Chebyshev-type inequalities for primes. Am. Math. Mon., 89(2):126-129, 1982. URL: https://doi.org/10.2307/2320934.
  23. Derek C. Oppen. A 2^2^2^pn upper bound on the complexity of Presburger arithmetic. J. Comput. Syst. Sci., 16(3):323-332, 1978. URL: https://doi.org/10.1016/0022-0000(78)90021-1.
  24. Loïc Pottier. Minimal solutions of linear diophantine systems: Bounds and algorithms. In Proc. RTA 1991, volume 488 of Lecture Notes in Computer Science, pages 162-173. Springer, 1991. URL: https://doi.org/10.1007/3-540-53904-2_94.
  25. 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 congres de Mathematiciens des Pays Slaves, pages 92-101. Ksiaznica Atlas, 1929. Google Scholar
  26. C. R. Reddy and Donald W. Loveland. Presburger arithmetic with bounded quantifier alternation. In Proc. STOC 1978, pages 320-325, New York, NY, USA, 1978. ACM. URL: https://doi.org/10.1145/800133.804361.
  27. J. Barkley Rosser and Lowell Schoenfeld. Approximate formulas for some functions of prime numbers. Illinois J. Math., 6(1):64-94, 1962. URL: https://doi.org/10.1215/ijm/1255631807.
  28. Sasha Rubin. Automata presenting structures: A survey of the finite string case. Bull. Symb. Log., 14(2):169-209, 2008. URL: https://doi.org/10.2178/BSL/1208442827.
  29. Alexander Schrijver. Theory of linear and integer programming. John Wiley & Sons, 1986. Google Scholar
  30. Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, and Sergey Bereg. Monadic decomposition. J. ACM, 64(2):14:1-14:28, 2017. URL: https://doi.org/10.1145/3040488.
  31. Joachim von zur Gathen and Malte Sieveking. A bound on solutions of linear integer equalities and inequalities. Proceedings of the American Mathematical Society, 72(1):155-158, 1978. URL: https://doi.org/10.1090/S0002-9939-1978-0500555-0.
  32. Volker Weispfenning. The complexity of almost linear Diophantine problems. J. Symb. Comput., 10(5):395-403, 1990. URL: https://doi.org/10.1016/S0747-7171(08)80051-X.
  33. Volker Weispfenning. Complexity and uniformity of elimination in Presburger arithmetic. In Proc. ISSAC 1997, pages 48-53. ACM, 1997. URL: https://doi.org/10.1145/258726.258746.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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