2024/01/29 by Jakub Gajarský, Gajarský, Jakub, Michał Pilipczuk +7
Computer Science · Engineering · #Combinatorics (math.CO) #Data Structures and Algorithms (cs.DS) #Discrete Mathematics (cs.DM) #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic in Computer Science (cs.LO) #Radiation Effects in Electronics #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.2401.16230
openalex publication_date 2024/01/29 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.