Modular difference logic is hard

Nikolaj Bjorner, Andreas Blass, Yuri Gurevich, and Madanlal Musuvathi

Abstract

In connection with machine arithmetic, we are interested in systems of constraints of the form x + k ≤ y + l. Over integers, the satisfiability problem for such systems is polynomial time. The problem becomes NP complete if we restrict attention to the residues for a fixed modulus N.

Details

Publication typeTechReport
NumberMSR-TR-2008-140
Pages8
InstitutionMicrosoft Research
> Publications > Modular difference logic is hard