Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson 4 51st
International Colloquium on Automata, Languages, and Programming (ICALP 2024)
ICALP 2024 ICALP 2024 July 8–12, 2024 Tallinn, Estonia 297 153 Department of
Computer Science, University of Oxford,
UKchristoph.haase@cs.ox.ac.ukhttps://orcid.org/0000-0002-5452-936X Department
of Computer Science & Engineering, IIT Bombay,
Indiakrishnas@cse.iitb.ac.inhttps://orcid.org/0000-0003-0925-398X Max Planck
Institute for Software Systems (MPI-SWS), Germanykmadnani@mpi-
sws.orghttps://orcid.org/0000-0003-0629-3847 Department of Mathematics, IIT
Bombay, India21b090022@iitb.ac.inhttps://orcid.org/0009-0001-6858-6605 Max
Planck Institute for Software Systems (MPI-SWS), Germanygeorg@mpi-
sws.orghttps://orcid.org/0000-0002-6421-4388 Christoph Haase, Shankara
Narayanan Krishna, Khushraj Madnani, Om Swostik Mishra, and Georg Zetzsche
<ccs2012> <concept> <concept_id>10003752.10003790</concept_id>
<concept_desc>Theory of computation Logic</concept_desc>
<concept_significance>500</concept_significance> </concept> </ccs2012>
[500]Theory of computation Logic

# An efficient quantifier elimination procedure for Presburger arithmetic

Christoph Haase  Shankara Narayanan Krishna  Khushraj Madnani  Om Swostik
Mishra  Georg Zetzsche

###### Abstract

All known quantifier elimination procedures for Presburger arithmetic require
doubly exponential time for eliminating a single block of existentially
quantified variables. It has even been claimed in the literature that this
upper bound is tight. We observe that this claim is incorrect and develop, as
the main result of this paper, a quantifier elimination procedure eliminating
a block of existentially quantified variables in singly exponential time. As
corollaries, we can establish the precise complexity of numerous problems.
Examples include deciding (i) monadic decomposability for existential
formulas, (ii) whether an existential formula defines a well-quasi ordering
or, more generally, (iii) certain formulas of Presburger arithmetic with
Ramsey quantifiers. Moreover, despite the exponential blowup, our procedure
shows that under mild assumptions, even $\NP$ upper bounds for decision
problems about quantifier-free formulas can be transferred to existential
formulas. The technical basis of our results is a kind of small model property
for parametric integer programming that generalizes the seminal results by von
zur Gathen and Sieveking on small integer points in convex polytopes.

###### keywords:

Presburger arithmetic, quantifier elimination, parametric integer programming,
convex geometry

###### category:

Track B: Automata, Logic, Semantics, and Theory of Programming

[3cm]eu-erc.pdfFunded by the European Union (ERC, FINABIS, 101077902). Views
and opinions expressed are however those of the author(s) only and do not
necessarily reflect those of the European Union or the European Research
Council Executive Agency. Neither the European Union nor the granting
authority can be held responsible for them. Christoph Haase is supported by
the European Research Council (ERC) under the European Union’s Horizon 2020
research and innovation programme (Grant agreement No. 852769, ARiAT).

###### Acknowledgements.

We are grateful to (i) Pascal Bergsträßer, Moses Ganardi, and Anthony W. Lin
for discussions about Weispfenning’s lower bound, (ii) Pascal Baumann, Eren
Keskin, Roland Meyer for discussions on polyhedra, and (iii) Anthony W. Lin
and Matthew Hague for explaining some aspects of their results on monadic
decomposability.

##  1 Introduction

Presburger arithmetic is the first-order theory of the integers with addition
and order. This theory was shown decidable by Mojżesz Presburger in 1929 [25]
by establishing a quantifier elimination procedure in the extended structure
additionally consisting of infinitely many predicates $m\mid{\cdot}$ for all
integers $m>0$, asserting divisibility by a constant. Recall that a logical
theory $T$ admits quantifier elimination whenever for any formula
$\Phi(y_{1},\ldots,y_{k})\equiv\exists x\,\varphi(x,y_{1},\ldots,y_{k})$ with
$\varphi$ being quantifier free there is a computable quantifier-free formula
$\Psi(y_{1},\ldots,y_{k})$ such that $\Phi\leftrightarrow\Psi$ is a tautology
in $T$. Presburger’s quantifier elimination procedure has non-elementary
running time. In the early 1970s, Cooper [6] developed an improved version of
Presburger’s procedure, which was later shown to run in triply exponential
time [23]. Ever since, various other quantifier elimination procedures have
been established and analyzed, especially for fragments of Presburger
arithmetic with a fixed number of quantifier alternations, see e.g. [26, 32].
Weispfenning [33] analyzed lower bounds for quantifier-elimination procedures
and showed that, assuming unary encoding of numbers, _any_ quantifier
elimination procedure requires triply exponential time. In the same paper,
Weispfenning also claims that any algorithm eliminating a single block of
existential quantifiers inherently requires _doubly_ exponential time [33, p.
50].

The main contribution of this paper is to develop a quantifier elimination
procedure for Presburger arithmetic that eliminates a block of existentially
quantified variables in _singly_ exponential time. This, of course,
contradicts Weispfenning’s claim, which actually turns out to be incorrect as
we point out in detail in Appendix C. The key technical insight underlying our
procedure is a kind of small model property for parametric integer
programming. Given an integer matrix $A\in\mathbb{Z}^{\ell\times n}$ and
$\bm{b}\in\mathbb{Z}^{\ell}$, recall that integer programming is to decide
whether there is some $\bm{x}\in\mathbb{Z}^{n}$ such that $A\bm{x}\leq\bm{b}$.
It is well-known by the work of von zur Gathen and Sieveking [31], and Borosh
and Treybig [4], that if such an $\bm{x}$ exists then there is one whose bit
length is polynomially bounded in the bit lengths of $A$ and $\bm{b}$. In this
paper, we refer to the situation in which $\bm{b}$ is not fixed and provided
as a parameter as _parametric integer programming_. Our main technical result
states that, in this setting, if $A\bm{x}\leq\bm{b}$ has a solution for a
given $\bm{b}\in\mathbb{Z}^{\ell}$ then there are
$D\in\mathbb{Q}^{n\times\ell}$ and $\bm{d}\in\mathbb{Q}^{n}$, both of bit
length polynomial in the bit length of $A$, such that $\bm{x}=D\bm{b}+\bm{d}$
is integral and also a solution. Observe that there is only an exponential
number (in the bit length of $A$) of possible choices for $D$ and $\bm{d}$.
Eliminating a block of variables $\bm{x}$ from a system of linear inequalities
thus becomes easy: we have that $A\bm{x}\leq B\bm{y}+\bm{c}$ is equivalent to
the disjunction of systems of the form $A(D(B\bm{y}+\bm{c})+\bm{d})\leq
B\bm{y}+\bm{c}$ for all $D$ and $\bm{d}$ of bit length polynomial in $A$.
Using standard arguments, this approach can then be turned into a quantifier
elimination procedure that eliminates a block of existentially quantified
variables in exponential time.

##  2 Preliminaries

Throughout this paper, all vectors $\bm{z}$ are treated as column vectors
unless mentioned otherwise. For a vector $\bm{x}\in\mathbb{Q}^{n}$, let
$\|\bm{x}\|_{\infty}$ be the maximal absolute value of all components of
$\bm{x}$. Moreover, let $\|\bm{x}\|_{\mathsf{frac}}$ be the maximal absolute
value of all _numerators_ and _denominators_ of components in $\bm{x}$. The
latter is important for representations: Note that a vector
$\bm{x}\in\mathbb{Q}^{n}$ with $\|\bm{x}\|_{\mathsf{frac}}\leq m$ can be
represented using $O(n\log m)$ bits. We use analogous notations
$\|A\|_{\infty}$ and $\|A\|_{\mathsf{frac}}$ for matrices $A$. We will
sometimes refer to the _Hadamard inequality_ [19], which implies that for a
square matrix $A\in\mathbb{Z}^{n\times n}$, we have
$|\det(A)|\leq(n\cdot\|A\|_{\infty})^{n}$. In particular, the determinant of
$A$ is at most exponential in the maximal absolute value of entries of $A$.

##### Presburger arithmetic

_Presburger arithmetic_ (PA) is the first-order theory of the structure
$\langle\mathbb{Z};+,<,0,1\rangle$. In order to enable quantifier elimination,
we have to permit modulo constraints. Thus technically, we are working with
the structure
$\langle\mathbb{Z};+,<,(\equiv_{m})_{m\in\mathbb{Z}},0,1\rangle$, where
$a\equiv_{m}b$ stands for $a\equiv b\bmod{m}$. In our syntax, we allow atomic
formulas of the forms $a_{1}x_{1}+\cdots+a_{n}x_{n}\leq b$ (called _linear
inequalities_) or $a_{1}x_{1}+\cdots+a_{n}x_{n}\equiv b\bmod{m}$ (called
_modulo_ or _divisibility constraints_), where $x_{1},\ldots,x_{n}$ are
variables and $a_{1},\ldots,a_{n},b,m\in\mathbb{Z}$ are constants encoded in
binary. A formula is _quantifier-free_ if it contains no quantifiers or,
equivalently, is a Boolean combination of atomic formulas. Notice that
conjunctions of linear inequalities can be written as systems of linear
inequalities $A\bm{x}\leq\bm{b}$.

The _size_ of a PA Formula $\varphi$, denoted $|\varphi|$, is the number of
letters used to write it down, where we assume all constants to be encoded in
binary. (Sometimes, we say that a formula obeys a size bound even if constants
are encoded in unary; but this will be stated explicitly).

##### Fixed quantifier alternation fragments

The $\Sigma_{k}$ fragment of PA consists of formulas of the form
$\exists\bm{u_{1}}\forall\bm{u_{2}}\dots
Q_{k}\bm{u_{k}}\colon\varphi(\bm{u_{1}},\bm{u_{2}},\dots,\bm{u_{k}},\bm{z})$
where $\bm{u_{i}}$ is a vector of quantified variables, $\bm{z}$ is a vector
of free variables, $\varphi(\bm{u_{1}},\bm{u_{2}},\dots,\bm{u_{k}},\bm{z})$ is
a quantifier free PA formula, and $Q_{k}$ denotes $\forall$ or $\exists$
depending on whether $k$ is even or odd respectively. Similarly, the $\Pi_{k}$
fragment of PA consists of formulas of the form
$\forall\bm{u_{1}}\exists\bm{u_{2}}\dots
Q_{k}\bm{u_{k}}\colon\varphi(\bm{u_{1}},\bm{u_{2}},\dots,\bm{u_{k}},\bm{z})$
where $Q_{k}$ denotes $\forall$ or $\exists$ depending on whether $k$ is odd
or even respectively.

