Algorithms and Complexity Group
  • People
  • Research
  • Courses
  • Talks
  • Jobs
  • Contact

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]

 

 

News

  • PhD completed by Andre Schidler

    PhD completed by Andre Schidler

    2023-05-31
    Congratulations to André Schidler, who successfully defended his PhD thesis "Scalability for SAT-based combinatorial problem solving" today.   Thanks to …Read More »
  • PhD completed by Vaidyanathan P.R.

    PhD completed by Vaidyanathan P.R.

    2023-05-12
    Congratulations to Vaidyanathan P.R., who successfully defended his PhD thesis Scalable Bayesian Network Structure Learning using SAT-based Methods today. Thanks …Read More »
  • New FWF ESPRIT Postdocs

    New FWF ESPRIT Postdocs

    2022-11-09
    Leroy Chew and Alexis de Colnet just joined the Algorithms and Complexity group as PIs of their own FWF ESPRIT …Read More »
  • Best student paper award at DIAGRAMS 2022

    Best student paper award at DIAGRAMS 2022

    2022-10-01
    Alexander Dobler received the Best Student Paper Award at the 13th International Conference on the Theory and Application of Diagrams …Read More »
  • Robert Ganian promoted to Associate Professor

    Robert Ganian promoted to Associate Professor

    2022-07-01
    Effective as of today, Robert Ganian is promoted to a tenured Associate Professor at the Algorithms and Complexity group. Congratulations, …Read More »

News archive

All news for 2015, 2016, 2017, 2018, 2019, 2020, 2021 and 2022.
TU Wien Informatics
Offenlegung (§25 MedienG) Inhaber der Website ist das Institut für Logic and Computation an der Technischen Universität Wien, 1040 Wien. Die TU Wien distanziert sich von den Inhalten aller extern gelinkten Seiten und übernimmt diesbezüglich keine Haftung. – Disclaimer – Datenschutzerklärung
Log in requires cookies.