Modular difference logic is hard

Nikolaj Bjørner, Andreas Blass, Yuri Gurevich +1

In connection with machine arithmetic, we are interested in systems of constraints of the form x + k \leq y + k'. Over integers, the satisfiability problem for such systems is poly…