Share this page
Share this page E-mail this page Print this page RSS feeds
Home > Publications > An Efficient Decision Procedure for UTVPI Constraints
An Efficient Decision Procedure for UTVPI Constraints

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.

tr-2005-67.pdf
PDF file

In: Frontiers of Combining Systems (FroCos '05)

Publisher: Springer Verlag
All copyrights reserved by Springer 2007.

Details

Type: Inproceedings
Pages: 0
Number: MSR-TR-2005-67
Institution: Microsoft Research