一句话：给出 LIA 的三重指数几何判定过程，并证明其可定义集 VC 维的双重指数上界，解决 Nguyen–Pak 猜想。
本文研究线性整数算术（LIA，即 Presburger 算术）的两个公开问题。作者提出基于半线性集操作的几何判定过程，其时间复杂度为三重指数，与最优的量词消去和自动机方法相当。基于该结果，作者证明 LIA 可定义集的 Vapnik–Chervonenkis（VC）维具有双重指数上界，从而证实 D. Nguyen 与 I. Pak 的猜想。方法核心是新的半线性集与实数线性算术（LRA）可定义集的分解结果，并给出计算（ℝ-）半线性集补集的新算法，该算法在与布尔运算和投影反复组合时不会导致非初等膨胀，解决了半线性集上长期未决的问题；LRA 的类似结果也被获得。
This paper resolves two open problems on linear integer arithmetic (LIA), also known as Presburger arithmetic. First, we give a triply exponential geometric decision procedure for LIA, i.e., a procedure based on manipulating semilinear sets. This matches the running time of the best quantifier elimination and automata-based procedures. Second, building upon our first result, we give a doubly exponential upper bound on the Vapnik–Chervonenkis (VC) dimension of sets definable in LIA, proving a conjecture of D. Nguyen and I. Pak [Combinatorica 39, pp. 923–932, 2019]. These results partially rely on an analysis of sets definable in linear real arithmetic (LRA), and analogous results for LRA are also obtained. At the core of these developments are new decomposition results for semilinear and -semilinear sets, the latter being the sets definable in LRA. These results yield new algorithms to compute the complement of (-)semilinear sets that do not cause a non-elementary blowup when repeatedly combined with procedures for other Boolean operations and projection. The existence of such an algorithm for semilinear sets has been a long-standing open problem.