# Complexity of integer programming with added predicates

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}$$

• Are you restricting to $x_i>0$? – user76479 May 13 '16 at 18:30
• it looks very unlikely to me... – Dima Pasechnik May 13 '16 at 20:23
• Yes we can restrict to positive variables. I don't think it will change much. – Danny Nguyen May 13 '16 at 21:05
• switching to positive variables is a linear change of variables, you double the number of them, which is OK in this setting. – Dima Pasechnik May 13 '16 at 21:23
• @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 – Steve Huntsman May 17 '18 at 17:10

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