A graph class $\mathscr{C}$ is called monadically stable if one cannot interpret, in first-order logic, arbitrary large linear orders in colored graphs from $\mathscr{C}$. We prove that the model checking problem for first-order logic is fixed-parameter tractable on every monadically stable graph class. This extends the results of [Grohe, Kreutzer, and Siebertz; J. ACM '17] for nowhere dense classes and of [Dreier, M\"ahlmann, and Siebertz; STOC '23] for structurally nowhere dense classes to all monadically stable classes. As a complementary hardness result, we prove that for every hereditary graph class $\mathscr{C}$ that is edge-stable (excludes some half-graph as a semi-induced subgraph) but not monadically stable, first-order model checking is $\mathrm{AW}[*]$-hard on $\mathscr{C}$, and $\mathrm{W}[1]$-hard when restricted to existential sentences. This confirms, in the special case of edge-stable classes, an on-going conjecture that the notion of monadic NIP delimits the tractability of first-order model checking on hereditary classes of graphs. For our tractability result, we first prove that monadically stable graph classes have almost linear neighborhood complexity. Using this, we construct sparse neighborhood covers for monadically stable classes, which provides the missing ingredient for the algorithm of [Dreier, M\"ahlmann, and Siebertz; STOC '23]. The key component of this construction is the usage of orders with low crossing number [Welzl; SoCG '88], a tool from the area of range queries. For our hardness result, we prove a new characterization of monadically stable graph classes in terms of forbidden induced subgraphs. We then use this characterization to show that in hereditary classes that are edge-stable but not monadically stable, one can effectively interpret the class of all graphs using only existential formulas.

翻译：图类 $\mathscr{C}$ 称为单演稳定的，如果无法用一阶逻辑在 $\mathscr{C}$ 的着色图中解释任意大的线性序。我们证明，在每个单演稳定图类上，一阶逻辑的模型检测问题是固定参数可解的。该结果将 [Grohe, Kreutzer, and Siebertz; J. ACM '17] 关于无处稠密类的结果以及 [Dreier, M\"ahlmann, and Siebertz; STOC '23] 关于结构无处稠密类的结果推广至所有单演稳定类。作为互补的困难性结果，我们证明：对于每个满足边稳定（排除某些半图作为半诱导子图）但非单演稳定的遗传图类 $\mathscr{C}$，一阶模型检测在 $\mathscr{C}$ 上是 $\mathrm{AW}[*]$-困难的，且当其限制于存在句时是 $\mathrm{W}[1]$-困难的。这证实了在边稳定类的特殊情形下，一个持续猜想：即单演 NIP 概念界定了遗传图类上一阶模型检测的可解性。关于可解性结果，我们首先证明单演稳定图类具有近线性邻域复杂度。利用这一性质，我们为单演稳定类构造了稀疏邻域覆盖，这补全了 [Dreier, M\"ahlmann, and Siebertz; STOC '23] 算法缺失的关键要素。该构造的核心组件是使用低交叉数序 [Welzl; SoCG '88]——一种来自范围查询领域的工具。关于困难性结果，我们以禁用诱导子图的形式给出了单演稳定图类的新刻画。随后利用该刻画证明：在满足边稳定但非单演稳定的遗传类中，可以仅使用存在公式有效解释所有图构成的类。