zbMATH — the first resource for mathematics

Incremental satisfiability and implication for UTVPI constraints. (English) Zbl 1243.90141
Summary: Unit two-variable-per-inequality (UTVPI) constraints form one of the largest classes 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 \(\mathcal O(m+n\log n+p)\) time and \(\mathcal O(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.

90C10 Integer programming
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68W40 Analysis of algorithms
Full Text: DOI