2021/10/12 by André Schidler, Stefan Szeider, Schidler, André +1 · 1 citation
Computer Science · #Combinatorics (math.CO) #Data Structures and Algorithms (cs.DS) #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic in Computer Science (cs.LO) #VLSI and Analog Circuit Testing #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2110.06146
openalex publication_date 2021/10/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The graph invariant twin-width was recently introduced by Bonnet, Kim, Thomassé, and Watrigan. Problems expressible in first-order logic, which includes 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. Computing such a certificate, however, is an intrinsic problem, for which no nontrivial algorithm is known. In this paper, we propose the first practical approach for computing the twin-width of graphs together with the corresponding certificate. We propose efficient SAT-encodings that rely on a characterization of twin-width based on elimination sequences. This allows us to determine the twin-width of many famous graphs with previously unknown twin-width. We utilize our encodings to identify the smallest graphs for a given twin-width bound d ∈ \1,…,4\.