2026-07-22T04:16:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24179 2025-11-12T13:34:10Z ddc:004 open_access

One-Parametric Presburger Arithmetic Has Quantifier Elimination Mansutti, Alessio Starchak, Mikhail R. decision procedures quantifier elimination non-linear integer arithmetic We give a quantifier elimination procedure for one-parametric Presburger arithmetic, the extension of Presburger arithmetic with the function x ↦ t ⋅ x, where t is a fixed free variable ranging over the integers. This resolves an open problem proposed in [Bogart et al., Discrete Analysis, 2017]. As conjectured in [Goodrick, Arch. Math. Logic, 2018], quantifier elimination is obtained for the extended structure featuring all integer division functions x ↦ ⌊x/(f(t))⌋, one for each integer polynomial f. Our algorithm works by iteratively eliminating blocks of existential quantifiers. The elimination of a block builds on two sub-procedures, both running in non-deterministic polynomial time. The first one is an adaptation of a recently developed and efficient quantifier elimination procedure for Presburger arithmetic, modified to handle formulae with coefficients over the ring ℤ[t] of univariate polynomials. The second is reminiscent of the so-called "base t division method" used by Bogart et al. As a result, we deduce that the satisfiability problem for the existential fragment of one-parametric Presburger arithmetic (which encompasses a broad class of non-linear integer programs) is in NP, and that the smallest solution to a satisfiable formula in this fragment is of polynomial bit size. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alessio Mansutti and Mikhail R. Starchak 2025 Is Part Of LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2025.72 urn:nbn:de:0030-drops-241794 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.72 eng https://creativecommons.org/licenses/by/4.0/legalcode