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_{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.