[Back]

N. Lodha, S. Ordyniak, S. Szeider:
"A SAT Approach to Branchwidth";
Talk: Theory and Application of Satisfiability Testing -- SAT, Bordeaux, France; 2016-07-05 - 2016-07-08; in: "Proceedings of SAT 2016: Theory and Applications of Satisfiability Testing - SAT 2016", (2016), ISBN: 978-3-319-40969-6; 179 - 195.

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.

http://publik.tuwien.ac.at/files/publik_254656.pdf