On Deciding Linear Arithmetic Constraints Over p-adic Integers for All Primes

Authors Christoph Haase , Alessio Mansutti

Thumbnail PDF


  • Filesize: 1.08 MB
  • 20 pages

Document Identifiers

Author Details

Christoph Haase
  • Department of Computer Science, University of Oxford, UK
Alessio Mansutti
  • Department of Computer Science, University of Oxford, UK

Cite AsGet BibTex

Christoph Haase and Alessio Mansutti. On Deciding Linear Arithmetic Constraints Over p-adic Integers for All Primes. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 55:1-55:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Given an existential formula Φ of linear arithmetic over p-adic integers together with valuation constraints, we study the p-universality problem which consists of deciding whether Φ is satisfiable for all primes p, and the analogous problem for the closely related existential theory of Büchi arithmetic. Our main result is a coNEXP upper bound for both problems, together with a matching lower bound for existential Büchi arithmetic. On a technical level, our results are obtained from analysing properties of a certain class of p-automata, finite-state automata whose languages encode sets of tuples of natural numbers.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • linear arithmetic
  • Büchi arithmetic
  • p-adic numbers
  • automatic structures


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


  1. László Babai, Lance Fortnow, and Carsten Lund. Non-deterministic exponential time has two-prover interactive protocols. Comput. Complex., 1:3-40, 1991. URL: https://doi.org/10.1007/BF01200056.
  2. Achim Blumensath and Erich Grädel. Automatic structures. In Logic in Computer Science, LICS, pages 51-62. IEEE Computer Society, 2000. URL: https://doi.org/10.1109/LICS.2000.855755.
  3. Véronique Bruyère. Entiers et automates finis. Mémoire de fin d’études, 1985. Google Scholar
  4. Véronique Bruyère, Georges Hansel, Christian Michaux, and Roger Villemaire. Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc. Simon Stevin, 1(2):191-238, 1994. URL: https://doi.org/10.36045/bbms/1103408547.
  5. J. Richard Büchi. Weak second-order arithmetic and finite automata. Math. Logic Quart., 6(1‐6):66-92, 1960. URL: https://doi.org/10.1002/malq.19600060105.
  6. Dmitry Chistikov and Christoph Haase. The taming of the semi-linear set. In International Colloquium on Automata, Languages, and Programming, ICALP, volume 55 of LIPIcs, pages 128:1-128:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.128.
  7. Alan Cobham. On the base-dependence of sets of numbers recognizable by finite automata. Math. Syst. Theory, 3(2):186-192, June 1969. Google Scholar
  8. Andreas Dolzmann and Thomas Sturm. P-adic constraint solving. In International Symposium on Symbolic and Algebraic Computation, ISSAC, pages 151-158. ACM, 1999. URL: https://doi.org/10.1145/309831.309894.
  9. András Frank and Éva Tardos. An application of simultaneous Diophantine approximation in combinatorial optimization. Combinatorica, 7(1):49–65, 1987. URL: https://doi.org/10.1007/BF02579200.
  10. Erich Grädel. Dominoes and the complexity of subclasses of logical theories. Ann. Pure Appl. Log., 43(1):1-30, 1989. Google Scholar
  11. Florent Guépin, Christoph Haase, and James Worrell. On the existential theories of Büchi arithmetic and linear p-adic fields. In Logic in Computer Science, LICS, pages 1-10. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785681.
  12. Christoph Haase. Subclasses of Presburger arithmetic and the weak EXP hierarchy. In Computer Science Logic (CSL) and Logic in Computer Science (LICS), CSL-LICS, pages 47:1-47:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603092.
  13. Christoph Haase and Jakub Rózycki. On the expressiveness of Büchi arithmetic. In Foundations of Software Science and Computation Structures, FOSSACS, volume 12650 of Lect. Notes Comp. Sci., pages 310-323. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-71995-1_16.
  14. Bernard R. Hodgson. On direct products of automaton decidable theories. Theor. Comput. Sci., 19(3):331-335, 1982. URL: https://doi.org/10.1016/0304-3975(82)90042-1.
  15. Albert E. Ingham. On the Estimation of N(σ, T). Q. J. Math., os-11(1):201-202, January 1940. URL: https://doi.org/10.1093/qmath/os-11.1.201.
  16. Bakhadyr Khoussainov and Anil Nerode. Automatic presentations of structures. In Logical and Computational Complexity, LCC, volume 960 of Lect. Notes Comp. Sci., pages 367-392. Springer, 1995. URL: https://doi.org/10.1007/3-540-60178-3_93.
  17. Aless Lasaruk and Thomas Sturm. Effective quantifier elimination for Presburger arithmetic with infinity. In Computer Algebra in Scientific Computing, CASC, volume 5743 of Lect. Notes Comp. Sci., pages 195-212. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04103-7_18.
  18. Antonia Lechner, Joël Ouaknine, and James Worrell. On the complexity of linear arithmetic with divisibility. In Logic in Computer Science, LICS, pages 667-676. IEEE, 2015. URL: https://doi.org/10.1109/LICS.2015.67.
  19. Yuri V. Linnik. On the least prime in an arithmetic progression. I. The basic theorem. Rec. Math. [Mat. Sbornik] N.S., 15(57):139-178, 1944. Google Scholar
  20. L. Lipshitz. The diophantine problem for addition and divisibility. T. Am. Math. Soc., 235:271-283, 1978. URL: https://doi.org/10.2307/1998219.
  21. Markus Lohrey. Model-checking hierarchical structures. J. Comput. Syst. Sci., 78(2):461-490, 2012. URL: https://doi.org/10.1016/j.jcss.2011.05.006.
  22. Jaban Meher and M. Ram Murty. Ramanujan’s proof of Bertrand’s postulate. Am. Math. Mon., 120(7):650-653, 2013. Google Scholar
  23. Loïc Pottier. Minimal solutions of linear Diophantine systems: Bounds and algorithms. In Rewriting Techniques and Applications, RTA, volume 488 of Lect. Notes Comp. Sci., pages 162-173. Springer, 1991. URL: https://doi.org/10.1007/3-540-53904-2_94.
  24. Zdeněk Sawa. Efficient construction of semilinear representations of languages accepted by unary nondeterministic finite automata. Fundam. Informaticae, 123(1):97-106, 2013. URL: https://doi.org/10.3233/FI-2013-802.
  25. Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Trans. Comput. Theory, 8(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2858784.
  26. Aleksei L Semenov. Presburgerness of predicates regular in two number systems. Sib. Math. J., 18(2):289-300, 1977. URL: https://doi.org/10.1007/BF00967164.
  27. 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: https://doi.org/10.2307/2042554.
  28. Herbert S. Wilf. A circle-of-lights algorithm for the "money-changing problem". Am. Math. Mon., 85(7):562-565, 1978. URL: https://doi.org/10.1080/00029890.1978.11994639.
  29. Pierre Wolper and Bernard Boigelot. On the construction of automata from linear arithmetic constraints. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS, pages 1-19, 2000. URL: https://doi.org/10.1007/3-540-46419-0_1.
  30. Triantafyllos Xylouris. Über die Nullstellen der Dirichletschen L-Funktionen und die kleinste Primzahl in einer arithmetischen Progression. PhD thesis, Rheinische Friedrich-Wilhelms-Universität Bonn, 2011. URL: http://hdl.handle.net/20.500.11811/5074.