
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
View/ Open
Type
Communication / ConférenceDate
2020Conference title
61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020Conference date
2020-11Conference city
OnlineConference country
United StatesBook title
61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020Publisher
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
ISBN
978-1-7281-9621-3
Pages
601-612
Metadata
Show full item recordAuthor(s)
Bonnet, EdouardModèles de calcul, Complexité, Combinatoire [MC2]
Kim, Eun Jung

Laboratoire d'analyse et modélisation de systèmes pour l'aide à la décision [LAMSADE]
Thomassé, Stéphan

Modèles de calcul, Complexité, Combinatoire [MC2]
Watrigant, Rémi
Modèles de calcul, Complexité, Combinatoire [MC2]
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 / Keywords
Twin-width; FO model checking; fixed-parameter tractabilityRelated items
Showing items related by title and author.
-
Bonnet, Édouard; Kim, Eun Jung; Thomassé, Stéphan; Watrigant, Rémi (2021) Article accepté pour publication ou publié
-
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