TR-IIS-06-001    Fulltext

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_2ω . Although an upper bound of 2^2O(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.