Document Open Access Logo

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

Authors Christoph Haase , Alessio Mansutti

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2021.55.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

Funding

This work is part of a project that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 852769, ARiAT).

Cite As Get 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) https://doi.org/10.4230/LIPIcs.MFCS.2021.55

Abstract

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
Keywords
  • linear arithmetic
  • Büchi arithmetic
  • p-adic numbers
  • automatic structures

Metrics

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

References

  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.
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 About DROPS Imprint Privacy Contact