TR-IIS-06-001    Fulltext


On the Satisfiability of Modular Arithmetic Formula

Bow-Yaw Wang

Abstract

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.