BranchLIS: a tool for computing branch decompositions of graphs and hypergraphs with SAT-based local improvement

Various decomposition techniques have proven to be useful for efficient solving of many hard problems, e.g., the #P-complete problem of counting models for a propositional formula, albeit there is an exponential dependency on the width measures that are associated with these decompositions. Therefore, it is of interest to obtain decompositions of small width. There are various exact methods, approximations, and heuristics which allow us to compute the decompositions. The exact methods can be only used for very small problem instances and are generally slow, whereas the approximations and heuristic methods are usually fast but far off from the optimal widths. SAT-based local improvements try to use the speed of the heuristics and use exact methods to get better upper bounds for a given width parameter.

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. We propose BranchLIS, a SAT approach to finding branch decompositions of small width.

SAT Encoding for Branchwidth

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 a certain width. For our encoding, we developed a novel partition-based characterization of branch decomposition. Using this encoding we can obtain optimal widths for small instances as well as an upper bound for larger instances.

SAT-based Local Improvement for Branchwidth

The encoding size imposes a limit on the size of the input hypergraph. In order to break through this barrier and to scale the SAT approach to larger instances, we developed a new heuristic approach (BranchLIS) 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.

Downloads

The source code can be downloaded from GitHub. BranchLIS is written in Python2.7 and requires Python library Networkx. BranchLIS can also be used for visualizing the graphs and their decomposition (requires matplotlib).

Team

Neha Lodha, Sebastian Ordyniak, Stefan Szeider

Developer

Neha Lodha

Publications

2 results

2017
[2]	A SAT Approach to Branchwidth Neha Lodha, Sebastian Ordyniak, Stefan Szeider Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017 (Carles Sierra, ed.), pages 4894–4898, 2017, ijcai.org. Note: Sister Conference Best Paper Track [bibtex] [pdf] [doi]
2016
[1]	A SAT Approach to Branchwidth Neha Lodha, Sebastian Ordyniak, Stefan Szeider Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings (Nadia Creignou, Daniel Le Berre, eds.), volume 9710 of Lecture Notes in Computer Science, pages 179–195, 2016, Springer Verlag. [bibtex] [doi]