Document Open Access Logo

Constructing Small Monadic Decompositions in Presburger Arithmetic

Authors Moses Ganardi , Marin Ricros

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.47.pdf
  • Filesize: 0.86 MB
  • 22 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Monadic decomposition
  • variable independence
  • Presburger arithmetic

Metrics

Abstract

A monadic decomposition of a formula over a first-order theory is an equivalent Boolean combination of atomic formulas, each containing only one variable. Monadic decomposition is a generic simplification technique that has found applications in various settings such as quantifier elimination, string solving, and constraint databases. Previous work has mostly focused on the decision problem of whether a formula admits a monadic decomposition. However, much less is known on how to efficiently produce a small monadic decomposition, which is required for any application.
We study this question for the quantifier-free fragment of Presburger arithmetic. Here, monadic decomposability is known to be coNP-complete, and monadic decompositions can be computed in exponential time. An exponential size lower bound was only known for monadic decompositions in disjunctive or conjunctive normal form (DNF or CNF). In this work, we extend this exponential lower bound to general monadic decompositions. Guided by this lower bound, we present fragments that admit polynomially-sized monadic decompositions, which, in many cases, can be constructed efficiently. A surprising key ingredient in our proof is a family of small-depth circuits for arithmetic operations in Chinese remainder representation.

Cite As Get BibTex

Moses Ganardi and Marin Ricros. Constructing Small Monadic Decompositions in Presburger Arithmetic. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 47:1-47:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.47

Author Details

Moses Ganardi
  • University of Kaiserslautern-Landau, Kaiserslautern, Germany
Marin Ricros
  • University of Kaiserslautern-Landau, Kaiserslautern, Germany

Acknowledgements

The authors thank Dmitry Chistikov, Markus Lohrey, Philipp Werner, and Georg Zetzsche for inspiring discussions. Also, the authors thank Mikhail Starchak, Roland Guttenberg, and Om Swostik Mishra for discussions on quantifier elimination.

References

  1. Eric Allender. The division breakthroughs. Bull. EATCS, 74:61-77, 2001. Google Scholar
  2. Paul Beame, Stephen A. Cook, and H. James Hoover. Log depth circuits for division and related problems. SIAM J. Comput., 15(4):994-1003, 1986. URL: https://doi.org/10.1137/0215070.
  3. Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, and Georg Zetzsche. Ramsey quantifiers over automatic structures: Complexity and applications to verification. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 28:1-28:14. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533346.
  4. Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, and Georg Zetzsche. Ramsey quantifiers in linear arithmetics. Proc. ACM Program. Lang., 8(POPL):1-32, 2024. URL: https://doi.org/10.1145/3632843.
  5. Ashok K. Chandra, Larry J. Stockmeyer, and Uzi Vishkin. Constant depth reducibility. SIAM J. Comput., 13(2):423-439, 1984. URL: https://doi.org/10.1137/0213028.
  6. Dmitry Chistikov, Christoph Haase, and Alessio Mansutti. Quantifier elimination for counting extensions of presburger arithmetic. In Patricia Bouyer and Lutz Schröder, editors, Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, volume 13242 of Lecture Notes in Computer Science, pages 225-243. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99253-8_12.
  7. Andrew Chiu, George I. Davida, and Bruce E. Litow. Division in logspace-uniform NC^1. RAIRO Theor. Informatics Appl., 35(3):259-275, 2001. URL: https://doi.org/10.1051/ITA:2001119.
  8. Elias Rojas Collins, Chris Köcher, and Georg Zetzsche. The complexity of separability for semilinear sets and parikh automata. In Pawel Gawrychowski, Filip Mazowiecki, and Michal Skrzypczak, editors, 50th International Symposium on Mathematical Foundations of Computer Science, MFCS 2025, Warsaw, Poland, August 25-29, 2025, volume 345 of LIPIcs, pages 38:1-38:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.MFCS.2025.38.
  9. Loris D'Antoni and Margus Veanes. The power of symbolic automata and transducers. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, volume 10426 of Lecture Notes in Computer Science, pages 47-67. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63387-9_3.
  10. George I. Davida and Bruce E. Litow. Fast parallel arithmetic via modular representation. SIAM J. Comput., 20(4):756-765, 1991. URL: https://doi.org/10.1137/0220048.
  11. Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, and Martin C. Rinard. Word equations with length constraints: What’s decidable? In Armin Biere, Amir Nahir, and Tanja E. J. Vos, editors, Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers, volume 7857 of Lecture Notes in Computer Science, pages 209-226. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-39611-3_21.
  12. Seymour Ginsburg and Edwin H Spanier. Bounded regular sets. Proceedings of the American Mathematical Society, 17(5):1043-1049, 1966. Google Scholar
  13. 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.
  14. Christoph Haase. A survival guide to presburger arithmetic. ACM SIGLOG News, 5(3):67-82, 2018. URL: https://doi.org/10.1145/3242953.3242964.
  15. Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani, Om Swostik Mishra, and Georg Zetzsche. An efficient quantifier elimination procedure for presburger arithmetic. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors, 51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, Tallinn, Estonia, July 8-12, 2024, volume 297 of LIPIcs, pages 142:1-142:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.ICALP.2024.142.
  16. Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. Monadic decomposition in integer linear arithmetic. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I, 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.
  17. William Hesse, Eric Allender, and David A. Mix Barrington. Uniform constant-depth threshold circuits for division and iterated multiplication. J. Comput. Syst. Sci., 65(4):695-716, 2002. URL: https://doi.org/10.1016/S0022-0000(02)00025-9.
  18. Gabriel M. Kuper, Leonid Libkin, and Jan Paredaens, editors. Constraint Databases. Springer, 2000. URL: https://doi.org/10.1007/978-3-662-04031-7.
  19. Leonid Libkin. Variable independence for first-order definable constraints. ACM Trans. Comput. Log., 4(4):431-451, 2003. URL: https://doi.org/10.1145/937555.937557.
  20. M. Lothaire. Makanin’s Algorithm, pages 387-442. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2002. Google Scholar
  21. Oliver Markgraf, Daniel Stan, and Anthony W. Lin. Learning union of integer hypercubes with queries - (with applications to monadic decomposition). In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II, volume 12760 of Lecture Notes in Computer Science, pages 243-265. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-81688-9_12.
  22. Franco Parlamento, Alberto Policriti, and KPSB Rao. Witnessing differences without redundancies. Proceedings of the American Mathematical Society, 125(2):587-594, 1997. Google Scholar
  23. 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.
  24. Heribert Vollmer. Introduction to Circuit Complexity - A Uniform Approach. Texts in Theoretical Computer Science. An EATCS Series. Springer, 1999. URL: https://doi.org/10.1007/978-3-662-03927-4.
  25. Volker Weispfenning. Complexity and uniformity of elimination in presburger arithmetic. In Bruce W. Char, Paul S. Wang, and Wolfgang Küchlin, editors, Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation, ISSAC 1997, Maui, Hawaii, USA, July 21-23, 1997, pages 48-53. ACM, 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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact