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 $({\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.
翻译:已知对于子图封闭的图类,一阶模型检测问题具有固定参数可解性当且仅当该图类是无处稠密的[Grohe, Kreutzer, Siebertz, STOC 2014]。然而,其关于公式大小的依赖关系是非初等的,事实上即使对于所有树构成的图类,这种非初等性也是不可避免的[Frick and Grohe, LICS 2002]。另一方面,已知对于有界度图类[Frick and Grohe, LICS 2002]和有界路径宽度图类[Lampis, ICALP 2023],该依赖关系是初等的。本文推广了这些结果,并几乎完整刻画了模型检测问题具有关于公式大小呈初等依赖的固定参数可解性的子图封闭图类。这类图满足:存在某个数$d$,使得对任意$r$,该图类中所有图均避免作为$(\leq r)$-细分出现某个深度为$d$且大小受$r$的初等函数界定的树。特别地,这意味着若所考虑的图类排除某固定树作为拓扑子式,则该图类中图的一阶模型检测问题具有关于公式大小呈初等依赖的固定参数可解性。