##### Bounded existential Presburger arithmetic

In addition to our quantifier elimination result, we shall prove a somewhat
stronger version, which states that one can compute a compact representation
of a quantifier-free formula in polynomial time. As compact representations,
we introduce a syntactic variant of existential Presburger arithmetic, which
we call _bounded existential Presburger arithmetic_ , short
$\exists^{\leq}\mathrm{PA}$. Essentially, $\exists^{\leq}\mathrm{PA}$ requires
all quantifiers to be restricted to bounded intervals, but also permits
polynomials over the quantified variables. Using standard methods, one can
translate every formula in $\exists^{\leq}\mathrm{PA}$ in polynomial time into
an $\exists\mathrm{PA}$ formula. However, the converse is not obvious, and our
main results states that this is possible. Syntactically, an
$\exists^{\leq}\mathrm{PA}$ formula over free variables $y_{1},\ldots,y_{m}$
is of the form

$\exists^{\leq k_{1}}x_{1}\cdots\exists^{\leq k_{n}}x_{n}\colon\varphi,$

where $x_{1},\ldots,x_{n}$ are variables, each $k_{i}\in\mathbb{N}$ is a
number given in binary, and $\varphi$ is a quantifier-free formula where every
atom is of one of the forms:

$\sum_{i=1}^{m}p_{i}y_{i}\leq
q\quad\text{or}\quad\sum_{i=1}^{m}p_{i}y_{i}\equiv r\bmod{q},$ (1)

where $p_{1},\ldots,p_{m},q,r\in\mathbb{Z}[x_{1},\ldots,x_{n}]$ are
polynomials over the variables $x_{1},\ldots,x_{n}$. Thus, where
$\exists\mathrm{PA}$ allows constant integral coefficients,
$\exists^{\leq}\mathrm{PA}$ allows polynomials from
$\mathbb{Z}[x_{1},\ldots,x_{n}]$. The quantifiers $\exists^{\leq k_{i}}x_{i}$
are interpreted as “there exists $x_{i}\in\mathbb{Z}$ with $|x_{i}|\leq
k_{i}$”.

######  Remark 2.1.

Now indeed, a $\exists^{\leq}\mathrm{PA}$ formula can be converted in
polynomial time into an $\exists\mathrm{PA}$ formula: The bounded
quantification is clearly expressible in $\exists\mathrm{PA}$. The terms
$p_{i}y_{i}$ and $q$ in (1) (recall $p_{i}$ and $q$ are polynomials are from
$\mathbb{Z}[x_{1},\ldots,x_{n}]$) are also expressible, because multiplication
with exponentially bounded variables can be expressed using polynomial-size
$\exists\mathrm{PA}$ formulas. This is because given a polynomial
$p\in\mathbb{Z}[x_{1},\ldots,x_{n}]$ and a variable $y$, we can construct a
polynomial-size existential formula $\pi(x_{1},\ldots,x_{n},y,z)$ expressing
$z=p(x_{1},\ldots,x_{n})\cdot y\wedge|x_{1}|\leq
k_{1}\wedge\cdots\wedge|x_{n}|\leq k_{n}$. This, in turn, follows from the
fact that given $\ell$ in unary, we can construct an existential formula
$\mu_{\ell}(x,y,z)$, of size linear in $\ell$, expressing $z=x\cdot
y\wedge|x|\leq 2^{\ell}$ (see [17, Sec. 3.1] or [18, p. 7]). Thus, we can
construct $\pi$ in $\exists\mathrm{PA}$ by introducing a variable for each
subterm of $p$ (which can clearly all be bounded exponentially).

##### Making $\exists^{\leq}\mathrm{PA}$ formulas quantifier-free

Moreover, a $\exists^{\leq}\mathrm{PA}$ formula can easily be converted (in
exponential time) into an exponential-size quantifier-free formula: Just take
an exponential disjunction over all assignments of the existentially bounded
variables $x_{1},\ldots,x_{n}$ and replace the variables by their values in
all the atoms. Thus, $\exists^{\leq}\mathrm{PA}$ formulas can be regarded as
compact representations of quantifier-free formulas.

##  3 Main results

Here, we state and discuss implications of the main result of this paper:

######  Theorem 3.1.

Given a formula of $\exists\mathrm{PA}$, we can construct in polynomial time
an equivalent formula in $\exists^{\leq}\mathrm{PA}$.

From Theorem 3.1, we can deduce the following, since by the remark Remark 2.1
in Section 2, one can easily convert a $\exists^{\leq}\mathrm{PA}$ formula
into an exponential-sized quantifier-free formula.

######  Corollary 3.2.

Given a formula $\varphi$ in existential Presburger arithmetic, we can compute
in exponential time an equivalent quantifier-free formula $\psi$ of size
exponential in $\varphi$. Moreover, all constants in $\psi$ are encoded in
unary.

In Section 6, we will see that an exponential blowup cannot be avoided when
eliminating a block of existential quantifiers, even if we allow constants to
be encoded in binary in the quantifier-free formula.

There are several applications of Theorems 3.1 and 3.2. The most obvious type
of applications are those, where, for every problem111To be precise: Every
_semantic_ problem, meaning one that only depends on the set defined by the
input formula.  that is in $\NP$ (resp. $\coNP$) for quantifier-free formulas,
the same problem belongs to $\NEXP$ (resp. $\coNEXP$) for existential
formulas. Oftentimes, this yields optimal complexity. We mention some
examples.

A direct consequence of Corollary 3.2 (and the $\NP$ membership of the
quantifier free fragment of PA) is the following.

######  Corollary 3.3.

The $\Sigma_{2}$-fragment of Presburger arithmetic belongs to $\NEXP$.

The $\NEXP$ upper bound is known and was shown by Haase [17, Thm. 1]. In fact,
the $\Sigma_{2}$-fragment is known to be $\NEXP$-complete: An $\NEXP$ lower
bound was shown much earlier by Grädel [14], already for the
$\exists\forall^{*}$-fragment.

##### Ramsey quantifiers

In fact, combining Corollary 3.2 with the results from [2], we can strengthen
Corollary 3.3. The _Ramsey quantifier_ $\exists^{\mathsf{ram}}$ states the
existence of infinite (directed) cliques. More precisely, if
$\varphi(\bm{x},\bm{y},\bm{z})$ is a Presburger formula where $\bm{x}$ and
$\bm{y}$ are vectors of $n$ variables each, then
$\exists^{\mathsf{ram}}(\bm{x},\bm{y})\colon\varphi(\bm{x},\bm{y},\bm{z})$ is
satisfied for $\bm{z}$ if and only if there exists an infinite sequence
$\bm{a}_{1},\bm{a}_{2},\ldots\in\mathbb{Z}^{n}$ of pairwise distinct vectors
with $\varphi(\bm{a}_{i},\bm{a}_{j},\bm{z})$ for every $i<j$. As mentioned in
[2], Ramsey quantifiers can be applied to deciding liveness properties,
deciding monadic decomposability (see below), and deciding whether a formula
defines a well-quasi-ordering (see below).

In [2, Thm. 5.1], it is shown that if $\varphi(\bm{x},\bm{y},\bm{z})$ is an
$\exists\mathrm{PA}$ formula, then one can compute in polynomial time an
$\exists\mathrm{PA}$ formula $\varphi^{\prime}(\bm{z})$ equivalent to
$\exists^{\mathsf{ram}}(\bm{x},\bm{y},\bm{z})\colon\varphi(\bm{x},\bm{y},\bm{z})$.

######  Corollary 3.4.

Given a $\Sigma_{2}$-formula $\varphi(\bm{x},\bm{y},\bm{z})$, we can construct
an exponential-size $\exists\mathrm{PA}$ formula equivalent to
$\exists^{\mathsf{ram}}(\bm{x},\bm{y})\colon\varphi(\bm{x},\bm{y},\bm{z})$. In
particular, deciding the truth of
$\exists^{\mathsf{ram}}(\bm{x},\bm{y})\colon\psi$ for $\Sigma_{2}$-formulas
$\psi(\bm{x},\bm{y})$ is $\NEXP$-complete.

Indeed, Corollary 3.2 lets us convert $\varphi(\bm{x},\bm{y},\bm{z})$ into an
exponential-size existential formula $\varphi^{\prime}$, so that we can apply
the above result of [2] to the formula
$\exists^{\mathsf{ram}}(\bm{x},\bm{y})\colon\varphi^{\prime}(\bm{x},\bm{y},\bm{z})$,
which results in an equivalent exponential $\exists\mathrm{PA}$ formula. The
$\NEXP$ lower bound in the second statement follows from $\NEXP$-hardness of
the $\Sigma_{2}$-fragment and the fact that for a given $\Sigma_{2}$-formula
$\chi$ without free variables, the statement
$\exists^{\mathsf{ram}}(\bm{x},\bm{y})\colon\chi\wedge\bm{x}<\bm{y}$ is
equivalent to $\chi$.

##### Detecting WQOs

A _well-quasi-ordering_ (WQO) is a reflexive and transitive ordering
$(X,\leq)$ such that for every sequence $x_{1},x_{2},\ldots\in X$, there are
$i<j$ with $x_{i}\leq x_{j}$. Well-quasi-orderings are of paramount importance
in the widely applied theory of well-structured transition systems [7, 1, 10].
The problem of deciding whether a given Presburger formula
$\varphi(\bm{x},\bm{y})$ defines a WQO was recently raised by Finkel and Gupta
[8], with the hope of establishing automatically that certain systems are
well-structured. As observed in [9, Prop. 12], this problem reduces to
evaluating Ramsey quantifiers, which is decidable by [28]. Based on an $\NP$
algorithm for Ramsey quantifiers, it is shown in [2, Sec. 8.3] that given a
quantifier-free formula $\varphi(\bm{x},\bm{y})$, where $\bm{x}$ and $\bm{y}$
are vectors of $n$ variables each, it is $\coNP$-complete whether the relation
$R\subseteq\mathbb{Z}^{n}\times\mathbb{Z}^{n}$ defined by $\varphi$ is a WQO.
Our results allow us to settle the complexity for existential formulas:

######  Corollary 3.5.

Given an $\exists\mathrm{PA}$ formula $\varphi$, it is $\coNEXP$-complete to
decide whether $\varphi$ defines a WQO.

The upper bound follows directly from Corollary 3.2 and the fact that it is
$\coNP$-complete to decide whether a given quantifier-free formula defines a
well-quasi-ordering [2, Sec. 8.3]. This yields a $\coNEXP$ procedure overall.
It should be noted that Corollary 3.5 can also be deduced from Corollary 3.4
(using the same idea as in [2, Sec. 8.3]). However, we find it instructive to
demonstrate how quantifier elimination permits a direct transfer of the
$\coNP$ algorithm as a black box. We show the $\coNEXP$ lower bound in Section
5.

