Quanitifier Free Presburger Arithmetic: Upper bound on solution size?

Question

DISCLAIMER: I had originally posted this to CS.SE, 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, 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.

Answer 1

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)

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).