Integer Linear-Exponential Programming in NP by Quantifier Elimination

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ˣ and remainder terms (x 2ʸ). Our result implies that the existential theory of the structure (N,0,1,+,2(·),V₂(·,·),≤) 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 ↦ 2ˣ and the binary predicate V₂(x,y) that is true whenever y ≥ 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).