Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
N. Lodha, S. Ordyniak, S. Szeider:
"A SAT Approach to Branchwidth";
Vortrag: Theory and Application of Satisfiability Testing -- SAT,
Bordeaux, France;
05.07.2016
- 08.07.2016; in: "Proceedings of SAT 2016: Theory and Applications of Satisfiability Testing - SAT 2016",
(2016),
ISBN: 978-3-319-40969-6;
S. 179
- 195.
Kurzfassung englisch:
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.
Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/publik_254656.pdf
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.