Complejidad de la programación entera con predicados añadidos

Question

Un teorema clásico en Programación Entera por Lenstra dice que cualquier sistema de enteros $$A x \le b$$ se puede resolver en tiempo polinómico, donde $A \in \mathbb{Z}^{m \times n}, x \in \mathbb{Z}^n, b \in \mathbb{Z}^m$. Aquí fijamos la dimensión $n$ de las variables a resolver (sería NP-completo resolver para $n$ arbitrario).

Visto bajo la lente de la lógica/complexidad computacional, este teorema dice que cualquier declaración existencial $$ \exists x \in \mathbb{Z}^n : \Phi(x)$$ se puede decidir en tiempo polinómico, donde $\Phi$ es una fórmula en la aritmética de Presburger.

Por el trabajo de Semenov, también sabemos que la aritmética de Presburger con predicados adicionales, como "x es una potencia de 2", o "x es un número Fibonacci" es decidible.

Pregunta: Para $n$ fijo, ¿podemos decidir en tiempo polinómico oraciones de la forma $$\exists x \in \mathbb{Z}^n : \Psi(x)$$ donde $\Psi(x)$ es una fórmula de Presburger, aumentada con algunos predicados de Fibonacci (o Potencia de 2)?

Ejemplo: ¿Tiene el siguiente sistema una solución?

$$ \begin{cases} 3x_1 + 2x_2 \le 1000 \\ 17x_2 - x_1 \le 5 \\ 2x_1 + 5x_2 \quad \text{es una potencia de 2} \end{cases} $$

Answer 1

¿Me estoy perdiendo algo? Es bien sabido que decidir proposiciones en la aritmética de Presberger lleva tiempo de doble exponencial. La programación entera parecería ser peor en lugar de mejor que un simple algoritmo de decisión, que podría verse como un solucionador cuyo resultado estaba restringido a estar en el conjunto {0,1}.