一句话：几乎完整刻画了子图封闭图类上一阶模型检测何时以初等依赖于公式大小的固定参数算法可解，并证明排除固定树作为拓扑子式即可。
已知对子图封闭图类，一阶模型检测是固定参数可解的当且仅当该类 nowhere dense，但对公式大小的依赖一般是非初等的，即使树类也不可避免。本文研究何时该依赖可降为初等，推广了有界度与有界路径宽度的结果。作者给出几乎完整的刻画：子图封闭图类具有初等依赖的 FPT 一阶模型检测，当且仅当存在深度 d，使得对每个 r，某棵深度为 d 且大小不超过 r 的初等函数的树，不在该类所有图中作为 (≤r)-subdivision 出现。由此推出，若图类排除某棵固定树作为拓扑子式，则其上的一阶模型检测是固定参数可解的，且对公式大小的依赖为初等。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{abs-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},
booktitle = {LICS},
year = {2024},
doi = {10.1145/3661814.3662094}
}