Talks and Poster Presentations (with Proceedings-Entry):
N. Lodha, S. Ordyniak, S. Szeider:
"A SAT Approach to Branchwidth";
Talk: Theory and Application of Satisfiability Testing -- SAT,
- 2016-07-08; in: "Proceedings of SAT 2016: Theory and Applications of Satisfiability Testing - SAT 2016",
Branch decomposition is a prominent method for structurally decomposing a graph, hypergraph or CNF formula. The width of a branch decomposition provides a measure of how well the object is decomposed. For many applications it is crucial to compute a branch decomposition whose width is as small as possible. We propose a SAT approach to finding branch decompositions of small width. The core of our approach is an efficient SAT encoding which determines with a single SAT-call whether a given hypergraph admits a branch decomposition of certain width. For our encoding we developed a novel partition-based characterization of branch decomposition. The encoding size imposes a limit on the size of the given hypergraph. In order to break through this barrier and to scale the SAT approach to larger instances, we developed a new heuristic approach where the SAT encoding is used to locally improve a given candidate decomposition until a fixed-point is reached. This new method scales now to instances with several thousands of vertices and edges.
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.