Presburger formulas [KK67] are those formulas that can be constructed by combining affine constraints on integer variables with the logical operations , and , and the quantifiers and . The affine constraints can be either equality constraints or inequality constraints (abbreviated as EQs and GEQs respectively). For example, the formulas in the previous section are Presburger formulas. There are a number of algorithms for testing the satisfiability of arbitrary Presburger formulas [KK67,Coo72,PW93]. The best known upper bound on the performance of an algorithm for verifying Presburger formulas is [Opp78], and we have no reason to believe that our method will provide better worst-case performance. However, our method may be more efficient for many simple cases that arise in our applications.

omega@cs.umd.edu