##### Monadic decomposability

A Presburger formula is _monadic_ if each of its atoms contains at most one
variable. Moreover, we say that a Presburger formula $\varphi$ is _monadically
decomposable_ if $\varphi$ is equivalent to a monadic Presburger formula.
Motivated by the role monadic formulas play in constraint databases [15, 21],
Veanes, Bjørner, and Nachmanson, and Bereg recently raised the question of how
to decide whether a given formula is monadically decomposable [30]. For
Presburger arithmetic, decidability follows from [13, p. 1048] and for
quantifier-free formulas, monadic decomposability was shown $\coNP$-complete
in [20, Thm. 1] (in [2, Cor. 8.1], the $\coNP$ upper bound is shown via Ramsey
quantifiers). Corollary 3.2 allows us to settle the case of
$\exists\mathrm{PA}$ formulas.

######  Corollary 3.6.

Monadic decomposability of $\exists\mathrm{PA}$ formulas is
$\coNEXP$-complete.

This is because given an $\exists\mathrm{PA}$ formula, we can compute an
exponential-sized quantifier-free formula and apply the existing $\coNP$
procedure, yielding a $\coNEXP$ upper bound overall. Again, the $\coNEXP$
upper bound could also be deduced from Corollary 3.4 (but this proof shows
again how to transfer algorithms using quantifier elimination). The $\coNEXP$
lower bound follows the same idea as the $\coNP$ lower bound in [2], see
Section 5.

#####  $\NP$ upper bounds

In addition to new $\NEXP$ and $\coNEXP$ upper bounds, Theorem 3.1 can also be
used to obtain $\NP$ upper bounds. Suppose we have a predicate $\mathfrak{p}$
on sets of integral vectors. That is, for each $S\subseteq\mathbb{Z}^{m}$ for
some $m\in\mathbb{N}$, either $\mathfrak{p}(S)$ is true or not. We call this
predicate _admissible_ if for any $m\in\mathbb{N}$,
$S_{1},S_{2}\subseteq\mathbb{Z}^{m}$, we have that $\mathfrak{p}(S_{1}\cup
S_{2})$ implies $\mathfrak{p}(S_{1})$ or $\mathfrak{p}(S_{2})$. Let us see
some examples:

  1. (i)

The predicate $\mathfrak{p}$ with $\mathfrak{p}(S)$ if and only if
$S\neq\emptyset$.

  2. (ii)

The predicate $\mathfrak{p}$ with $\mathfrak{p}(S)$ if and only if $S$ is
infinite.

  3. (iii)

The predicate $\mathfrak{p}$ with $\mathfrak{p}(S)$ if and only if
$S\subseteq\mathbb{Z}$ and $S$ contains a power of $2$.

  4. (iv)

The predicate $\mathfrak{p}$ with $\mathfrak{p}(S)$ if and only if
$S\subseteq\mathbb{Z}^{2k}$ and viewed as a relation
$S\subseteq\mathbb{Z}^{k}\times\mathbb{Z}^{k}$, $S$ has an infinite clique.

  5. (v)

The predicate $\mathfrak{p}$ with $\mathfrak{p}(S)$ if and only if
$S\subseteq\mathbb{Z}$ and $S$ contains infinitely many primes.

  6. (vi)

The predicate $\mathfrak{p}$ with $\mathfrak{p}(S)$ if and only if
$S\subseteq\mathbb{Z}^{2}$ and $S$ contains a pair $(x,2^{x})$.

For each such predicate, we consider the problem
$\mathfrak{p}(\exists\mathrm{PA})$:

Input

An $\exists\mathrm{PA}$ formula $\varphi$ with $m$ free variables for some
$m\in\mathbb{N}$.

Question

Does $\mathfrak{p}(S)$ hold, where $S\subseteq\mathbb{Z}^{m}$ is the set
defined by $\varphi$?

Moreover, $\mathfrak{p}(\mathrm{QF})$ is the restriction of the problem where
the input formula $\varphi$ is quantifier-free.

For several of the examples above, it is known that
$\mathfrak{p}(\exists\mathrm{PA})$ is in $\NP$: For (i) and (ii), these are
standard facts, and for (iii), this follows from $\NP$-completeness of
existential Büchi arithmetic [16, Thm. 1]. For (iv), this follows from the
fact that Ramsey quantifiers can be evaluated in $\NP$ [2, Thm 5.1]. Our
results imply that for proving $\NP$ upper bounds, we may always assume a
quantifier-free input formula. This is perhaps surprising, because one might
expect that for non-linear predicates, it is difficult to bound the quantified
variables.

######  Corollary 3.7.

For every admissible predicate $\mathfrak{p}$, the problem
$\mathfrak{p}(\exists\mathrm{PA})$ is in $\NP$ if and only if
$\mathfrak{p}(\mathrm{QF})$ is in $\NP$.

Here, the “only if” direction is trivial, and the “if” direction follows from
Theorem 3.1. This is because Theorem 3.1 allows us to assume that $\varphi$ is
given as a $\exists^{\leq}\mathrm{PA}$ formula $\exists^{\leq
k_{1}}x_{1}\cdots\exists^{\leq
k_{n}}x_{n}\colon\psi(x_{1},\ldots,x_{n},y_{1},\ldots,y_{m})$. Moreover,
admissibility of $\mathfrak{p}$ implies that $\mathfrak{p}$ is satisfied for
$\varphi$ if and only if there exists an assignment $(a_{1},\ldots,a_{n})$ for
the bounded variables such that the quantifier-free formula
$\psi(a_{1},\ldots,a_{n},y_{1},\ldots,y_{m})$ satisfies $\mathfrak{p}$. Thus,
we can guess the assignment (which occupies polynomially many bits) and run
the $\NP$ algorithm for quantifier-free formulas.

##  4 Quantifier elimination

In this section, we prove Theorem 3.1. The following is our main geometric
ingredient.

######  Proposition 4.1.

Let $A\in\mathbb{Z}^{\ell\times n}$ and $\bm{b}\in\mathbb{Z}^{\ell}$, and let
$\Delta$ be an upper bound on all absolute values of the subdeterminants of
$A$. If the system $A\bm{x}\leq\bm{b}$ has an integral solution, then it has
an integral solution of the form $D\bm{b}+\bm{d}$, where
$D\in\mathbb{Q}^{n\times\ell}$ and $\bm{d}\in\mathbb{Q}^{n}$ with
$\|D\|_{\mathsf{frac}}\leq\Delta$ and $\|\bm{d}\|_{\mathsf{frac}}\leq
n\Delta^{2}$.

Before we prove Proposition 4.1, let us see how it implies Theorem 3.1 and
Corollary 3.2.

##### Proof of Corollary 3.2

While Corollary 3.2 follows from Theorem 3.1, it follows very directly from
Proposition 4.1 and the proof is a good warm-up for the proof of Theorem 3.1.
Therefore, we first derive Corollary 3.2 from Proposition 4.1. Suppose we are
given a Presburger formula $\exists\bm{x}\colon\varphi(\bm{x},\bm{y})$, where
$\bm{x}=(x_{1},\ldots,x_{n})$ and $\bm{y}=(y_{1},\ldots,y_{m})$ are variables
and $\varphi$ is quantifier-free.

It is well-known that divisibility constraints can be eliminated in favor of
existentially quantified variables, since $a\equiv b\bmod{m}$ if and only if
$\exists x\colon a-b=mx$. Thus, we may assume that $\varphi$ contains no
divisibility constraints. Then, by moving all negations inwards and using the
standard equivalence $\neg(r\leq t)\iff t+1\leq r$, we may assume that
$\varphi$ is a positive Boolean combination of atoms
$\bm{a}^{\top}\bm{x}\leq\bm{b}^{\top}\bm{y}+c$, where
$\bm{a}\in\mathbb{Z}^{n}$, $\bm{b}\in\mathbb{Z}^{m}$, and $c\in\mathbb{Z}$.

By bringing $\varphi$ into DNF, we can write it as a disjunction of
exponentially many systems of inequalities of the form $A\bm{x}\leq
B\bm{y}+\bm{c}$, where $A\in\mathbb{Z}^{\ell\times n}$,
$B\in\mathbb{Z}^{\ell\times m}$, and $\bm{c}\in\mathbb{Z}^{\ell}$. Thus, it
suffices to construct a quantifier-free formula for $\exists\bm{x}\colon
A\bm{x}\leq B\bm{y}+\bm{c}$. Let $\Delta$ be an upper bound for all absolute
values of subdeterminants of $A$. Since the transformation into DNF does not
change the appearing constants, we have that
$\Delta\leq((m+n)\|A\|_{\infty})^{m+n}$ is at most exponential in the size of
the input formula.

According to Proposition 4.1, a vector $\bm{x}$ with $\varphi(\bm{x},\bm{y})$
exists if and only if there exists a matrix $D\in\mathbb{Q}^{n\times\ell}$ and
$\bm{d}\in\mathbb{Q}^{n}$ with $\|D\|_{\mathsf{frac}}\leq\Delta$ and
$\|\bm{d}\|_{\mathsf{frac}}\leq n\Delta^{2}$ such that (i) substituting
$D(B\bm{y}+\bm{c})+\bm{d}$ for $\bm{x}$ satisfies $A\bm{x}\leq B\bm{y}+\bm{c}$
and also (ii) the vector $D(B\bm{y}+\bm{c})+\bm{d}$ is integral. Therefore,
the formula $\exists\bm{x}\colon A\bm{x}\leq B\bm{y}+\bm{c}$ is equivalent to

$\bigvee_{(D,\bm{d})\in P}A(D(B\bm{y}+\bm{c})+\bm{d})\leq
B\bm{y}+\bm{c}\leavevmode\nobreak\ \wedge\leavevmode\nobreak\
D(B\bm{y}+\bm{c})+\bm{d}\in\mathbb{Z}^{n}$

where $P$ is the set of all pairs $(D,\bm{d})$ with
$D\in\mathbb{Q}^{n\times\ell}$, $\bm{d}\in\mathbb{Q}^{n}$,
$\|D\|_{\mathsf{frac}}\leq\Delta$, and $\|\bm{d}\|_{\mathsf{frac}}\leq
n\Delta^{2}$. Clearly, $P$ contains at most exponentially many elements.
Moreover, note that the condition $D(B\bm{y}+\bm{c})+\bm{d}\in\mathbb{Z}^{n}$
is a set of $n$ modulo constraints.

##### Proof of Theorem 3.1

The proof of Theorem 3.1 is similar to the above construction—we just need to
circumvent the exponential conversion into DNF. We proceed as follows.

