A SAT Approach to Branchwidth

A SAT Approach to Branchwidth

Neha Lodha, Sebastian Ordyniak, Stefan Szeider

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Best Sister Conferences. Pages 4894-4898. https://doi.org/10.24963/ijcai.2017/689

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.
Keywords:
Artificial Intelligence: knowledge representation and reasoning
Artificial Intelligence: search and constraint satisfaction
Artificial Intelligence: other