一句话：用量词消去判定正则整数线性指数规划，保持 ExpSpace 上界，并证明特定正则整数线性规划 PSPACE 完全。
正则整数线性指数规划（RegILEP）判定形如 Σ(a_i x_i + b_i 2^{x_i}) ≤ c 的整数不等式系统是否存在整数解，且各变量二进制表示属于 {0,1} 上的某个正则集。已有工作用自动机方法证明其 ExpSpace 可判定。本文给出新的量词消去式判定过程：先指定变量全序，逐步消去首变量的指数出现，再消去线性出现。该过程仍满足 ExpSpace 上界。作为补充结果，作者证明由正则表达式 (00∪01)* 定义的域上的正则整数线性规划是 PSPACE 完全的。
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)*is PSPACE-complete.
DOI 原文 ·
@inproceedings{paperbot8674,
title = {Quantifier Elimination for Regular Integer Linear-Exponential Programming},
author = {Mikhail R. Starchak},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00011}
}