As above, we are given a Presburger formula
$\exists\bm{x}\colon\varphi(\bm{x},\bm{y})$, where
$\bm{x}=(x_{1},\ldots,x_{n})$ and $\bm{y}=(y_{1},\ldots,y_{m})$ are variables
and $\varphi$ is quantifier-free. Moreover, we may assume that $\varphi$
contains no divisibility constraints and is a positive Boolean combination of
atoms $\bm{a}^{\top}\bm{x}\leq\bm{b}^{\top}\bm{y}+c$, where
$\bm{a}\in\mathbb{Z}^{n}$, $\bm{b}\in\mathbb{Z}^{m}$, and $c\in\mathbb{Z}$.

Let $\bm{a}_{i}^{\top}\bm{x}\leq\bm{b}_{i}^{\top}\bm{y}+c_{i}$ for
$i=1,\ldots,\ell$ be the set of all atoms occurring in $\varphi$ and let
$A\in\mathbb{Z}^{\ell\times n}$ be the matrix with rows $\bm{a}_{i}^{\top}$
and $B\in\mathbb{Z}^{\ell\times m}$ be the matrix of rows $\bm{b}_{i}^{\top}$,
and let $\bm{c}\in\mathbb{Z}^{\ell}$ be the (column) vector with entries
$c_{1},\ldots,c_{\ell}$. Thus, our formula $\varphi$ consists of $\ell$ atoms,
each of which is a row in the system of linear inequalities $A\bm{x}\leq
B\bm{y}+\bm{c}$. Let $\varphi^{\prime}$ be the formula obtained from $\varphi$
by replacing the atom
$\bm{a}_{i}^{\top}\bm{x}\leq\bm{b}_{i}^{\top}\bm{y}+c_{i}$ by $z_{i}=1$, where
$z_{i}$, $i\in\\{1,\ldots,\ell\\}$, is a fresh variable for each of the $\ell$
atoms. Now let $\Delta$ be an upper bound on all absolute values of the
subdeterminants of $A$. Then $\Delta\leq((m+n)\|A\|_{\infty})^{m+n}$ is at
most exponential in the size of the input formula. Consider the formula

$\exists z_{1},\ldots,z_{\ell}\in\\{0,1\\}\colon\quad\exists
D\in\mathbb{Q}^{n\times\ell},\|D\|_{\mathsf{frac}}\leq\Delta\colon\\\
\exists\bm{d}\in\mathbb{Q}^{n},\leavevmode\nobreak\
\|\bm{d}\|_{\mathsf{frac}}\leq
n\Delta^{2}\colon\quad\varphi^{\prime}\leavevmode\nobreak\
\wedge\leavevmode\nobreak\
D(B\bm{y}+\bm{c})+\bm{d}\in\mathbb{Z}^{n}\leavevmode\nobreak\
\wedge\leavevmode\nobreak\
\bigwedge_{i=1}^{\ell}\left(z_{i}=1\to\psi_{i}\right),$ (2)

where $\psi_{i}$ is the formula
$\bm{a}_{i}^{\top}(D(B\bm{y}+\bm{c})+\bm{d})\leq\bm{b}_{i}^{\top}\bm{y}+c_{i}$.
Note that (2) is expressible in $\exists^{\leq}\mathrm{PA}$: We introduce (i)
one variable for each $z_{i}$, (ii) two variables for each entry of $D$ (one
for the numerator, and one for the denominator), and (iii) two variables for
each entry of $\bm{d}$.

Each of the $n$ divisibility constraints of
$D(B\bm{y}+\bm{c})+\bm{d}\in\mathbb{Z}^{n}$ and each of the atoms $\psi_{i}$
can be written in the forms (1). To see this, let $u_{1},\ldots,u_{k}$ be the
bounded variables used for the numerators or denominators in $D$ and $\bm{d}$.
Observe that the vector $B\bm{y}$ is a linear combination of $\bm{y}$ with
integer coefficients. The matrix $D$ and the vector $\bm{d}$ consist of
quotients of bounded variables, hence rational functions in
$\mathbb{Z}[u_{1},\ldots,u_{k}]$. Thus, the vector $D(B\bm{y}+\bm{c})+\bm{d}$
has in each entry an expression $s+\sum_{i=1}^{m}r_{i}y_{i}$, where
$r_{1},\ldots,r_{m},s\in\mathbb{Z}[u_{1},\ldots,u_{k}]$. Hence, by multiplying
with the product of all denominators, we can write each inequality
$\bm{a}_{i}^{\top}(D(B\bm{y}+\bm{c})+\bm{d})\leq\bm{b}_{i}^{\top}\bm{y}+c_{i}$
in the form of (1). Moreover, for the requirement
$D(B\bm{y}+\bm{c})+\bm{d}\in\mathbb{Z}^{n}$, we can write each row of
$D(B\bm{y}+\bm{c})+\bm{d}$ as a quotient
$\tfrac{1}{q}(r+\sum_{i=1}^{m}p_{i}y_{i})$, where
$q,r,p_{1},\ldots,p_{m}\in\mathbb{Z}[u_{1},\ldots,u_{k}]$, so that membership
in $\mathbb{Z}$ is equivalent to $\sum_{i=1}^{m}p_{i}y_{i}\equiv-r\pmod{q}$.

Let us argue why (2) is equivalent to
$\exists\bm{x}\colon\varphi(\bm{x},\bm{y})$. Clearly, if (2) is satisfied,
then $\bm{z}=(z_{1},\ldots,z_{\ell})$ yields a set of atoms that, if
satisfied, makes $\varphi$ true. Moreover, the vector
$D(B\bm{y}+\bm{c})+\bm{d}$ is an integer vector that satisfies all the atoms
specified by $\bm{z}$.

Conversely, suppose $\varphi(\bm{x},\bm{y})$ holds for some
$\bm{x}\in\mathbb{Z}^{n}$ and $\bm{y}\in\mathbb{Z}^{m}$. First, we set exactly
those $z_{i}$ to $1$ for which the $i$-th atom in $\varphi$ is satisfied by
$\bm{x},\bm{y}$. Recall that each row of $A$ (and each row of $B$, and of
$\bm{c}$) corresponds to an atom in $\varphi$. Let $A^{\prime}$ be the matrix
obtained from $A$ by selecting those rows that correspond to atoms that are
satisfied by our $\bm{x}$ and $\bm{y}$. Define $B^{\prime}$ similarly from
$B$, and $\bm{c}^{\prime}$ from $\bm{c}$. Then we have $A^{\prime}\bm{x}\leq
B^{\prime}\bm{y}+\bm{c}^{\prime}$. Now Proposition 4.1 yields a matrix
$D^{\prime}$ and a vector $\bm{d}$ (each with $n$ rows) with
$A^{\prime}(D^{\prime}(B^{\prime}\bm{y}+\bm{c}^{\prime})+\bm{d})\leq
B^{\prime}\bm{y}+\bm{c}^{\prime}$. Now the set of rows of
$B^{\prime}\bm{y}+\bm{c}^{\prime}$ is a subset of the rows of
$B\bm{y}+\bm{c}$, so by inserting zero-columns into $D^{\prime}$, we can
construct a matrix $D$ with
$D(B\bm{y}+\bm{c})=D^{\prime}(B^{\prime}\bm{y}+\bm{c}^{\prime})$. Hence, we
have $A^{\prime}(D(B\bm{y}+\bm{c})+\bm{d})\leq
B^{\prime}\bm{y}+\bm{c}^{\prime}$. The latter means exactly that $\psi_{i}$ is
satisfied for every $i$ with $z_{i}=1$. Thus, this choice of
$z_{1},\ldots,z_{\ell}$, $D$, and $\bm{d}$ satisfies (2). This establishes
Theorem 3.1.

###  4.1 Constructing solutions as affine transformations

####  4.1.1 Convex geometry

Before we start with the proof of Proposition 4.1, we recall some standard
definitions from convex geometry from Schrijver’s book [29]. Below, we let
$\mathbb{R}_{+}=\\{r\in\mathbb{R}\>|\>r\geq 0\\}$. A _polyhedron_ is a set
$P=\\{\bm{x}\in\mathbb{R}^{n}\>|\>A\bm{x}\leq\bm{b}\\}$, where $A$ is an
$\ell\times n$ integer matrix and $\bm{b}\in\mathbb{Z}^{\ell}$. Let
$C\subseteq\mathbb{R}^{\ell}$, then $C$ is a _convex cone_ if
$\lambda\bm{x}+\mu\bm{y}\in C$ for all $\bm{x},\bm{y}\in C$ and
$\lambda,\mu\in\mathbb{R}_{+}$. Given a set $X\subseteq\mathbb{R}^{\ell}$,

$\operatorname{cone}(X)=\\{\lambda_{1}\bm{x}_{1}+\dots+\lambda_{t}\bm{x}_{t}\mid
t\geq 0,\leavevmode\nobreak\ \bm{x}_{1},\dots,\bm{x}_{t}\in
X,\leavevmode\nobreak\ \lambda_{1},\dots,\lambda_{t}\in\mathbb{R}_{+}\\}\,.$

The _convex hull_ of a set $X\subseteq\mathbb{R}^{\ell}$ is the smallest
convex set containing that set, i.e.,

$\operatorname{conv.hull}(X)=\\{\lambda_{1}\bm{x}_{1}+\dots+\lambda_{t}\bm{x}_{t}\mid
t\geq 1,\leavevmode\nobreak\ \bm{x}_{1},\bm{x}_{2},\dots\bm{x}_{t}\in X,\\\
\lambda_{1},\dots,\lambda_{t}\in\mathbb{R}_{+},\leavevmode\nobreak\
\lambda_{1}+\dots+\lambda_{t}=1\\}\,.$

Next, we recall some terminology concerning the structure of polyhedra. The
_characteristic cone_ of a polyhedron $P=\\{\bm{x}\mid
A\bm{x}\leq\bm{b}\\}\subseteq\mathbb{R}^{n}$ is the set
$\operatorname{char.cone}(P)\coloneqq\\{\bm{y}\in\mathbb{R}^{n}\mid
A\bm{y}\leq 0\\}$. The _lineality space_ of polyhedron $P$ is the set
$\operatorname{lin.space}(P)\coloneqq\\{\bm{y}\in\mathbb{R}^{n}\mid
A\bm{y}=0\\}$.

######  Definition 4.2 (Faces).

Given a polyhedron $P\subseteq\mathbb{R}^{n}$, $F\subseteq P$ is a _face_ of
$P$ if and only if $F$ is non-empty and

$F=\\{\bm{x}\in P\>|\>A^{\prime}\bm{x}=\bm{b}^{\prime}\\}$

