Twin-width I: tractable FO model checking
Bonnet, Edouard; Kim, Eun Jung; Thomassé, Stéphan; Watrigant, Rémi (2020), Twin-width I: tractable FO model checking, 61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, p. 601-612. 10.1109/FOCS46700.2020.00062
TypeCommunication / Conférence
Conference title61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020
Conference countryUnited States
Book title61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020
MetadataShow full item record
Kim, Eun Jung
Laboratoire d'analyse et modélisation de systèmes pour l'aide à la décision [LAMSADE]
Abstract (EN)Inspired by a width invariant defined on permutations by Guillemot and Marx [SODA '14], we introduce the notion of twin-width on graphs and on matrices. Proper minor-closed classes, bounded rank-width graphs, map graphs, Kt-free unit d-dimensional ball graphs, posets with antichains of bounded size, and proper subclasses of dimension-2 posets all have bounded twin-width. On all these classes (except map graphs without geometric embedding) we show how to compute in polynomial time a sequence of d-contractions, witness that the twin-width is at most d. We show that FO model checking, that is deciding if a given first-order formula ϕ evaluates to true for a given binary structure G on a domain D, is FPT in |ϕ| on classes of bounded twin-width, provided the witness is given. More precisely, being given a d-contraction sequence for G, our algorithm runs in time f(d,|ϕ|)⋅|D| where f is a computable but non-elementary function. We also prove that bounded twin-width is preserved by FO interpretations and transductions (allowing operations such as squaring or complementing a graph). This unifies and significantly extends the knowledge on fixed-parameter tractability of FO model checking on non-monotone classes, such as the FPT algorithm on bounded-width posets by Gajarsk\'y et al. [FOCS '15].
Subjects / KeywordsTwin-width; FO model checking; fixed-parameter tractability
Showing items related by title and author.
Bonamy, Marthe; Bonnet, Edouard; Bousquet, Nicolas; Charbit, Pierre; Giannopoulos, Panos; Kim, Eun Jung; Rzążewski, P.; Sikora, Florian; Thomassé, S. (2021) Article accepté pour publication ou publié