A unit two variable per inequality (UTVPI) constraint is of the form a.x+b.y ≤ 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.
['Shuvendu K. Lahiri', 'Madanlal Musuvathi']
An efficient decision procedure for UTVPI constraints