Computing Twin-width with SAT and Branch & Bound

Computing Twin-width with SAT and Branch & Bound

André Schidler, Stefan Szeider

Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence
Main Track. Pages 2013-2021. https://doi.org/10.24963/ijcai.2023/224

The graph width-measure twin-width recently attracted great attention because of its solving power and generality. Many prominent NP-hard problems are tractable on graphs of bounded twin-width if a certificate for the twin-width bound is provided as an input. Bounded twin-width subsumes other prominent structural restrictions such as bounded treewidth and bounded rank-width. Computing such a certificate is NP-hard itself, already for twin-width 4, and the only known implemented algorithm for twin-width computation is based on a SAT encoding. In this paper, we propose two new algorithmic approaches for computing twin-width that significantly improve the state of the art. Firstly, we develop a SAT encoding that is far more compact than the known encoding and consequently scales to larger graphs. Secondly, we propose a new Branch & Bound algorithm for twin-width that, on many graphs, is significantly faster than the SAT encoding. It utilizes a sophisticated caching system for partial solutions. Both algorithmic approaches are based on new conceptual insights into twin-width computation, including the reordering of contractions.
Keywords:
Constraint Satisfaction and Optimization: CSO: Constraint programming
Constraint Satisfaction and Optimization: CSO: Applications
Constraint Satisfaction and Optimization: CSO: Constraint satisfaction