A common approach to solving problems in the sciences is to reduce them to solving some kind of system of equations. While in engineering and physics those systems often involve quantities over the reals, computer science predominantly deals with discrete domains such as the integers. However, performing arithmetic over the integers is computationally expensive, affecting both decidability and complexity. In some cases, solutions even grow too large to be explicitly constructed.

This talk will survey recent results and techniques for deciding integer logics, even when solutions are prohibitively large to construct explicitly. In more technical terms, I will outline how we can establish an NP upper bound for existential Büchi arithmetic and an EXPSPACE upper bound for existential Semenov arithmetic, using techniques from automata theory and specifically vector addition systems. The talk is aimed at a broad audience and assumes no prior knowledge of these logics. I will also discuss applications, particularly in solving restricted classes of string constraints.