Abstract
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 develop a
novel partition-based characterization of branch decompositions. 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 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