Incremental Satisfiability and Implication for UTVPI Constraints

Thumbnail Image

Date

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Description

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.
14 pages, 1 figure

Keywords

Data Structures and Algorithms, Computational Geometry, Logic in Computer Science, F.2.2; G.2.2

Citation

URI

http://salesiana.dossiersoluciones.com/handle/123456789/138333

Consulte el texto completo en el siguiente enlace:

https://arxiv.org/abs/0709.2961
 http://arxiv.org/abs/0709.2961

Collections

arXiv