Incremental Satisfiability and Implication for UTVPI Constraints

TL;DR

This paper introduces a new incremental algorithm for efficiently checking the satisfiability and implication of UTVPI constraints, which are widely used in various computational fields.

Contribution

It presents a novel incremental algorithm that improves the efficiency of UTVPI constraint satisfaction and implication checking, with optimal time and space complexity.

Findings

Algorithm requires O(m + n log n + p) time

Supports incremental checking of satisfiability and implication

Applicable to large sets of UTVPI constraints

Abstract

Unit two-variable-per-inequality (UTVPI) constraints form one of the largest class of integer constraints which are polynomial time solvable (unless P=NP). There is considerable interest in their use for constraint solving, abstract interpretation, spatial databases, and theorem proving. In this paper we develop a new incremental algorithm for UTVPI constraint satisfaction and implication checking that requires O(m + n log n + p) time and O(n+m+p) space to incrementally check satisfiability of m UTVPI constraints on n variables and check implication of p UTVPI constraints.