Elementary first-order model checking for sparse graphs
Jakub Gajarský, Michal Pilipczuk, Marek Sokolowski, Giannos Stamoulis, Szymon Torunczyk
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 d such that for every r, some tree of depth d and size bounded by an elementary function of r is avoided as an (≤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.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 3bc61cf3-7a37-4ca5-8dbc-1226982a95beCited by top-tier papers2
- 3D-grids are not transducible from planar graphsJakub Gajarský, Michal Pilipczuk, Filip PokrývkaLICS 2025 · 2 citations
- Fine-Grained Bounds for Courcelle's TheoremDaniel Lokshtanov, Fahad Panolan, Saket Saurabh, Jie Xue et al.STOC 2026
Builds on6
- Twin-width I: tractable FO model checkingÉdouard Bonnet, Eun Jung Kim, Stéphan Thomassé, Rémi WatrigantFOCS 2020 · 82 citations
- Stable graphs of bounded twin-widthJakub Gajarský, Michal Pilipczuk, Szymon TorunczykLICS 2022 · 16 citations
- First-Order Model Checking on Structurally Sparse Graph ClassesJan Dreier, Nikolas Mählmann, Sebastian SiebertzSTOC 2023 · 13 citations
- Flip-width: Cops and Robber on dense graphsSzymon TorunczykFOCS 2023 · 9 citations
- Model Checking on Interpretations of Classes of Bounded Local CliquewidthÉdouard Bonnet, Jan Dreier, Jakub Gajarský, Stephan Kreutzer et al.LICS 2022 · 7 citations
Related papers
- Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph ClassesNicole Schirrmacher, Sebastian Siebertz, Giannos Stamoulis, Dimitrios M. Thilikos et al.LICS 2024 · 3 citations
- First-Order Model Checking on Monadically Stable Graph ClassesJan Dreier, Ioannis Eleftheriadis, Nikolas Mählmann, Rose McCarty et al.FOCS 2024 · 8 citations
- Flip-Breakability: A Combinatorial Dichotomy for Monadically Dependent Graph ClassesJan Dreier, Nikolas Mählmann, Szymon TorunczykSTOC 2024 · 8 citations
- Model Checking for Low Monodimensionality Fragments of CMSO on Topological-Minor-Free Graph ClassesIgnasi Sau, Nicole Schirrmacher, Sebastian Siebertz, Giannos Stamoulis et al.LICS 2026
- Efficiently Finding and Counting Patterns with Distance Constraints in Sparse GraphsDaniel Lokshtanov, Fahad Panolan, Saket Saurabh, Jie Xue et al.STOC 2025 · 2 citations
