Algorithmic Meta-Theorems

Instructor: Jan Dreier

These are the slides and videos from the first time I held this course in 2021. In the first block, we define treewidth (part 2), and show that all problems definable in monadic second-order logic can be solved efficiently on graph classes with bounded treewidth (part 3 and 4). In the second block, we show that all problems definable in first-order logic can be solved efficiently on more and more general sparse graphs. After proving the result for graph classes with bounded degree and bounded local treewidth (part 5), we introduce the notions of bounded expansion and nowhere dense graph classes (part 6) and solve all problems definable in first-order logic on bounded expansion graph classes (part 7 and 8). We close with a short overview over dense graph classes (part 9).

Slides

Part 1: Introduction
Part 2: Treewidth
Part 3: Courcelle's Theorem I
Part 4: Courcelle's Theorem II
Part 5: Gaifman Locality
Part 6: Sparsity Definitions
Part 7: Model-Checking
Part 8 and 9: Dense Graphs

Recordings

Part 1: Introduction

We outline the course, discuss organizational matters and get a first intuition on how graph structure can help solve hard problems.

Part 2: Treewidth

We introduce treewidth and solve independent set via dynamic programming. We also get an overview over basic logical notation and monadic second order (MSO) logic.

Part 3: Courcelle's Theorem I

We present Courcelle's theorem and and its extensions and discuss what can be expressed in MSO1 and MSO2. We start proving Courcelle's theorem using the logical decomposition result by Feferman and Vaught.

Part 4: Courcelle's Theorem II

We finish the proof of Courcelle's theorem and briefly mention cliquewidth. Then we change topics and motivate sparse graph classes and first order (FO) logic.

Part 5: Gaifman Locality

We analyze the expressiveness of FO logic using Ehrenfeucht-Fraïssé games. We introduce the locality of FO logic (Gaifman's Theorem) and show how it can be used to evaluate FO formulas on graph classes with bounded degree or locally bounded treewidth.

Part 6: Sparsity Definitions

We introduce bounded expansion and nowhere dense graph classes via shallow minors and argue why these are the right notions of sparsity. We show how they generalize other sparsity measures.

Part 7: Model-Checking I

We present the main algorithmic results for sparse graphs: At first, we use low treedepth colorings to evaluate existential FO formulas on bounded expansion graph classes. We then introduce quantifier-elimination to evaluate FO formulas on bounded expansion classes.

Part 8: Model-Checking II

We finish the proof that one can efficiently evaluate FO formulas on bounded expansion classes, and show that there are no tractable sparsity measures beyond nowhere dense graph classes.

Part 9: Dense Graphs

The lecture ends with an outlook on algorithmically tractable dense graph classes. We introduce transductions, twinwidth and pose central open questions.