Twin-width I: tractable FO model checking

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ý et al. [FOCS '15].

Authors

• Édouard Bonnet
• Eun Jung Kim 0002
• Stéphan Thomassé
• Rémi Watrigant

Keywords

• Model checking
• Lips
• Computational modeling
• Dynamic programming
• Computer science
• Periodic structures
• Mathematics
• Small Class
• Functional Graph
• Binary Structure
• Guillemot
• Path Length
• Error Values
• Linear Time
• Linear Order
• Vertices
• Red Edge
• Simple Graph
• Binary Relation
• Set Of Graphs
• Free Variables
• Permutation Matrix
• Hypergraph
• Planar Graphs
• Density Classes
• Class Of Graphs
• Induced Subgraph
• Hamiltonian Path
• Black Edges
• Adjacent Vertices
• Linear-time Algorithm
• Block Diagonal
• First-order Logic
• Depth-first
• Twin-width
• FO model checking
• fixed-parameter tractability