A classical theorem in Integer Programming by Lenstra says that any integer system $$A x \le b$$ can be solved in polynomial time, where $A \in \mathbb{Z}^{m \times n}, x \in \mathbb{Z}^n, b \in \mathbb{Z}^m$. Here we fix the dimension $n$ of the variables to be solved over (it would be NP-complete to solve for $n$ arbitrary).

Viewed under the the lense of logic/computational complexity, this theorem says that any existential statement $$ \exists x \in \mathbb{Z}^n : \Phi(x)$$ can be decided in polynomial time, where $\Phi$ is a formula in Presburger arithmetic.

By the work of Semenov, we also know that Presburger arithmetic with added precidates, such as "x is a power of 2", or "x is a Fibonacci number" is decidable.

Question: For $n$ fixed, can we decide in polynomial time sentences of the form $$\exists x \in \mathbb{Z}^n : \Psi(x)$$ where $\Psi(x)$ is a Presburger formula, augmented with some the Fibonacci (or Power of 2) predicates?

Example: Does the following system have a solution?

$$ \begin{cases} 3x_1 + 2x_2 \le 1000 \\ 17x_2 - x_1 \le 5 \\ 2x_1 + 5x_2 \quad \text{is a power of 2} \end{cases} $$

  • 1
    $\begingroup$ Are you restricting to $x_i>0$? $\endgroup$ – user76479 May 13 '16 at 18:30
  • $\begingroup$ it looks very unlikely to me... $\endgroup$ – Dima Pasechnik May 13 '16 at 20:23
  • $\begingroup$ Yes we can restrict to positive variables. I don't think it will change much. $\endgroup$ – Danny Nguyen May 13 '16 at 21:05
  • 1
    $\begingroup$ switching to positive variables is a linear change of variables, you double the number of them, which is OK in this setting. $\endgroup$ – Dima Pasechnik May 13 '16 at 21:23
  • 1
    $\begingroup$ @Turbo The simplest way to have an SMT solver work on this is to have a literal for each power of two in a reasonable range (note this is imposing bounds) and then just do its thing. I’m not sure if there is a better way to do things offhand. A good place to start after en.wikipedia.org/wiki/Satisfiability_modulo_theories is decision-procedures.org $\endgroup$ – Steve Huntsman May 17 '18 at 17:10

Do I miss something? It's well known that deciding propositions in Presberger arithmetic takes double-exponential time. Integer programming would seem to be worse rather than better than a mere decision algorithm, which could be seen as a solver whose result was constrained to be in the set {0,1}.

  • $\begingroup$ I think that the formulas $\Phi$ involved here are quantifier-free, so the doubly-exponential bound doesn't come into play. $\endgroup$ – Noah Schweber Jun 17 '16 at 17:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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