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.
Quanitifier Free Presburger Arithmetic: Upper bound on solution size?
cc.complexity theory;ds.algorithms;reference request;time complexity;integer programming
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$, thenthere 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 polynomialbound on the size of a smallest solution (and this is already an easy exercise).