Modular difference logic is hard

In connection with machine arithmetic, we are interested in systems of constraints of the form x + k y + k . 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.

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Nikolaj Bjørner, Andreas Blass, Yuri Gurevich, Madan Musuvathi
• Keywords: CORR 2008, Education, Machine Arithmetic, Polynomial Time, Satisfiability Problem