In:
INFORMS Journal on Computing, Institute for Operations Research and the Management Sciences (INFORMS), Vol. 22, No. 4 ( 2010-11), p. 514-527
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 + n log 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.
Type of Medium:
Online Resource
ISSN:
1091-9856
,
1526-5528
DOI:
10.1287/ijoc.1090.0369
Language:
English
Publisher:
Institute for Operations Research and the Management Sciences (INFORMS)
Publication Date:
2010
detail.hit.zdb_id:
2070411-2
detail.hit.zdb_id:
2004082-9
SSG:
3,2
