Incremental Satisfiability and Implication for UTVPI Constraints
| dc.creator | Schutt, Andreas | |
| dc.creator | Stuckey, Peter J. | |
| dc.date | 2007-09-19 | |
| dc.date.accessioned | 2026-07-07T08:30:48Z | |
| dc.date.available | 2026-07-07T08:30:48Z | |
| dc.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. | |
| dc.description | 14 pages, 1 figure | |
| dc.identifier | https://arxiv.org/abs/0709.2961 | |
| dc.identifier | http://arxiv.org/abs/0709.2961 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/138333 | |
| dc.subject | Data Structures and Algorithms | |
| dc.subject | Computational Geometry | |
| dc.subject | Logic in Computer Science | |
| dc.subject | F.2.2; G.2.2 | |
| dc.title | Incremental Satisfiability and Implication for UTVPI Constraints | |
| dc.type | text |