@techreport{lahiri2005an,
author = {Lahiri, Shuvendu and Musuvathi, Madan},
title = {An Efficient Decision Procedure for UTVPI Constraints},
year = {2005},
month = {May},
abstract = {A unit two variable per inequality (UTVPI) constraint is of the form a.x+b.y łeq d where x and y are integer variables, the coefficients a,b ∈ \-1,0,1$ and the bound d is an integer constant. This paper presents an efficient decision procedure for UTVPI constraints. Given m such constraints over n variables, the procedure checks the satisfiability of the constraints in O(n.m) time and O(n+m) space. This improves upon the previously known O(n2.m) time and O(n2) space algorithm based on transitive closure. Our decision procedure is also equality generating, proof generating, and model generating.},
publisher = {Springer Verlag},
url = {http://approjects.co.za/?big=en-us/research/publication/an-efficient-decision-procedure-for-utvpi-constraints/},
edition = {Frontiers of Combining Systems (FroCos '05)},
number = {MSR-TR-2005-67},
note = {Frontiers of Combining Systems (FroCos '05)},
}