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,
K
t
-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].
First-Order LTL Model Checking Using MDGs
