一句话:证明带星号的存在性 Presburger 算术为 NEXP 完全,并统一三个判定问题及其固定参数复杂度。
本文研究带 Kleene 星号(可嵌套)的存在性 Presburger 算术的可满足性复杂度。该逻辑自然扩展了 Presburger 算术,并统一了图群中有理子集成员问题与带状态和嵌套零测试的整数向量加法系统可达性问题。作者证明带星号存在性 Presburger 算术可满足性为 NEXP 完全,且上述三个问题可在多项式时间互相归约。对于固定参数变体,即固定逻辑的星号高度、图群成员问题的图参数、以及整数向量加法系统中不同零测试的个数,三者均为 NP 完全。由此得到固定图群上有理子集成员问题的完整复杂度图景:图为团时为 NL 完全,为不相交团并时为 P 完全,为传递森林且非团并时为 NP 完全,否则不可判定。
We study the computational complexity of existential Presburger arithmetic with (possibly nested occurrences of) a Kleene-star operator. In addition to being a natural extension of Presburger arithmetic, our investigation is motivated by two other decision problems. The first problem is the rational subset membership problem in graph groups. A graph group is an infinite group specified by a finite undirected graph. While a characterisation of graph groups with a decidable rational subset membership problem was given by Lohrey and Steinberg [J. Algebra, 320(2) (2008)], it has been an open problem (i) whether the decidable fragment has elementary complexity and (ii) what is the complexity for each fixed graph group. The second problem is the reachability problem for integer vector addition systems with states and nested zero tests. We prove that the satisfiability problem for existential Pres-burger arithmetic with stars is NEXP-complete and that all three problems are polynomially inter-reducible. Moreover, we consider for each problem a variant with a fixed parameter: We fix the star-height in the logic, a graph parameter for the membership problem, and the number of distinct zero-tests in the integer vector addition systems. We establish NP-completeness of all problems with fixed parameters. In particular, this enables us to obtain a complete description of the complexity landscape of the rational subset membership problem for fixed graph groups: If the graph is a clique, the problem is N L-complete. If the graph is a disjoint union of cliques, it is P-complete. If it is a transitive forest (and not a union of cliques), the problem is NP-complete. Otherwise, the problem is undecidable.