Monadically stable and monadically dependent graph classes: characterizations and algorithmic meta-theorems

Abstract

A graph class is monadically stable if it does not encode the class of all linear orders using first-order logic and vertex colors. This includes many sparse classes like planar graphs, bounded degree, bounded tree-width, and nowhere dense classes, but also dense classes like map graphs. More generally, a class is monadically dependent (also known as monadically NIP) if it does not encode the class of all graphs. This includes the aforementioned monadically stable classes, and also classes of bounded clique- or twin-width. Originating in model theory, monadic stability and dependence have predominantly been studied on infinite structures. In this thesis we combine tools from combinatorics and logic, to develop a theory for monadically stable and monadically dependent classes of finite graphs that is well suited for their algorithmic treatment.

We obtain the following structure/non-structure dichotomy. On the structure side, we characterize monadic stability and monadic dependence by two Ramsey-theoretic properties called flip-flatness and flip-breakability. This gives rise to a larger framework: natural restrictions of flip-flatness and flip-breakability characterize nowhere denseness, bounded clique- and tree-width, and shrub- and tree-depth. On the non-structure side, we characterize monadic stability and monadic dependence by explicitly listing few families of forbidden induced subgraphs.

We show the algorithmic applicability of our characterizations by proving new tractability and hardness results for the first-order model checking problem. Given a graph G and a first-order formula phi, we want to check whether G satisfies phi. It is conjectured that a hereditary graph class admits fixed-parameter tractable model checking if and only if it is monadically dependent. Building on flip-flatness, we prove a game characterization of monadic stability called Flipper game. Using the game tree of the Flipper game as a decomposition of the input graph, we show that first-order model checking is fixed-parameter tractable on every monadically stable graph class. This confirms an important case of the tractability side of the model checking conjecture. Using the forbidden induced subgraph characterization for monadically dependent classes, we completely resolve the hardness side: we show that first-order model checking is AW[*]-hard on every hereditary graph class that is not monadically dependent.