Integer Linear-Exponential Programming in NP by Quantifier Elimination
<|reference_start|>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^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).<|reference_end|>
@article{chistikov2024integer,
    title={Integer Linear-Exponential Programming in NP by Quantifier Elimination},
    author={Dmitry Chistikov and Alessio Mansutti and Mikhail R. Starchak},
    journal={arXiv preprint arXiv:2407.07083},
    year={2024},
    doi={10.4230/LIPIcs.ICALP.2024.132},
    archivePrefix={arXiv},
    eprint={2407.07083},
    primaryClass={cs.LO}
}