Integer Linear-Exponential Programming in NP by Quantifier Elimination

TL;DR

This paper introduces an NP procedure for solving linear-exponential systems with integer solutions, extending the satisfiability analysis of a complex logical theory and improving previous computational bounds.

Contribution

It presents a novel NP algorithm for linear-exponential systems using quantifier elimination, extending the existential theory of natural numbers with exponential and divisibility functions.

Findings

Decides satisfiability of linear-exponential systems in NP

Extends the existential theory of natural numbers with exponential and divisibility functions

Improves the complexity bound from EXPSPACE to NP

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