Integer Linear-Exponential Programming in NP by Quantifier Elimination

TL;DR

This work resolves the feasibility of linear-exponential systems, extending integer programming with base-$2$ exponentials and modulo constraints, by giving a nondeterministic polynomial-time quantifier-elimination procedure. Central to the approach is GaussQE, a polynomial-time QB-like elimination for linear inequalities over $\mathbb{Z}$ that leverages Bareiss’ ideas to control growth, together with LinExpSat, ElimMaxVar, and SolvePrimitive that progressively reduce linear-exponential problems to linear constraints. The main contributions are: (i) NP-membership for integer and natural-number linear-exponential feasibility, (ii) NP-completeness for the existential Büchi--Semenov arithmetic, and (iii) a bridge between logic and integer programming via quantifier elimination that yields practical decision procedures. These results tighten the complexity landscape relative to EXPSPACE bounds and provide a framework for further exploration of existential theories involving exponentiation and modular constraints.

Abstract

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

Theorems & Definitions (3)

• Theorem 1
• Theorem 2
• Theorem 3