This paper provides an NP procedure that decides whether a linear-exponential system of constraints has an integer solution. Linear-exponential systems extend standard integer linear programs with exponential terms $2^x$ and remainder terms ${(x \bmod 2^y)}$. Our result implies that the existential theory of the structure $(\mathbb{N},0,1,+,2^{(\cdot)},V_2(\cdot,\cdot),\leq)$ has an NP-complete satisfiability problem, thus improving upon a recent EXPSPACE upper bound. This theory extends the existential fragment of Presburger arithmetic with the exponentiation function $x \mapsto 2^x$ and the binary predicate $V_2(x,y)$ that is true whenever $y \geq 1$ is the largest power of $2$ dividing $x$. Our procedure for solving linear-exponential systems uses the method of quantifier elimination. As a by-product, we modify the classical Gaussian variable elimination into a non-deterministic polynomial-time procedure for integer linear programming (or: existential Presburger arithmetic).

翻译：本文提出了一种NP判定程序，用于判断线性-指数约束系统是否存在整数解。线性-指数系统在标准整数线性规划的基础上扩展了指数项$2^x$和余数项${(x \bmod 2^y)}$。我们的研究结果表明，结构$(\mathbb{N},0,1,+,2^{(\cdot)},V_2(\cdot,\cdot),\leq)$的存在性理论具有NP完全的可满足性问题，从而改进了近期提出的EXPSPACE上界。该理论将Presburger算术的存在片段扩展为包含指数函数$x \mapsto 2^x$和二元谓词$V_2(x,y)$——当$y \geq 1$是整除$x$的最大2的幂时该谓词为真。我们求解线性-指数系统的程序采用了量词消去法。作为副产品，我们将经典的高斯变量消去法改进为适用于整数线性规划（即存在性Presburger算术）的非确定性多项式时间程序。