Mixed and Integer Linear Programming Using Automata Techniques∗

We present a comprehensive overview of automata tech-niques for deciding first order logical theories. These tech-niques are useful in Integer Linear Programming and Mixed Integer Linear Programming, which in turn have wide appli-cations in diverse areas of computer science and engineering. We have several goals in this paper. The first is to solidify the theory underpinning the automata techniques. Since much of the previous literature in this subject was published only in the form of Extended Abstracts, many of the proofs to key theorems were missing. We fill in these gaps. Another objective is to explore extending the automata ap-proach to address questions beyond satisfiability. A key problem for the (M)ILP community has been the enumera-tion of solutions to systems. We present a way of addressing this question within the automata framework. Finally, we consider alternate approaches to (M)ILP and discuss their relative advantages and disadvantages as com-pared to the automata formulation