On Deciding Linear Arithmetic Constraints Over p-adic Integers for All Primes
Christoph Haase, Alessio Mansutti · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 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.