for some subsystem $A^{\prime}\bm{x}\leq\bm{b}^{\prime}$ of
$A\bm{x}\leq\bm{b}$. We call $F\subseteq P$ a _proper face_ of $P$ if
$F\neq\emptyset$ and $F\neq P$.

It follows that $P$ has only finitely many faces. A _minimal face_ of $P$ is a
face not containing any other face. We have the following characterization of
minimal faces [29, Thm 8.4],

######  Proposition 4.3.

A set $F$ is a minimal face of a polyhedron $P\subseteq\mathbb{R}^{n}$ if and
only if $\emptyset\neq F\subseteq P$ and

$F=\\{\bm{x}\in\mathbb{R}^{n}\>|\>A^{\prime}\bm{x}=\bm{b}^{\prime}\\}$

for some subsystem $A^{\prime}\bm{x}\leq\bm{b}^{\prime}$ of
$A\bm{x}\leq\bm{b}$, such that the matrix $A^{\prime}$ has the same rank as
$A$.

The following is shown in [29, Sec. 8.8]:

######  Proposition 4.4.

Let $C$ be the cone $\\{\bm{x}\in\mathbb{R}^{n}\>|\>A\bm{x}\leq\bm{0}\\}$.
There is a finite collection $G_{1},G_{2}.\dots,G_{s}$ of subsets, which are
of the form $G_{i}=\\{\bm{x}\in\mathbb{R}^{n}\mid\bm{a}_{i}^{\top}\bm{x}\leq
0,\leavevmode\nobreak\ A^{\prime}\bm{x}=\bm{0}\\}$, where
$\begin{bmatrix}A^{\prime}\\\ \bm{a}_{i}^{\top}\end{bmatrix}$ is a subset of
the rows of $A$, such that the following holds. If we choose for each
$i=1,\ldots,s$ a vector $\bm{y}_{i}$ from
$G_{i}\setminus\operatorname{lin.space}(C)$ and choose
$\bm{z}_{0},\ldots,\bm{z}_{t}$ in $\operatorname{lin.space}(C)$ such that
$\operatorname{lin.space}(C)=\operatorname{cone}(\bm{z}_{0},\ldots,\bm{z}_{t})$,
then

$C=\operatorname{cone}(\bm{y}_{1},\ldots,\bm{y}_{s},\bm{z}_{0},\ldots,\bm{z}_{t}).$

Here, the sets $G_{i}$ are also called minimal proper faces (but Proposition
4.4 is not a characterization of those).

####  4.1.2 Proof of Proposition 4.1

We now prove Proposition 4.1. For the remainder of the section, let
$A\in\mathbb{Z}^{\ell\times n}$ and $\bm{b}\in\mathbb{Z}^{\ell}$. Moreover,
let $\Delta$ be an upper bound on all absolute values of the sub-determinants
of $A$. Our first step is a simple application of standard facts about
polyhedra.

######  Lemma 4.5.

If the system $A\bm{x}\leq\bm{b}$ has a solution in $\mathbb{Q}^{n}$, then it
has one of the form $\frac{1}{a}E\bm{b}$, where
$E\in\mathbb{Z}^{n\times\ell}$, $a\in\mathbb{Z}\setminus\\{0\\}$,
$|a|\leq\Delta$, and $\|E\|_{\infty}\leq\Delta$.

######  Proof 4.6.

It is well-known that if $A\bm{x}\leq\bm{b}$ has a rational solution, then
there is a solution inside a minimal face of the polyhedron
$P=\\{\bm{x}\in\mathbb{R}^{n}\mid A\bm{x}\leq\bm{b}\\}$ defined by the system
of linear inequalities $A\bm{x}\leq\bm{b}$ [29, Thm. 8.5]. Recall that a
_minimal face_ is a non-empty subset $F\subseteq P$ of the form

$F=\\{\bm{x}\in\mathbb{R}^{n}\mid A^{\prime}\bm{x}=\bm{b}^{\prime}\\},$ (3)

where $A^{\prime}\bm{x}\leq\bm{b}^{\prime}$ is a subset of the inequalities in
$A\bm{x}\leq\bm{b}$ such that the matrix $A^{\prime}$ has the same rank as $A$
(see Proposition 4.3 or [29, Thm. 8.4]). Suppose $F$ is a non-empty minimal
face and satisfies (3). Here, we may assume that the rows of $A^{\prime}$ are
linearly independent (otherwise, we can remove redundant rows without changing
$F$). This means, $A^{\prime}$ can be written as $A^{\prime}=(B\quad C)$ such
that $B$ is invertible. Then the vector
$\bm{x}^{*}:=(B^{-1}\bm{b}^{\prime}\quad\bm{0})^{\top}$ belongs to $F$. Since
$F\subseteq P$, we know that $A\bm{x}^{*}\leq\bm{b}$. By Cramer’s rule, the
entry $(j,i)$ of $B^{-1}$ is $\tfrac{(-1)^{i+j}\det(B_{ij})}{\det(B)}$, where
$B_{ij}$ is the matrix obtained from $B$ by removing the $i$-th row and $j$-th
column. Note that $|\det(B_{ij})|\leq\Delta$ and $|\det(B)|\leq\Delta$. In
particular, $\bm{x}^{*}$ can be written as $\tfrac{1}{a}E\bm{b}$, where
$a=\det(B)$ and $\|E\|_{\infty}\leq\Delta$.

We also employ the following well-known fact, which again uses standard
arguments.

######  Lemma 4.7.

There are integral vectors $\bm{y}_{1},\ldots,\bm{y}_{s}$ with each component
being at most $\Delta$ in absolute value, such that
$\\{\bm{x}\in\mathbb{R}^{n}\mid
A\bm{x}\leq\bm{0}\\}=\operatorname{cone}(\bm{y}_{1},\ldots,\bm{y}_{s})$.

######  Proof 4.8.

Let $C=\\{\bm{x}\in\mathbb{R}^{n}\mid A\bm{x}\leq\bm{0}\\}$. The Lemma follows
from Proposition 4.4. First, it is a consequence of Cramer’s rule that we can
choose $\bm{z}_{0},\ldots,\bm{z}_{t}$ as a basis of
$\operatorname{lin.space}(C)=\\{\bm{x}\in\mathbb{R}^{n}\mid A\bm{x}=\bm{0}\\}$
so that all $\bm{z}_{0},\ldots,\bm{z}_{t}$ are integral and have absolute
values at most $\Delta$ in all components. For example, see [29, Cor. 3.1c].
It remains to pick from each set

$G_{i}\setminus\operatorname{lin.space}(C)=\\{\bm{x}\in\mathbb{R}^{n}\mid\bm{a}_{i}^{\top}\bm{x}<0,\leavevmode\nobreak\
A^{\prime}\bm{x}=\bm{0}\\}$

an integral vector with all components bounded by $\Delta$. For this, we can
proceed similarly to Lemma 4.5. As a subset of rows of $A$, the matrix
$B=\begin{bmatrix}A^{\prime}\\\ \bm{a}_{i}^{\top}\end{bmatrix}$ has rank at
most $n$, and we may assume $\bm{a}_{i}\neq\bm{0}$ (otherwise
$G_{i}\setminus\operatorname{lin.space}(C)$ would be empty). Moreover, we may
assume that the rows of $B$ are linearly independent, as otherwise we can
remove rows from $A^{\prime}$ without changing $G_{i}$. We can thus write
$B=(E\quad F)$, where $E$ is invertible. By Cramer’s rule (see, e.g. [29, Sec.
3.2]), the $j$-th component of the vector $\bm{y}=E^{-1}(0,\ldots,0,-1)$ can
be written as $\frac{1}{\det(E)}\det(\tilde{E})$, where $\tilde{E}$ is
obtained from $E$ by replacing the $j$-th column by $(0,\ldots,0,-1)$. This
means, the vector $|\det(E)|\cdot\bm{y}$ has only integer components and all
of them have absolute value at most $\Delta$. Now let $\bm{y}^{*}$ be the
vector obtained from $|\det(E)|\cdot\bm{y}$ adding as many $0$’s as $F$ has
columns. Then we have
$B\bm{y}^{*}=E(|\det(E)|\cdot\bm{y})=(0,\ldots,0,-|\det(E)|)$ and thus
$\bm{y}^{*}\in G_{i}\setminus\operatorname{lin.space}(C)$.

We also rely on the well-known theorem of Carathéodory [29, Cor. 7.1(i)].

######  Theorem 4.9 (Carathéodory’s theorem).

If $X\subseteq\mathbb{R}^{n}$ is some subset and
$\bm{x}\in\operatorname{cone}(X)$, then there are linearly independent
$\bm{x}_{1},\ldots,\bm{x}_{m}\in X$ with
$\bm{x}\in\operatorname{cone}(\bm{x}_{1},\ldots,\bm{x}_{m})$.

The following lemma is the key ingredient for proving Proposition 4.1. Its
proof closely follows the ideas of [29, Thm. 17.2], which Schrijver attributes
to Cook, Gerards, Schrijver, and Tardos [5]. The latter shows that for every
rational $\bm{x}$ that maximizes an expression $\bm{c}^{\top}\bm{x}$ among the
solutions of $A\bm{x}\leq\bm{b}$, there is a close-by integral vector that
maximizes this expression among all integral vectors.

######  Lemma 4.10.

Suppose the system $A\bm{x}\leq\bm{b}$ has an integral solution, and let
$\bm{r}\in\mathbb{Q}^{n}$ be a rational solution. Then there is an integral
solution $\bm{z}^{*}\in\mathbb{Z}^{n}$ with
$\|\bm{z}^{*}-\bm{r}\|_{\infty}\leq n\Delta$.

######  Proof 4.11.

An illustration of the proof is given in Figure 1. Let $\bm{z}$ be an integral
solution to $A\bm{x}\leq\bm{b}$. Split the equations $A\bm{x}\leq\bm{b}$ into
$A_{1}\bm{x}\leq\bm{b}_{1}$ and $A_{2}\bm{x}\leq\bm{b}_{2}$ such that
$A_{1}\bm{r}\leq A_{1}\bm{z}$ and $A_{2}\bm{r}\geq A_{2}\bm{z}$. In other
words, we split $A$, $\bm{b}$ into two sets of rows, depending on in which
coordinates $\bm{r}$ resp. $\bm{z}$ is larger. Now consider the cone
$C=\\{\bm{x}\in\mathbb{R}^{n}\>\mid\>A_{1}\bm{x}\geq\bm{0},\leavevmode\nobreak\
A_{2}\bm{x}\leq\bm{0}\\}$. Then, by the choice of $A_{1}$ and $A_{2}$, we have
$\bm{z}-\bm{r}\in C$ and therefore

$\bm{z}-\bm{r}=\lambda_{1}\bm{y}_{1}+\cdots+\lambda_{t}\bm{y}_{t},$

