English

Elementary first-order model checking for sparse graphs

Logic in Computer Science 2025-05-28 v2 Discrete Mathematics Data Structures and Algorithms Combinatorics Logic

Abstract

It is known that for subgraph-closed graph classes the first-order model checking problem is fixed-parameter tractable if and only if the class is nowhere dense [Grohe, Kreutzer, Siebertz, STOC 2014]. However, the dependency on the formula size is non-elementary, and in fact, this is unavoidable even for the class of all trees [Frick and Grohe, LICS 2002]. On the other hand, it is known that the dependency is elementary for classes of bounded degree [Frick and Grohe, LICS 2002] as well as for classes of bounded pathwidth [Lampis, ICALP 2023]. In this paper we generalise these results and almost completely characterise subgraph-closed graph classes for which the model checking problem is fixed-parameter tractable with an elementary dependency on the formula size. Those are the graph classes for which there exists a number dd such that for every rr, some tree of depth dd and size bounded by an elementary function of rr is avoided as an (r)({\leq} r)-subdivision in all graphs in the class. In particular, this implies that if the class in question excludes a fixed tree as a topological minor, then first-order model checking for graphs in the class is fixed-parameter tractable with an elementary dependency on the formula size.

Keywords

Cite

@article{arxiv.2401.16230,
  title  = {Elementary first-order model checking for sparse graphs},
  author = {Jakub Gajarský and Michał Pilipczuk and Marek Sokołowski and Giannos Stamoulis and Szymon Toruńczyk},
  journal= {arXiv preprint arXiv:2401.16230},
  year   = {2025}
}

Comments

44 pages