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 \in \-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(n^2.m) time and O(n^2) space algorithm based on transitive closure. Our decision procedure is also equality generating, proof generating, and model generating.

PDF file

In  Frontiers of Combining Systems (FroCos '05)

Publisher  Springer Verlag
All copyrights reserved by Springer 2007.

Details