A Combinatorial Certifying Algorithm for Linear Feasibility in UTVPI Constraints

摘要

In this paper, we discuss a new combinatorial certifying algorithm for the problem of checking linear feasibility in Unit Two Variable Per Inequality (UTVPI) constraints. A UTVPI constraint has at most two non-zero variables and the coefficients of the non-zero variables belong to the set {+ 1, -1}. These constraints occur in a number of application domains, including but not limited to program verification, abstract interpretation, and operations research. The proposed algorithm runs in O(m center dot n) time and O(m + n) space on a UTVPI system with n variables and m constraints. Observe that these resource bounds match the bounds of the fastest strongly polynomial algorithm for difference constraints. Inasmuch as UTVPI constraints subsume difference constraints, it is clear that the resource requirements of our algorithm are optimal. Additionally, our algorithm is certifying, in that it produces a satisfying assignment when presented with a feasible instance, and a refutation, otherwise. At the heart of our algorithm is a new constraint network representation for UTVPI constraints.