Twin-width I: tractable FO model checking
Bonnet, Édouard; Kim, Eun Jung; Thomassé, Stéphan; Watrigant, Rémi (2021), Twin-width I: tractable FO model checking, Journal of the ACM (JACM), 69, 1, p. 1–46. 10.1145/3486655
Type
Article accepté pour publication ou publiéExternal document link
https://hal.archives-ouvertes.fr/hal-03750975Date
2021Journal name
Journal of the ACM (JACM)Volume
69Number
1Publisher
ACM - Association for Computing Machinery
Pages
1–46
Publication identifier
Metadata
Show full item recordAuthor(s)
Bonnet, ÉdouardLaboratoire de l'Informatique du Parallélisme [LIP]
Kim, Eun Jung
Laboratoire d'analyse et modélisation de systèmes pour l'aide à la décision [LAMSADE]
Thomassé, Stéphan
Laboratoire de l'Informatique du Parallélisme [LIP]
Watrigant, Rémi
Laboratoire de l'Informatique du Parallélisme [LIP]
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 under 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ý et al. [FOCS '15].Subjects / Keywords
Twin-width, FO model checking, Fixed-parameter tractability, Twin-widthRelated items
Showing items related by title and author.
-
Bonnet, Edouard; Kim, Eun Jung; Thomassé, Stéphan; Watrigant, Rémi (2020) Communication / Conférence
-
Bonnet, Edouard; Geniet, Colin; Kim, Eun Jung; Thomassé, Stéphan; Watrigant, Rémi (2021) Communication / Conférence
-
Bonnet, Edouard; Kim, Eun Jung; Reinald, Amadeus; Thomassé, Stéphan; Watrigant, Rémi (2021) Communication / Conférence
-
Bonnet, Edouard; Geniet, Colin; Kim, Eun Jung; Thomassé, Stéphan; Watrigant, Rémi (2021) Communication / Conférence
-
Bonnet, Edouard; Kim, Eun Jung; Reinald, Amadeus; Thomassé, Stéphan (2022) Communication / Conférence