We show a reduction to propositional logic from a Boolean combination of inequalities of the form v
i ≥ v
j + c and v
i > v
j + c, where c is a constant and v
i, v
j are variables of type real or integer. Equalities and uninterpreted functions can be expressed in this logic as well. We
discuss the advantages of using this reduction as compared to competing methods, and present experimental results that support
our claims.
This research was supported in part by the Office of Naval Research (ONR) and the Naval Research Laboratory (NRL) under contract
no. N00014-01-1-0796, and the Gigascale Research Center under contract 98-DT-660. The second author is supported in part by
a National Defense Science and Engineering Graduate Fellowship.