Incremental Satisfiability and Implication for UTVPI Constraints

use for constraint solving, abstract interpretation, spatial databases, and theorem proving. In this paper we develop new incremental algorithms for UTVPI constraint satisfaction and implication checking that require 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. The algorithms can be straightforwardly extended to create non-incremental implication checking and generation of all (non-redundant) implied constraints, as well as generate minimal unsatisfiable subsets and minimal implicants. Key words: unit two variable per inequality constraints; satisfaction; implication

• Type: Journal
• Year: 2010
• Where: INFORMS
• Authors: Andreas Schutt, Peter J. Stuckey
• Keywords: INFORMS 2010, Minimal Unsatisfiable Subsets, UTVPI Constraint Satisfaction, Utvpi Constraints