Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 0705.4618

An Improved Tight Closure Algorithm for Integer Octagonal Constraints

Roberto Bagnara·Patricia M. Hill·Enea Zaffanella
View original source ↗Read source document ↗Export metadata ↓

Abstract

Integer octagonal constraints (a.k.a. ``Unit Two Variables Per Inequality'' or ``UTVPI integer constraints'') constitute an interesting class of constraints for the representation and solution of integer problems in the fields of constraint programming and formal analysis and verification of software and hardware systems, since they couple algorithms having polynomial complexity with a relatively good expressive power. The main algorithms required for the manipulation of such constraints are the satisfiability check and the computation of the inferential closure of a set of constraints. The latter is called `tight' closure to mark the difference with the (incomplete) closure algorithm that does not exploit the integrality of the variables. In this paper we present and fully justify an O(n^3) algorithm to compute the tight closure of a set of UTVPI integer constraints.

Explore related subjects

cs.DScs.CGcs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Roberto Bagnara, Patricia M. Hill, Enea Zaffanella. 2007-06-01. An Improved Tight Closure Algorithm for Integer Octagonal Constraints. https://arxiv.org/abs/0705.4618

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Decremental Single-Source Reachability in Planar Digraphs

In this paper we show a new algorithm for the decremental single-source reachability problem in directed planar graphs. It processes any sequence of edge deletions in $O(n\log^2{n}\log\log{n})$ total time and explicitly maintains the set of vertices reachable from a fixed source vertex. Hence, if all edges are eventually deleted, the amortized time of processing each edge deletion is only $O(\log^2 n \log \log n)$, which improves upon a previously known $O(\sqrt{n})$ solution. We also show an algorithm for decremental maintenance of strongly connected components in directed planar graphs with the same total update time. These results constitute the first almost optimal (up to polylogarithmic factors) algorithms for both problems. To the best of our knowledge, these are the first dynamic algorithms with polylogarithmic update times on general directed planar graphs for non-trivial reachability-type problems, for which only polynomial bounds are known in general graphs.

cs.DS↗
arXiv2026

Tight Bounds for Sparsifying Random CSPs

The problem of CSP sparsification asks: for a given CSP instance, what is the sparsest possible reweighting such that for every possible assignment to the instance, the number of satisfied constraints is preserved up to a factor of $1 \pm ε$? We initiate the study of the sparsification of random CSPs. In particular, we consider two natural random models: the $r$-partite model and the uniform model. In the $r$-partite model, CSPs are formed by partitioning the variables into $r$ parts, with constraints selected by randomly picking one vertex out of each part. In the uniform model, $r$ distinct vertices are chosen at random from the pool of variables to form each constraint. In the $r$-partite model, we exhibit a sharp threshold phenomenon. For every predicate $P$, there is an integer $k$ such that a random instance on $n$ vertices and $m$ edges cannot (essentially) be sparsified if $m \le n^k$ and can be sparsified to size $\approx n^k$ if $m \ge n^k$. Here, $k$ corresponds to the largest copy of the AND which can be found within $P$. Furthermore, these sparsifiers are simple, as they can be constructed by i.i.d. sampling of the edges. In the uniform model, the situation is a bit more complex. For every predicate $P$, there is an integer $k$ such that a random instance on $n$ vertices and $m$ edges cannot (essentially) be sparsified if $m \le n^k$ and can sparsified to size $\approx n^k$ if $m \ge n^{k+1}$. However, for some predicates $P$, if $m \in [n^k, n^{k+1}]$, there may or may not be a nontrivial sparsifier. In fact, we show that there are predicates where the sparsifiability of random instances is non-monotone, i.e., as we add more random constraints, the instances become more sparsifiable. We give a precise (efficiently computable) procedure for determining which situation a specific predicate $P$ falls into.

cs.DS↗
arXiv2026

Connectivity-Preserving Important Separators: A Framework for Cut-Uncut Problems

Important separators reduce the search space in parameterized graph separation to a small family that can be enumerated efficiently. We extend this approach to cut-uncut problems, which require separating some vertices while keeping a prescribed terminal set connected. We introduce connectivity-preserving important separators in undirected graphs. These are inclusion-minimal $s,t$-vertex separators that keep the prescribed terminals connected to $s$ and admit no such separator of no greater size whose source component is properly contained in their own. We show that there are at most $2^{O(k^2\log k)}$ such separators of size at most $k$ and give an algorithm that enumerates them in $O(2^{O(k^2\log k)}nT(n,m))$ time. Here $n$ and $m$ denote the numbers of vertices and edges, and $T(n,m)$ is the time to compute a minimum-cardinality $s,t$-separator. We apply this result to Mixed Multiway Cut-Uncut with any fixed number of terminal classes, improving the published $2^{O(p^3\log p)}$ parameter dependence to $2^{O(p^2\log p)}$, where $p$ is the sum of the vertex and edge deletion budgets. For Annotated Odd Cycle Transversal with the additional requirement that an unbounded set of undeletable terminals remain connected, we give a $2^{O(k^2\log k)}(n+m+1)^{O(1)}$-time algorithm. This improves the doubly exponential dependence of a direct treewidth-reduction approach. We also obtain a fixed-parameter tractable algorithm for finding a minimum-cardinality inclusion-minimal $s,t$-separator whose source component contains a prescribed set $A$ and avoids a prescribed set $B$.

cs.DS↗