First-Order Model Checking on Monadically Stable Graph Classes

A graph class C is monadically stable if one cannot interpret arbitrary long linear orders in colored graphs from C using any fixed first-order interpretation. We prove that on any monadically stable class, the model-checking for first-order logic is fixed-parameter tractable, that is, can be solved in time f(|phi|) * n^c, which culminates a 7 year work on this conjecture. The final piece of the puzzle involves construction of sparse neighborhood covers using Welzl orders, a tool borrowed from discrete geometry. This is a joint work with Jan Dreier, Ioannis Eleftheriadis, Nikolas Mählmann, Rose McCarty, and Szymon Toruńczyk.