Incremental Satisfiability and Implication for UTVPI Constraints

Unit two-variable-per-inequality (UTVPI) constraints form one of the largest class of integer constraints that are polynomial time solvable (unless P = NP). There is considerable interest in their use for constraint solving, abstract interpretation, spatial database algorithms, and theorem proving. In this paper we develop new incremental algorithms for UTVPI constraint satisfaction and implication checking that require order(m + n log n + p) time and order(n + m + p) space to incrementally check satisfiability of m UTVPI constraints on n variables, and we check the implication of p UTVPI constraints. The algorithms can be straightforwardly extended to create nonincremental implication checking and generation of all (nonredundant) implied constraints, as well as generate minimal unsatisfiable subsets and minimal implicants.