Courcelle's theorem
One meta-theorem that hands you thousands of linear-time algorithms.
The statement
Courcelle's theorem says: any graph property expressible in monadic second-order logic (MSO) can be decided in linear time on graphs of bounded treewidth. You write the property once, in logic, and you get a linear-time algorithm for free on every class of bounded width.
MSO is expressive — it can quantify over sets of vertices and edges, so it captures connectivity, colorability, the existence of a Hamiltonian cycle, and much more. Courcelle's theorem turns 'is this property MSO-definable?' into a sufficient condition for tractability on structured graphs.
Why it matters for the thesis
Courcelle's theorem is the formal reason treewidth deserves to be called a meter: it is not one trick for one problem but a boundary that separates an entire logical class of problems into tractable and intractable by a single graph parameter. The exponent is the width.
Questions
Is Courcelle's theorem practical?
The constants hidden in 'linear time' can be enormous, so it is more a classification tool than a recipe. But it tells you instantly whether a problem is tractable on bounded-width graphs.
What is MSO logic in one line?
First-order logic plus the ability to quantify over sets of vertices and edges — enough to state most natural graph properties.