Quantifier Elimination for Regular Integer Linear-Exponential Programming

Regular integer linear-exponential programming (RegILEP) asks whether a system of inequalities of the form $\sum\nolimits_{i = 1..n} {\left({{a_i}\cdot{x_i} + {b_i}\cdot{2^{{x_i}}}}\right)} \leq c$, where all coefficients are integers, has a solution in the integers whose binary representations belong to some regular set over the alphabet {0,1}. RegILEP has recently been proved decidable in ExpSpace using purely automata-theoretic techniques. The first contribution of the paper is a novel decision procedure for RegILEP, which works in a quantifier elimination fashion: after specifying a total order on the variables, the procedure gradually excludes the exponential occurrences of the leading variable and then eliminates the linear ones. This decision procedure meets the existing ExpSpace upper bound for the problem. As a complementary result, we show that regular integer linear programming for the domain defined by the regular expression (00∪01)<sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">*</sup> is PSPACE-complete.