Twin-width and Limits of Tractability of FO Model Checking on Geometric Graphs

TL;DR

This paper characterizes when hereditary classes of circle and permutation graphs have fixed-parameter tractable FO model checking, using twin-width to extend known results and identify precise structural conditions.

Contribution

It extends the characterization of tractable FO model checking from permutation graphs to circle graphs and interval graphs using twin-width, providing exact excluded-subgraph criteria.

Findings

FO model checking is FPT for hereditary classes excluding some permutation graph.

Characterization of bounded twin-width subclasses via excluded subgraphs.

Extension of twin-width concepts to bounded perturbations of graph classes.

Abstract

The complexity of the problem of deciding properties expressible in FO logic on graphs -- the FO model checking problem (parameterized by the respective FO formula), is well-understood on so-called sparse graph classes, but much less understood on hereditary dense graph classes. Regarding the latter, a recent concept of twin-width [Bonnet et al., FOCS 2020] appears to be very useful. For instance, the question of these authors [CGTA 2019] about where is the exact limit of fixed-parameter tractability of FO model checking on permutation graphs has been answered by Bonnet et al. in 2020 quite easily, using the newly introduced twin-width. We prove that such exact characterization of hereditary subclasses with tractable FO model checking naturally extends from permutation to circle graphs (the intersection graphs of chords in a circle). Namely, we prove that under usual complexity assumptions, FO model checking of a hereditary class of circle graphs is in FPT if and only if the class excludes some permutation graph. We also prove a similar excluded-subgraphs characterization for hereditary classes of interval graphs with FO model checking in FPT, which concludes the line a research of interval classes with tractable FO model checking started in [Ganian et al., ICALP 2013]. The mathematical side of the presented characterizations -- about when subclasses of the classes of circle and permutation graphs have bounded twin-width, moreover extends to so-called bounded perturbations of these classes.