[Zurück]

N. Lodha, S. Ordyniak, S. Szeider:
"A SAT Approach to Branchwidth";
ACM Transactions on Computational Logic, 20 (2019), 3; S. 1 - 24.

Branch decomposition is a prominent method for structurally decomposing a graph, a hypergraph, or a propositional
formula in conjunctive normal form. The width of a branch decomposition provides a measure of
how well the object is decomposed. For many applications, it is crucial to computing a branch decomposition
whose width is as small as possible. We propose an approach based on Boolean Satisfiability (SAT) to
finding branch decompositions of small width. The core of our approach is an efficient SAT encoding that
determines with a single SAT-call whether a given hypergraph admits a branch decomposition of a certain
width. For our encoding, we propose a natural partition-based characterization of branch decompositions.
The encoding size imposes a limit on the size of the given hypergraph. 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 SAT-based
local improvement method scales now to instances with several thousands of vertices and edges.

http://dx.doi.org/10.1145/3326159

https://publik.tuwien.ac.at/files/publik_284438.pdf