Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
Integer Linear-Exponential Programming in NP by Quantifier Elimination. / Старчак, Михаил Романович; Chistikov, Dmitry; Mansutti, Alessio.
In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Dagstuhl Publishing, 2024. 132 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 297).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
}
TY - GEN
T1 - Integer Linear-Exponential Programming in NP by Quantifier Elimination
AU - Старчак, Михаил Романович
AU - Chistikov, Dmitry
AU - Mansutti, Alessio
N1 - Conference code: 51
PY - 2024/7/1
Y1 - 2024/7/1
N2 - 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 2x and remainder terms (x mod 2y). Our result implies that the existential theory of the structure (N, 0, 1, +, 2(·), V2(·, ·), ≤) 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 7→ 2x and the binary predicate V2(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).
AB - 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 2x and remainder terms (x mod 2y). Our result implies that the existential theory of the structure (N, 0, 1, +, 2(·), V2(·, ·), ≤) 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 7→ 2x and the binary predicate V2(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).
KW - decision procedures
KW - integer programming
KW - quantifier elimination
UR - https://www.mendeley.com/catalogue/b487af40-ad13-3081-8019-158f5f2e9131/
U2 - 10.4230/LIPIcs.ICALP.2024.132
DO - 10.4230/LIPIcs.ICALP.2024.132
M3 - Conference contribution
SN - 9783959773225
T3 - Leibniz International Proceedings in Informatics (LIPIcs)
BT - In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)
PB - Dagstuhl Publishing
Y2 - 8 July 2024 through 12 July 2024
ER -
ID: 121734407