<p>You can find an answer in the following paper:</p>

<p>Joachim von zur Gathen, Malte Sieveking. A bound on solutions of integer linear equalities and inequalities.
Proc. AMS 72(1) (1978)
(<a href="http://www.ams.org/journals/proc/1978-072-01/S0002-9939-1978-0500555-0/S0002-9939-1978-0500555-0.pdf">pdf</a>)</p>

<p>A simple corollary of their result follows.
Let's say we have two integer systems, $A x = b$ and $C x \ge d$,
where you want $x$ to be in $\mathbb Z^n$.
Consider determinants of all square submatrices of the matrix $E = \left(\matrix{A &amp; b \\ C &amp; d}\right)$
and denote by $M$ an upper bound on their absolute values.
(In other words, set $M$ to be larger than or equal to the absolute value of all minors of $E$.)
Now, if there exists an $x \in \mathbb Z^n$ satisfying both $A x = b$ and $C x \ge d$, then
there exists such an $x$ whose components are at most $(n + 1) M$ in absolute value.</p>

<p>It remains to note that a determinant of a $k \times k$-matrix $S$ is at most $k!\, \|S\|_{\mathsf{max}}^k$
where $\|S\|_{\mathsf{max}} = \max |s_{i j}|$. Combining these two bounds will give a specific polynomial
bound on the size of a smallest solution (and this is already an easy exercise).</p>

CC BY-SA 3.0
2015-01-27T17:56:28.447Z
This looks like exactly what I was looking for. Thanks so much!
Joey Eremondi
CC BY-SA 3.0
2015-01-27T13:23:34.310Z
2015-01-27T13:23:34.310Z
dd1
<p>DISCLAIMER: I had originally posted this to <a href="https://cs.stackexchange.com/questions/37346/quanitifier-free-presburger-arithmetic-upper-bound-on-solution-size">CS.SE</a>, but I've deleted it and moved it here, since it received little attention, and I think it is a research level question.</p>

<p>According to <a href="http://www.cs.cmu.edu/~bryant/pubdir/lics04.pdf" rel="nofollow noreferrer">this paper</a>, if there is a solution to a quantifier free Presburger formula, there is a solution whose size in bits is polynomial in the problem size. This allows the problem to be in $NP$, easier than arbitrary Presburger formulas.</p>

<p>However, the paper doesn't explicitly reference where this bound comes from, just mentioning a connection to Integer Linear Programming.</p>

<p>I was wondering if anyone knew, what was the exact bound on the solution size, or if they could provide a reference for such? I have another problem which I can phrase as a QF Presburger formula, and I'd like to find a definite bound on the solution size. But I'm also trying to work it into an actual software system, so simply knowing "there exists a polynomial" doesn't help me much.</p>

<cc.complexity-theory><ds.algorithms><reference-request><time-complexity><integer-programming>
Quanitifier Free Presburger Arithmetic: Upper bound on solution size?
Joey Eremondi
# Quanitifier Free Presburger Arithmetic: Upper bound on solution size?

(Asked by: username_0 on 2015-01-24)

DISCLAIMER: I had originally posted this to [CS.SE](https://cs.stackexchange.com/questions/37346/quanitifier-free-presburger-arithmetic-upper-bound-on-solution-size), but I've deleted it and moved it here, since it received little attention, and I think it is a research level question.

According to [this paper](http://www.cs.cmu.edu/~bryant/pubdir/lics04.pdf), if there is a solution to a quantifier free Presburger formula, there is a solution whose size in bits is polynomial in the problem size. This allows the problem to be in $NP$, easier than arbitrary Presburger formulas.

However, the paper doesn't explicitly reference where this bound comes from, just mentioning a connection to Integer Linear Programming.

I was wondering if anyone knew, what was the exact bound on the solution size, or if they could provide a reference for such? I have another problem which I can phrase as a QF Presburger formula, and I'd like to find a definite bound on the solution size. But I'm also trying to work it into an actual software system, so simply knowing "there exists a polynomial" doesn't help me much.

**Tags:** cc.complexity-theory, ds.algorithms, reference-request, time-complexity, integer-programming


---

## 1 answers

### Answer by username_1 on 2015-01-27. Score: 6 | Accepted answer

You can find an answer in the following paper:

Joachim von zur Gathen, Malte Sieveking. A bound on solutions of integer linear equalities and inequalities.
Proc. AMS 72(1) (1978)
([pdf](http://www.ams.org/journals/proc/1978-072-01/S0002-9939-1978-0500555-0/S0002-9939-1978-0500555-0.pdf))

A simple corollary of their result follows.
Let's say we have two integer systems, $A x = b$ and $C x \ge d$,
where you want $x$ to be in $\mathbb Z^n$.
Consider determinants of all square submatrices of the matrix $E = \left(\matrix{A & b \\ C & d}\right)$
and denote by $M$ an upper bound on their absolute values.
(In other words, set $M$ to be larger than or equal to the absolute value of all minors of $E$.)
Now, if there exists an $x \in \mathbb Z^n$ satisfying both $A x = b$ and $C x \ge d$, then
there exists such an $x$ whose components are at most $(n + 1) M$ in absolute value.

It remains to note that a determinant of a $k \times k$-matrix $S$ is at most $k!\, \|S\|\_{\mathsf{max}}^k$
where $\|S\|\_{\mathsf{max}} = \max |s\_{i j}|$. Combining these two bounds will give a specific polynomial
bound on the size of a smallest solution (and this is already an easy exercise).

> **Comments:**
> **username_0**: This looks like exactly what I was looking for. Thanks so much!  

---

