zbMATH — the first resource for mathematics

An efficient decision procedure for UTVPI constraints. (English) Zbl 1171.68715
Gramlich, Bernhard (ed.), Frontiers of combining systems. 5th international workshop, FroCos 2005, Vienna, Austria, September 19–21, 2005. Proceedings. Berlin: Springer (ISBN 3-540-29051-6/pbk). Lecture Notes in Computer Science 3717. Lecture Notes in Artificial Intelligence, 168-183 (2005).
Summary: A unit two variable per inequality (UTVPI) constraint is of the form \(a\cdot x + b\cdot y \leq 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\cdot m)\) time and \(O(n+m)\) space. This improves upon the previously known \(O(n^{2}\cdot m)\) time and \(O(n^{2})\) space algorithm based on transitive closure. Our decision procedure is also equality generating, proof generating, and model generating.
For the entire collection see [Zbl 1089.68010].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q25 Analysis of algorithms and problem complexity
Full Text: DOI