TR-IIS-06-001    Fulltext

On the Satisfiability of Modular Arithmetic Formula

Bow-Yaw Wang


Modular arithmetic is the underlying integer computation model in conventional programming languages. In this paper, we discuss the satisfiability problem of modular arithmetic formulae over the finite ring Z . Although an upper bound of 22O(n4) can be obtained by solving alternation-free Presburger arithmetic, it is easy to see that the problem is in fact NP-complete. Further, we give an efficient reduction to integer programming with the number of constraints and variables linear in the length of the given linear modular arithmetic formula. For non-linear modular arithmetic formulae, an additional factor of ? is needed. With the advent of efficient integer programming packages, our word-level encoding could be useful to software verification in practice.