7
$\begingroup$

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.

$\endgroup$

1 Answer 1

6
$\begingroup$

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

$\endgroup$
1
  • $\begingroup$ This looks like exactly what I was looking for. Thanks so much! $\endgroup$ Jan 27, 2015 at 17:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.