An Efficient Decision Procedure for UTVPI Constraints

Shuvendu Lahiri and Madanlal Musuvathi


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.


Publication typeInproceedings
Published inFrontiers of Combining Systems (FroCos '05)
InstitutionMicrosoft Research
PublisherSpringer Verlag
> Publications > An Efficient Decision Procedure for UTVPI Constraints