Geometric decision procedures and the VC dimension of linear arithmetic theories
Dmitry V. Chistikov, Christoph Haase, Alessio Mansutti · 2022
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].