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).