[Back]

N. Lodha, S. Ordyniak, S. Szeider:
"A SAT Approach to Branchwidth";
Talk: 26th International Joint Conference on Artificial Intelligence (IJCAI 2017), Melbourne, Australia (invited); 2017-08-19 - 2017-08-25; in: "Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI 2017)", (2017), 4894 - 4898.

Branch decomposition is a prominent method for structurally
decomposing a graph, hypergraph or CNF formula. The width of a branch
decomposi- tion 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 develop a novel
partition-based characterization of branch de- compositions. 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 develop a new heuristic ap- proach 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.