Incremental satisfiability and implication for UTVPI constraints

Andreas Schutt, Peter J. Stuckey

Research output: Contribution to journalArticleResearchpeer-review

17 Citations (Scopus)

Abstract

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 (m+nlog n+ p) time and (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.

Original languageEnglish
Pages (from-to)514-527
Number of pages14
JournalINFORMS Journal on Computing
Volume22
Issue number4
DOIs
Publication statusPublished - 1 Sep 2010
Externally publishedYes

Keywords

  • Implication
  • Satisfaction
  • Unit two-variable-per-inequality constraints

Cite this