An Automata-Theoretic Approach to Presburger Arithmetic Constraints

This paper introduces a finite-automata based representation of
Presburger arithmetic definable sets of integer vectors. The
representation consists of concurrent automata operating on the
binary encodings of the elements of the represented sets. This
representation has several advantages. First, being
automata-based it is operational in nature and hence leads directly
to algorithms, for instance all usual operations on sets of integer
vectors translate naturally to operations on automata. Second, the
use of concurrent automata makes it compact. Third, it is insensitive
to the representation size of integers. Our representation can be
used whenever arithmetic constraints are needed. To illustrate its
possibilities we show that it can handle integer programming optimally,
and that it leads to a new original algorithm for the satisfiability
of arithmetic inequalities.