where $\lambda_{1},\ldots,\lambda_{t}\geq 0$ are real numbers and
$\bm{y}_{1},\ldots,\bm{y}_{t}$ are some linearly independent vectors chosen
from the set of integer vectors $\\{\bm{y}_{1},\ldots,\bm{y}_{s}\\}$ provided
by Lemma 4.7 satisfying
$C=\operatorname{cone}(\bm{y}_{1},\ldots,\bm{y}_{s}\\}$. The choice of
linearly independent vectors is possible due to Carathéodory’s theorem. In
particular, each $\bm{y}_{i}$ has maximal absolute value at most $\Delta$ and
we have $t\leq n$.

Observe that for any $\mu_{1},\ldots,\mu_{t}$ with
$0\leq\mu_{i}\leq\lambda_{i}$ for $i\in[1,t]$, the vector

$\bm{r}+\mu_{1}\bm{y}_{1}+\cdots+\mu_{t}\bm{y}_{t}$

is still a solution to $A\bm{x}\leq\bm{b}$. Indeed,
$A_{1}\bm{y}_{i}\geq\bm{0}$ and $A_{2}\bm{y}_{i}\leq\bm{0}$ implies

$\displaystyle A_{1}(\bm{r}+\mu_{1}\bm{y}_{1}+\cdots+\mu_{t}\bm{y}_{t})$
$\displaystyle\leq A_{1}\bm{z}\leq\bm{b}_{1},\leavevmode\nobreak\ \text{and}$
$\displaystyle A_{2}(\bm{r}+\mu_{1}\bm{y}_{1}+\cdots+\mu_{t}\bm{y}_{t})$
$\displaystyle\leq A_{2}\bm{r}\leq\bm{b}_{2},$

and thus $A(\bm{r}+\mu_{1}\bm{y}_{1}+\cdots+\mu_{t}\bm{y}_{t})\leq\bm{b}$. In
particular, the vector

$\bm{z}^{*}=\bm{r}+(\lambda_{1}-\lfloor\lambda_{1}\rfloor)\bm{y}_{1}+\cdots+(\lambda_{t}-\lfloor\lambda_{t}\rfloor)\bm{y}_{t}$

is a solution to $A\bm{x}\leq\bm{b}$. Moreover, $\bm{z}^{*}$ is obtained from
$\bm{z}$ by subtracting integer multiples of the integer vectors
$\bm{y}_{1},\ldots,\bm{y}_{t}$, and thus $\bm{z}^{*}$ is integral as well.
Finally, we have

$\|\bm{z}^{*}-\bm{r}\|_{\infty}=\|(\lambda_{1}-\lfloor\lambda_{1}\rfloor)\bm{y}_{1}+\cdots+(\lambda_{t}-\lfloor\lambda_{t}\rfloor)\bm{y}_{t}\|_{\infty}\leq\sum_{i=1}^{t}\|\bm{y}_{i}\|_{\infty}\leq
n\Delta.$

$(0,0)$$\bm{y}_{1}$$\bm{y}_{2}=\bm{y}_{t}$$\bm{y}_{3}$$\bm{y}_{s-1}$$\bm{y}_{s}$$\bm{z}-\bm{r}$$\bm{z}$$\bm{r}$$\bm{y}_{1}^{\prime}$$\bm{y}_{2}^{\prime}$$\bm{z}^{*}$$\bm{z}-\bm{r}=\lambda_{1}\bm{y}_{1}+\lambda_{2}\bm{y}_{2}$$\bm{z}^{*}-r{=}\\{\lambda_{1}\\}\bm{y}_{1}{+}\\{\lambda_{2}\\}\bm{y}_{2}$

Figure 1: The main idea behind Lemma 4.10. The region enclosed by blue lines
depicts the solution space of the given system of linear inequalities. As
mentioned in the lemma, $\bm{r}$ and $\bm{z}$ are respectively the given
rational and integral solutions. Due to Lemma 4.7, we know that $C$
(containing $\bm{z}-\bm{r}$) can be obtained as a cone of integer vectors
$\bm{y}_{1},\ldots\bm{y}_{s}$. Moreover, by Carathéodory’s theorem, we know
that there are $t$ linearly independent ($t=2$ in this case) vectors whose
cone contains $\bm{z}-\bm{r}$. Intuitively, these vectors
($\bm{y}_{1},\bm{y}_{2}$) form a coordinate system for searching the required
$z^{*}$. For $i\in\\{1,2\\}$, $\bm{y}_{i}^{\prime}=\bm{y}_{i}+\bm{r}$,
$\\{\lambda_{i}\\}=\lambda_{i}-\lfloor\lambda_{i}\rfloor$.

######  Proof 4.12 (Proof of Proposition 4.1).

According to Lemma 4.5, there is a rational solution $\tfrac{1}{a}E\bm{b}$ to
$A\bm{x}\leq\bm{b}$, where $E\in\mathbb{Z}^{n\times\ell}$,
$a\in\mathbb{Z}\setminus\\{0\\}$, $|a|\leq\Delta$, and
$\|E\|_{\infty}\leq\Delta$. We set $D:=\tfrac{1}{a}E$. Now since
$A\bm{x}\leq\bm{b}$ has an integral solution, Lemma 4.10 yields an integral
solution $\bm{z}^{*}$ close to $D\bm{b}$, meaning
$\|\bm{z}^{*}-D\bm{b}\|_{\infty}\leq n\Delta$. We set
$\bm{d}:=\bm{z}^{*}-D\bm{b}$. Then of course $D\bm{b}+\bm{d}=\bm{z}^{*}$ is an
integral solution to $A\bm{x}\leq\bm{b}$. Moreover, we clearly have
$\|\bm{d}\|_{\infty}\leq n\Delta$. It remains to show that even
$\|\bm{d}\|_{\mathsf{frac}}\leq n\Delta^{2}$. Indeed, since $\bm{z}^{*}$ is
integral, $\bm{b}$ is integral, and $D=\tfrac{1}{a}E$ with integral $E$, we
know that in $\bm{d}=\bm{z}^{*}-D\bm{b}$, every entry can be written with $a$
as its denominator. As this fraction has absolute value at most $n\Delta$ and
$|a|\leq\Delta$, both numerator and denominator have absolute value at most
$n\Delta^{2}$.

##  5 Matching complexity lower bounds

In this section we prove the lower bounds for Corollaries 3.5 and 3.6.

##### Detecting WQOs

We begin with the lower bound for Corollary 3.5. That is, we show that
deciding whether an existential Presburger formula defines a WQO is $\coNEXP$
hard. The idea is essentially the same as the $\coNP$ lower bound for
detecting WQOs for quantifier-free formulas in [3, Sec. 8]. The proof follows
from reducing the satisfiability problem for $\Pi_{2}$ sentences to WQO-
definability of existential Presburger formulas. Given an instance $\gamma$ of
a $\Pi_{2}$ sentence, we synthesize an existential Presburger formula
$\varphi$ and show that $\varphi$ defines a WQO iff $\gamma$ is satisfiable.
The $\coNEXP$-completeness of $\Pi_{2}$ sentences follows from the
$\NEXP$-completeness of $\Sigma_{2}$ sentences [17].

Consider an instance of a $\Pi_{2}$ sentence

$\gamma\coloneqq\forall\bm{y}\colon\exists\bm{x}\colon\psi(\bm{x},\bm{y})$

where $\psi$ is quantifier-free, $\bm{x}$ ranges over $\mathbb{Z}^{n}$, and
$\bm{y}$ ranges over $\mathbb{Z}^{m}$. The goal is to construct an existential
PA formula $\varphi$ such that $\varphi$ defines a WQO iff $\gamma$ is true.
First we define the formula

$\Gamma(\bm{y})\coloneqq\exists\bm{x}\psi(\bm{x},\bm{y})$

Now, define the existential Presburger formula $\varphi$ as follows.

$\displaystyle\varphi((x,\bm{x}),(y,\bm{y}))\coloneqq$
$\displaystyle(x<0\wedge y<0)\vee(x>0\wedge y>0)\vee(x<0\wedge y=0)$
$\displaystyle\vee$ $\displaystyle(x=0\wedge y>0)\vee(x=0\wedge y=0)$
$\displaystyle\vee$ $\displaystyle(x<0\wedge y>0\wedge\Gamma(\bm{y})).$

Here, both $\bm{x}$ and $\bm{y}$ range over $\mathbb{Z}^{m}$, hence $\varphi$
defines a relation in $\mathbb{Z}^{1+m}\times\mathbb{Z}^{1+m}$. Since the
existential quantifiers of $\Gamma$ can be moved in front of $\varphi$,
$\varphi$ is an existential Presburger instance.

######  Lemma 5.1.

$\varphi$ defines a WQO if and only if $\gamma$ is true i.e. $\Gamma(w)$ is
true $\forall\>\bm{w}\in\mathbb{Z}^{m}$.

######  Proof 5.2.

($\Rightarrow$) Let $\varphi$ define a WQO. Assume for contradiction there
exists $\bm{w}\in\mathbb{Z}^{m}$ such that $\Gamma(\bm{w})$ is false. Notice
that, by definition, $\varphi((-1,\bm{w}),(0,\bm{w}))$ and
$\varphi((0,\bm{w}),(1,\bm{w}))$ are true. By transitivity, we must have that
$\varphi((-1,\bm{w}),(1,\bm{w}))$ is true. Therefore, $\Gamma(\bm{w})$ must be
true. This is a contradiction.
($\Leftarrow$) Let $\Gamma(\bm{w})$ be true for all $\bm{w}\in\mathbb{Z}^{m}$.
Let $A$, $B$ and $C$ be sets of all vectors over $\mathbb{Z}^{1+m}$ with
negative, zero and positive first component, respectively. It is easy to see
that $\varphi$ relates all vectors within each of $A$, $B$ and $C$. Further,
$\varphi(\bm{u},\bm{v})$ is true if

  * •

$\bm{u}\in A$ and $\bm{v}\in B$, or

  * •

$\bm{u}\in B$ and $\bm{v}\in C$, or

  * •

$\bm{u}\in A$ and $\bm{v}\in C$.

This means that $\varphi$ must be a transitive, reflexive relation. Hence,
$\varphi$ trivially defines a WQO: in any infinite sequence
$\bm{u}_{1},\bm{u}_{2},\dots$ of vectors over $\mathbb{Z}^{1+m}$, we can
always find $\bm{u}_{i},\bm{u}_{j}$ with $i<j$ such that both
$\bm{u}_{i},\bm{u}_{j}$ belong to either $A$ or $B$ or $C$. Since $\varphi$
relates all vectors within each of these, the lemma follows.

##### Monadic decomposability

