Incremental Satisfiability and Implication for UTVPI Constraints

Autor:	Schutt, Andreas, Stuckey, Peter J.
Rok vydání:	2007
Předmět:	Computer Science - Data Structures and Algorithms Computer Science - Computational Geometry Computer Science - Logic in Computer Science F.2.2 G.2.2
Druh dokumentu:	Working Paper
Popis:	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. Comment: 14 pages, 1 figure
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/0709.2961 Zobrazit plný text záznamu View this record from Arxiv