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