Let us now show the lower bound for Corollary 3.6, i.e., that monadic
decomposability for $\exists\mathrm{PA}$ formulas is $\coNEXP$-hard. The idea
is the same as the $\coNP$-hardness for quantifier-free formulas in [2]222As
Anthony W. Lin and Matthew Hague explained to us, it would also not be
difficult to adapt the idea of the $\coNP$ lower bound in [20, Lem. 2].. We
reduce from the $\Pi_{2}$-fragment of Presburger arithmetic, which is known to
be $\coNEXP$-complete (see the discussion around Corollary 3.3). Suppose we
are given a $\Pi_{2}$-formula
$\varphi=\forall\bm{x}\exists\bm{y}\colon\psi(\bm{x},\bm{y})$, where $\bm{x}$
contains $n$ variables, and $\bm{y}$ contains $m$ variables. We claim that the
existential formula $\kappa=\exists\bm{y}\colon\psi(\bm{x},\bm{y})\vee
z_{1}=z_{2}$ (which has free variables $\bm{x}$, $z_{1}$, $z_{2}$) is
monadically decomposable if and only if $\varphi$ holds (see Section 5), which
would clearly complete the reduction.

Indeed, if $\varphi$ holds, then $\kappa$ is satisfied for every vector in
$\mathbb{Z}^{n+2}$ and is thus clearly monadically decomposable. Conversely,
if $\varphi$ does not hold, then there is some $\bm{a}\in\mathbb{Z}^{n}$ so
that $\exists\bm{y}\colon\psi(\bm{a},\bm{y})$ fails to hold. If $\kappa$ were
monadically decomposable, then so would the formula
$\kappa\wedge\bm{x}=\bm{a}$, but this is equivalent to $z_{1}=z_{2}$, which is
clearly not monadically decomposable. This establishes the claim and hence
$\coNEXP$-hardness.

##  6 An exponential lower bound for quantifier elimination

Our main results show that one can eliminate a block of existential
quantifiers with only an exponential blow-up. Using an example from [17, Thm.
2], we will now prove an exponential lower bound, even if constants are
encoded in binary.

In the presence of binary encoded constants, we cannot use Weispfenning’s
lower bound argument [33, Thm. 3.1] (even for a singly exponential lower
bound), which compares norms of vectors in finite sets defined by
$\exists\mathrm{PA}$ vs. quantifier-free formulas. Indeed, it is a simple
consequence of Pottier’s bounds on Hilbert bases [24] that finite sets defined
by $\exists\mathrm{PA}$ formulas consist of at most exponentially large
vectors. With binary encoded constants, one easily constructs quantifier-free
formulas defining finite sets of exponentially large vectors.

Instead, we measure the periodicity of infinite sets. Recall that every
Presburger formula with one free variable defines an _ultimately periodic_ set
$S\subseteq\mathbb{Z}$, meaning that there are $n_{0},p\in\mathbb{N}$, $p\geq
1$, such that for every $n\in\mathbb{Z}$, $|n|\geq n_{0}$, we have $n+p\in S$
if and only if $n\in S$. Such a $p$ is called a _period_ of $S$. For a formula
$\varphi$ with one free variable, we denote by $|\varphi|_{\mathsf{p}}$ the
_smallest_ period of the set defined by $\varphi$. In [17, Thm. 2], Haase
constructs333See also Appendix B. a sequence $(\Phi_{n}(x))_{n\geq 0}$ of
$\exists\mathrm{PA}$ formulas of size $O(n^{2})$ such that
$|\Phi_{n}|_{\mathsf{p}}$ is at least $2^{2^{\Omega(n)}}$. The following will
imply that the formulas $\Phi_{n}$ require exponential-sized quantifier-free
equivalents:

######  Lemma 6.1.

Let $\varphi$ be quantifier-free with one free variable. Then
$|\varphi|_{\mathsf{p}}\leq 2^{|\varphi|}$.

######  Proof 6.2.

We prove this by structural induction. If $\varphi$ is an atom $ax\leq b$,
then $|\varphi|_{\mathsf{p}}=1$. If $\varphi$ is an atom $ax\equiv b\bmod{c}$
with constants $a,b,c$ written in binary, then
$|\varphi|_{\mathsf{p}}\leq|c|\leq 2^{|\varphi|}$. Moreover,
$|\neg\varphi|_{\mathsf{p}}=|\varphi|_{\mathsf{p}}$. Now observe that if
$S_{1},S_{2}\subseteq\mathbb{Z}$ are ultimately periodic sets, then we have
$|S_{1}\cup
S_{2}|_{\mathsf{p}}\leq|S_{1}|_{\mathsf{p}}\cdot|S_{2}|_{\mathsf{p}}$ and
$|S_{1}\cap
S_{2}|_{\mathsf{p}}\leq|S_{1}|_{\mathsf{p}}\cdot|S_{2}|_{\mathsf{p}}$. This
implies
$|\varphi_{1}\vee\varphi_{2}|_{\mathsf{p}}\leq|\varphi_{1}|_{\mathsf{p}}\cdot|\varphi_{2}|_{\mathsf{p}}\leq
2^{|\varphi_{1}|+|\varphi_{2}|}\leq 2^{|\varphi|}$ and similarly
$|\varphi_{1}\wedge\varphi_{2}|_{\mathsf{p}}\leq|\varphi_{1}|_{\mathsf{p}}\cdot|\varphi_{2}|_{\mathsf{p}}\leq
2^{|\varphi_{1}|+|\varphi_{2}|}\leq 2^{|\varphi|}$.

Now indeed, if $(\varphi_{n})_{n\geq 0}$ is a sequence of quantifier-free
equivalents of $(\Phi_{n})_{n\geq 0}$, then for some constant $c>0$ and large
$n$, we have
$2^{|\varphi_{n}|}\geq|\varphi_{n}|_{\mathsf{p}}=|\Phi_{n}|_{\mathsf{p}}\geq
2^{2^{cn}}$ and hence $|\varphi_{n}|\geq 2^{cn}$.

pages main.pages.ctrpages pages0 pages

## References

  * [1] Parosh A. Abdulla, Karlis Čerāns, Bengt Jonsson, and Yih-Kuen Tsay.  Algorithmic analysis of programs with well quasi-ordered domains.  Inform. and Comput., 160(1–2):109–127, 2000.  doi:10.1006/inco.1999.2843.
  * [2] Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, and Georg Zetzsche.  Ramsey quantifiers in linear arithmetics.  In Proc. POPL 2024, pages 1–32, 2024.  doi:10.1145/3632843.
  * [3] Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, and Georg Zetzsche.  Ramsey quantifiers in linear arithmetics, 2023.  arXiv:2311.04031, doi:10.48550/arXiv.2311.04031.
  * [4] Itshak Borosh and Leon B. Treybig.  Bounds on positive integral solutions of linear Diophantine equations.  P. Am. Math. Soc., 55:299–304, 1976.  doi:10.1090/S0002-9939-1976-0396605-3.
  * [5] W. Cook, A. M. H. Gerards, A. Schrijver, and É. Tardos.  Sensitivity theorems in integer linear programming.  Math. Program., 34:251–264, 1986.  doi:10.1007/BF01582230.
  * [6] D. C. Cooper.  Theorem proving in arithmetic without multiplication.  In Bernard Meltzer and Donald Michie, editors, Proceedings of the Seventh Annual Machine Intelligence Workshop, Edinburgh, 1971, volume 7, pages 91–99. Edinburgh University Press, 1972.
  * [7] Alain Finkel.  A generalization of the procedure of Karp and Miller to well structured transition systems.  In Proc. ICALP 1987, volume 267 of Lecture Notes in Computer Science, pages 499–508. Springer, 1987.  doi:10.1007/3-540-18088-5_43.
  * [8] Alain Finkel and Ekanshdeep Gupta.  The well structured problem for Presburger counter machines.  In Proc. FSTTCS 2019, volume 150 of LIPIcs, pages 41:1–41:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.  doi:10.4230/LIPICS.FSTTCS.2019.41.
  * [9] Alain Finkel and Ekanshdeep Gupta.  The well structured problem for Presburger counter machines.  CoRR, abs/1910.02736, 2019.  arXiv:1910.02736, doi:10.48550/arXiv.1910.02736.
  * [10] Alain Finkel and Philippe Schnoebelen.  Well-structured transition systems everywhere!  Theor. Comput. Sci., 256(1–2):63–92, 2001.  doi:10.1016/S0304-3975(00)00102-X.
  * [11] Michael J. Fischer and Michael O. Rabin.  Super-exponential complexity of Presburger arithmetic.  In Bob F. Caviness and Jeremy R. Johnson, editors, Quantifier Elimination and Cylindrical Algebraic Decomposition, pages 122–135, Vienna, 1998\. Springer Vienna.  doi:10.1007/978-3-7091-9459-1_5.
  * [12] Martin Fürer.  The complexity of Presburger arithmetic with bounded quantifier alternation depth.  Theor. Comput. Sci., 18:105–111, 1982.  doi:10.1016/0304-3975(82)90115-3.
  * [13] Seymour Ginsburg and Edwin H Spanier.  Bounded regular sets.  P. Am. Math. Soc., 17(5):1043–1049, 1966.  doi:10.1090/S0002-9939-1966-0201310-3.
  * [14] Erich Grädel.  Dominoes and the complexity of subclasses of logical theories.  Ann. Pure Appl. Log., 43(1):1–30, 1989.  doi:10.1016/0168-0072(89)90023-7.
  * [15] Stéphane Grumbach, Philippe Rigaux, and Luc Segoufin.  Spatio-temporal data handling with constraints.  GeoInformatica, 5(1):95–115, 2001.  doi:10.1023/A:1011464022461.
  * [16] Florent Guépin, Christoph Haase, and James Worrell.  On the existential theories of Büchi arithmetic and linear $p$-adic fields.  In Proc. LICS 2019, pages 1–10. IEEE, 2019.  doi:10.1109/LICS.2019.8785681.
  * [17] Christoph Haase.  Subclasses of Presburger arithmetic and the weak EXP hierarchy.  In Proc. CSL-LICS 2014, pages 47:1–47:10. ACM, 2014.  doi:10.1145/2603088.2603092.
  * [18] Christoph Haase and Georg Zetzsche.  Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests.  In Proc. LICS 2019, pages 1–14. IEEE, 2019.  doi:10.1109/LICS.2019.8785850.
  * [19] Jacques Hadamard.  Rèsolution d’une question relative aux dèterminants.  B. Sci. Math., 2(17):240–246, 1893.
  * [20] Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu.  Monadic decomposition in integer linear arithmetic.  In Proc. IJCAR 2020, volume 12166 of Lecture Notes in Computer Science, pages 122–140. Springer, 2020.  doi:10.1007/978-3-030-51074-9_8.
  * [21] Gabriel Kuper, Leonid Libkin, and Jan Paredaens.  Constraint Databases.  Springer, 2000.
  * [22] Mohan Nair.  On Chebyshev-type inequalities for primes.  Am. Math. Mon., 89(2):126–129, 1982.  doi:10.2307/2320934.
  * [23] Derek C. Oppen.  A $2^{2^{2^{pn}}}$ upper bound on the complexity of Presburger arithmetic.  J. Comput. Syst. Sci., 16(3):323–332, 1978.  doi:10.1016/0022-0000(78)90021-1.
  * [24] Loïc Pottier.  Minimal solutions of linear diophantine systems: Bounds and algorithms.  In Proc. RTA 1991, volume 488 of Lecture Notes in Computer Science, pages 162–173. Springer, 1991.  doi:10.1007/3-540-53904-2_94.
  * [25] Mojżesz Presburger.  Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt.  In Comptes Rendus du I congres de Mathematiciens des Pays Slaves, pages 92–101. Ksiaznica Atlas, 1929.
  * [26] C. R. Reddy and Donald W. Loveland.  Presburger arithmetic with bounded quantifier alternation.  In Proc. STOC 1978, pages 320–325, New York, NY, USA, 1978. ACM.  doi:10.1145/800133.804361.
  * [27] J. Barkley Rosser and Lowell Schoenfeld.  Approximate formulas for some functions of prime numbers.  Illinois J. Math., 6(1):64 – 94, 1962.  doi:10.1215/ijm/1255631807.
  * [28] Sasha Rubin.  Automata presenting structures: A survey of the finite string case.  Bull. Symb. Log., 14(2):169–209, 2008.  doi:10.2178/BSL/1208442827.
  * [29] Alexander Schrijver.  Theory of linear and integer programming.  John Wiley & Sons, 1986.
  * [30] Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, and Sergey Bereg.  Monadic decomposition.  J. ACM, 64(2):14:1–14:28, 2017.  doi:10.1145/3040488.
  * [31] Joachim von zur Gathen and Malte Sieveking.  A bound on solutions of linear integer equalities and inequalities.  Proceedings of the American Mathematical Society, 72(1):155–158, 1978.  doi:10.1090/S0002-9939-1978-0500555-0.
  * [32] Volker Weispfenning.  The complexity of almost linear Diophantine problems.  J. Symb. Comput., 10(5):395–403, 1990.  doi:10.1016/S0747-7171(08)80051-X.
  * [33] Volker Weispfenning.  Complexity and uniformity of elimination in Presburger arithmetic.  In Proc. ISSAC 1997, pages 48–53. ACM, 1997.  doi:10.1145/258726.258746.

