Incremental Satisfiability and Implication for UTVPI Constraints
Data Structures and Algorithms
2007-09-20 v1 Computational Geometry
Logic in Computer Science
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.
Cite
@article{arxiv.0709.2961,
title = {Incremental Satisfiability and Implication for UTVPI Constraints},
author = {Andreas Schutt and Peter J. Stuckey},
journal= {arXiv preprint arXiv:0709.2961},
year = {2007}
}
Comments
14 pages, 1 figure