First-Order Model Checking on Monadically Stable Graph Classes

Abstract

A graph class C is called monadically stable if one cannot interpret, in first-order logic, arbitrary large linear orders in colored graphs from 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, Siebertz; J. ACM '17] for nowhere dense classes and of [Dreier, Mählmann, Siebertz; STOC '23] for structurally nowhere dense classes to all monadically stable classes. This result is complemented by a hardness result showing that monadic stability is precisely the dividing line between tractability and intractability of first-order model checking on hereditary classes that are edge-stable: exclude some half-graph as a semi-induced subgraph. Precisely, we prove that for every hereditary graph class C that is edge-stable but not monadically stable, first-order model checking is AW[∗] -hard on C, and W[1]-hard when restricted to existential sentences. This confirms, in the special case of edge-stable classes, an open conjecture that the notion of monadic dependence 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, by combining tools from stability theory and from sparsity theory. We then use this result to construct sparse neighborhood covers for monadically stable graph classes, which provides the missing ingredient for the algorithm of [Dreier, Mählmann, 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 first 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 efficiently interpret the class of all graphs using only existential formulas; this implies W[1]-hardness of model checking already for existential formulas.