##  Appendix A More Details for Lemma 4.7

We recall Cramer’s rule which has been used in the proof.

######  Proposition A.1 (Cramer’s rule).

Let a system of $n$ linear equations for $n$ unknowns be represented as

$Ax=b\,,$

where $A$ is an invertible $(n\times n)$ matrix. This system has as unique
solution given by $x=(x_{1},x_{2},\dots,x_{n})$ where,

$x_{i}=\frac{\det(A_{i})}{\det(A)}$

$A_{i}$ is the matrix formed by replacing the $i$th column of $A$ by $b$.

##  Appendix B Sets with large periods

The formula $\Phi_{n}$ constructed by Haase in [17, Thm. 2] defines the set

$S_{n}=\\{a\in\mathbb{N}\mid\exists b\colon 1<b<2^{n},\leavevmode\nobreak\
\text{$b$ divides $a$}\\}.$

and Haase argues that the smallest period of $S_{n}$ is $2^{2^{\Omega(n)}}$.
While the latter is true, the argument in [17] does not quite show this. The
proof of [17, Thm. 2] argues that the smallest period of $S_{n}$ is the least
common multiple of the numbers $\\{1,\ldots,2^{n}-1\\}$, which is lower
bounded by $2^{2^{\Omega(n)}}$ according to Nair [22]. However, as we will
see, the smallest period of $S_{n}$ is in fact a slightly smaller number. It
is still lower bounded $2^{2^{\Omega(n)}}$, but this requires a different
argument. We present a correction.

An easy fix for the result would be to instead define the set

$\displaystyle S^{\prime}_{n}$ $\displaystyle=\\{a\in\mathbb{N}\mid\exists
b\colon 1<b<2^{n},\leavevmode\nobreak\ \text{$b$ does not divide $a$}\\}$
$\displaystyle=\\{a\in\mathbb{N}\mid\exists b,c\colon
1<b<2^{n},\leavevmode\nobreak\ 1\leq c<2^{n},\leavevmode\nobreak\ \text{$b$
divides $a+c$}\\},$

for which a simple modification of the formulas $\Phi_{n}$ in [17] yields a
polynomial-sized $\exists\mathrm{PA}$ formula $\Phi^{\prime}_{n}$. Moreover,
the smallest period of $S^{\prime}_{n}$ is indeed the least common multiple of
$\\{1,\ldots,2^{n}-1\\}$, and so Nair’s bound would apply.

However, one can show that the smallest period of $S_{n}$ is indeed lower
bounded by $2^{2^{\Omega(n)}}$, just not by the least common multiple of
$\\{1,\ldots,2^{n}-1\\}$. For any natural $n\in\mathbb{N}$, define the
_primorial_ of $n$, in symbols $n\\#$, as the product of all primes $\leq n$.
Thus, if $p_{1},p_{2},\ldots$ is the sequence of all primes in ascending order
and $\pi(n)$ is the number of all prime numbers $\leq n$, then

$n\\#=\prod_{i=1}^{\pi(n)}p_{i}.$

######  Claim 1.

The smallest period of $S_{n}$ is $2^{n}\\#$.

######  Proof B.1.

Clearly, $2^{n}\\#$ is a period of $S_{n}$: $S_{n}$ is the set of all numbers
that have a prime divisor among $\\{2,\ldots,2^{n}-1\\}$, and adding or
subtracting the product of all these primes does not change that.

It remains to show that $2^{n}\\#$ is the smallest period of $S_{n}$. Suppose
$k$ is a period of $S_{n}$. We will show that every prime $p$ with $1<p<2^{n}$
is a divisor of $k$, which will clearly establish the claim. Let
$\\{p_{1},\ldots,p_{\ell}\\}$ be the primes in $\\{2,\ldots,2^{n}-1\\}$.
Towards a contradiction, suppose there is a prime $p_{j}$, $1\leq j\leq\ell$,
that does not divide $k$. By the Chinese Remainder Theorem, the system of
congruences

$\displaystyle x$ $\displaystyle\equiv 1\pmod{p_{i}}$ $\displaystyle\text{for
each $i\in\\{1,\ldots,\ell\\}$, $i\neq j$},$ $\displaystyle x$
$\displaystyle\equiv-k\pmod{p_{j}}$

has infinitely many solutions $a\in\mathbb{N}$. For each such $a$, we have
$a\notin S_{n}$, because $a$ is not divisible by any $p_{i}$, $1\leq
i\leq\ell$. However, $a+k$ is divisible by $p_{j}$, and thus $a+k\in S_{n}$.
Therefore, $k$ cannot be a period of $S_{n}$.

Using 1, we can now obtain the $2^{2^{\Omega(n)}}$ lower bound for the
smallest period of $S_{n}$. This is because equation (3.14) of [27] implies
that for every $m\geq 563$, we have $m\\#\geq 2^{m-1}$. In particular, for
$n\geq 10$, we have $2^{n}\\#\geq 2^{2^{n}-1}$. This proves that
$|\Phi_{n}|_{\mathsf{p}}$ is lower bounded by $2^{2^{\Omega(n)}}$.

##  Appendix C Incorrect lower bounds on eliminating a block of existential
quantifiers

We elaborate on a flaw in Weispfenning’s paper [33] which is a consequence of
misinterpreting results from the literature, from which he incorrectly
concludes that the elimination of a block of existential quantifiers from a
formula of Presburger arithmetic results in an inherent doubly exponential
blow-up.

The main result of Section 3 of [33] is Theorem 3.1, which states that
performing quantifier elimination on _arbitrary_ formulas of Presburger
arithmetic results in an inherent triply exponential blow-up, assuming unary
encoding of numbers. To this end, Weispfenning invokes a result by Fischer and
Rabin [11] who showed that there exists a function
$g\colon\mathbb{N}\to\mathbb{N}$ such that for almost all $n$,

$g(n)\geq 2^{2^{2^{n+1}}}\,,$

and who gave a family of formulas $\Phi_{n}(x,y,z)$ of Presburger arithmetic
of size linear in $n$ such that $\Phi_{n}(x,y,z)$ holds if and only if $0\leq
x,y,z<g(n)$ and $x\cdot y=z$. He then goes on concluding that the smallest
quantifier-free formula defining the set
$\\{z\in\mathbb{Z}\mid\Phi_{n}(1,z,z)\\}$ requires a formula of size at least
$g(n)$, assuming unary encoding of numbers.

Weispfenning then continues sketching how to adapt this approach in the
presence of a bounded number of quantifier alternations. To this end, he
appeals to a result by Fürer [12], which states that for some constant $r>0$,
one can define multiplication up to

$2^{2^{(n/a)^{ra}}}$ (4)

using a formula of length $n$ and $a$ quantifier alternations. Adapting his
line of reasoning from the general case, Weispfenning applies this to $a=1$
and concludes that eliminating a block of existential quantifiers yields an
inherent doubly exponential blow up. Fürer does indeed claim the existence of
such a family in the third paragraph in [12, p. 108]. However, a close
inspection of Fürer’s proof reveals that these formulas are not constructed
_for every $a$ and $n$_, but only _for infinitely many $a$ and $n$_. More
specifically, Fürer supposes some given $k,m\in\mathbb{N}$ and constructs a
formula of length $c(mk\log k+1)$ and $2m+d$ quantifier alternations (see the
seventh paragraph in [12, p. 108]). Here, $c$ and $d$ appear to be unspecified
constants. By choosing $a=2m+d$ and $n=c(mk\log k+1)$, Fürer’s claims then
yield multiplication up to (4) for a suitable $r>0$. In particular, Fürer’s
construction does not yield the existence of such formulas for _every_
$a\in\mathbb{N}$.

Of course, from the fact that existential Presburger arithmetic allows for
defining ultimately periodic sets with a doubly exponential period, cf.
Appendix B, it is not unreasonable to believe that this could somehow be
turned into a lower bound similar to the one claimed by Weispfenning. However,
such large periods can already be produced by an exponential intersection of
divisibility constraints and thus do not imply a doubly exponential lower
bound on the formula size after eliminating a block of existentially
quantified variables.

pagestotal main.pagestotal.ctrpagestotal pagestotal0 pagestotal

todos main.todos.ctrtodos todos0 todos