Computing and Certifying Twin-Width Using Logic

doi:10.1145/3769869

Return

Computing and Certifying Twin-Width Using Logic

2026-01-01

PRE

André Schidler *

Stefan Szeider

DOI：10.1145/3769869

Original

Original request for help

Save

Abstract

En 中文

Twin-width is a powerful graph invariant that supports the efficient solution of various NP-hard problems when the input graph has a bounded twin-width. First-order model checking is fixed-parameter tractable on graph classes of bounded twin-width. This work introduces two algorithmic strategies for exact twin-width computation: SAT encodings and a Branch & Bound approach. The SAT encodings explore distinct formulations of twin-width, enhancing performance across different instance types; the Branch & Bound algorithm leverages cached partial solutions for improved efficiency on larger graphs. We propose a verification framework combining these methods and yield verifiable proofs for computed twin-width. Our research contributes conceptual insights into twin-width computation, including new contraction orderings and lower and upper bound techniques that can be of independent interest. We accompany our theoretical developments with a rigorous experimental evaluation.

Keywords:

twin-width

sat