Courcelle's theorem

Courcelle's theorem states that every graph property expressible in monadic second-order logic can be decided in linear time on graphs of bounded treewidth, when the formula and width are fixed.

Monadic second-order logic: A logic that quantifies over individuals and sets of individuals, with relations and predicates. Its formulas specify the graph properties covered by the theorem.
Vertex cover: A set of graph vertices that includes at least one endpoint of every edge. The existence of a vertex cover of a specified size is expressible in monadic second-order logic.
First-order logic: A logic that quantifies over individual objects but not over sets or relations. It is weaker than the monadic second-order language used to express the theorem's properties.
Algorithmic meta-theorem: A general theorem that derives algorithms for many problems from shared logical or structural conditions. Courcelle's result is a landmark example of logic generating algorithms across entire problem families.
Tree decomposition: A representation of a graph as overlapping vertex sets arranged in a tree, satisfying coverage and connectivity conditions. It organizes bounded-treewidth graphs into pieces where formulas can be evaluated.
Dominating set: A set of vertices such that every vertex outside the set has a neighbor inside it. Bounded-treewidth instances admit linear-time decision algorithms through logical definability.
MSO₁: Monadic second-order logic for graphs, allowing quantification over vertices and vertex sets. This graph-logic variant underlies a common formulation of Courcelle's theorem.
Tree automata: Finite-state computational models that recognize languages of finite trees. Automata theory supplies the finite-state machinery behind the theorem's logical algorithm.
Treewidth: A graph parameter measuring how closely a graph resembles a tree, defined through the width of its tree decompositions. A fixed bound on this parameter is the structural condition enabling linear-time evaluation.
Graph coloring: An assignment of colors to graph vertices so that adjacent vertices receive different colors. For fixed numbers of colors, existence of a proper coloring is expressible in the theorem's logic.

Linked from 1 page