Skip to content

Overview

  • Logic preliminaries: first-order logic (FO) and monadic second-order logic (MSO)
  • Expressing graph problems by logical formulas
  • Complexity of model checking for FO and MSO
  • Courcelle’s Theorem for bounded tree-width and its refinements
  • Applications to concrete problems (colouring, Hamiltonicity, vertex cover, etc.)
  • Courcelle’s Theorem for bounded clique-width
  • Graph minors and non-uniform FPT results
  • A first-order meta-theorem (Seese’s theorem)

Idea of Algorithmic Meta-Theorems

Idea:

  • Formulate a problem \(P\) by a logical sentence \(\phi_P\) (of “short” size).
  • Use model checking of \(\phi_P\) on logical structures of bounded width (tree-width, clique-width, …).
  • The running time depends only on the width, \(|\phi_P|\), and the structure size, often yielding FPT algorithms.

Benefits:

  • Quick, easy way to prove that many problems are in FPT.
  • Avoids designing a custom dynamic programming algorithm.

Limitations:

  • The obtained algorithm is typically far from optimal.
  • Problem‑specific algorithms usually give much better running times.

Logic Preliminaries

First‑Order Logic (FO)

Syntax:

  • Vocabulary \(\tau = \{R_1, \dots, R_n\}\) with arities.
  • Atomic formulas: \(x = y\) and \(R(x_1, \dots, x_{ar(R)})\) for \(R \in \tau\).
  • Built using \(\neg, \land, \lor, \rightarrow, \leftrightarrow\) and quantifiers \(\exists x\), \(\forall x\).

Semantics:

  • A \(\tau\)-structure \(\mathcal{A} = \langle A; R_1^{\mathcal{A}}, \dots, R_n^{\mathcal{A}} \rangle\).
  • For a formula \(\phi(x_1,\dots,x_k)\), its interpretation \(\phi(\mathcal{A}) \subseteq A^k\) is defined inductively.
  • \(\mathcal{A} \models \phi(a_1,\dots,a_k)\) means the tuple is in \(\phi(\mathcal{A})\).
  • For a sentence \(\phi\), \(\mathcal{A} \models \phi\) means \(\phi(\mathcal{A}) \neq \emptyset\).

Graph structures:

  • \(\tau_G = \{E/2\}\): symmetric edge relation (simple graphs).
  • \(\tau_{HG} = \{VERT/1, EDGE/1, INC/2\}\): hypergraph representation where vertices and edges are elements, and incidence is a binary relation.

Example: \(k\)-independent set.

\[ \phi_k := \exists x_1 \dots \exists x_k \bigwedge_{1 \le i < j \le k} \big( \neg (x_i = x_j) \land \neg E(x_i, x_j) \big) \]

\(\mathcal{A}_{\tau_G}(G) \models \phi_k \;\iff\; G\) has an independent set of size \(k\).

Complexity:

\(\text{MC(FO)}\) can be solved in time \(O(|\phi| \cdot |A|^w \cdot w)\), where \(w\) is the width (max number of free variables in any subformula). This is not FPT in general.

Monadic Second‑Order Logic (MSO)

Syntax (extends FO):

  • Set variables \(X, Y, \dots\) (unary predicates).
  • New atomic formulas: \(X(x)\).
  • Second‑order quantifiers \(\exists X, \forall X\).

Semantics:

  • \(\phi(\mathcal{A}) \subseteq A^k \times \mathcal{P}(A)^{\ell}\) for \(k\) first‑order and \(\ell\) second‑order variables.
  • \(\mathcal{A} \models \phi(a_1,\dots,a_k, P_1,\dots,P_\ell)\) has the obvious meaning.

Two common variants:

  • MSO\(_1\) (also denoted \(\text{MSO}(\tau_G)\)): allows quantification over sets of vertices only (no edge‑set variables). The vocabulary is essentially \(\{INC/2\}\) where vertices and edges are distinct sorts, but set variables range only over vertex sets.
  • MSO\(_2\) (or \(\text{MSO}(\tau_{HG})\)): allows quantification over both vertex sets and edge sets. It is strictly more expressive.

Example: 3‑colorability (MSO\(_1\) sentence): $$ \exists C_1 \exists C_2 \exists C_3 \Big( \forall x (C_1(x) \lor C_2(x) \lor C_3(x)) \land \forall x \bigwedge_{i<j} \neg(C_i(x) \land C_j(x)) \ \land \forall x \forall y \big( E(x,y) \rightarrow \bigwedge_i \neg(C_i(x) \land C_i(y)) \big) \Big) $$

Expressibility:

  • MSO\(_1\) can express properties like independent set, dominating set, vertex cover, connectivity (with care).
  • MSO\(_2\) can express Hamiltonicity, feedback vertex set, perfect matchings, etc., which are not expressible in MSO\(_1\).

Courcelle’s Theorem for Tree‑Width

Tree‑Width for Structures

A tree decomposition of a \(\tau\)‑structure \(\mathcal{A} = \langle A; \{R^{\mathcal{A}}\} \rangle\) is a pair \(\langle T, \{B_t\}_{t \in T} \rangle\) with a tree \(T\) and bags \(B_t \subseteq A\) satisfying:

(T1) \(A = \bigcup_t B_t\);

(T2) every tuple in every relation \(R^{\mathcal{A}}\) is contained in some bag;

(T3) for each \(a \in A\), the nodes \(\{t \mid a \in B_t\}\) form a connected subtree.

Width: \(\max_t |B_t| - 1\).

Tree‑width \(tw(\mathcal{A})\) is the minimum width over all tree decompositions.

Courcelle’s Theorem (1990)

p*-tw-MC(MSO)

Input: a \(\tau\)‑structure \(\mathcal{A}\), an MSO sentence \(\phi\).
Parameter: \(tw(\mathcal{A}) + |\phi|\).
Question: \(\mathcal{A} \models \phi\)?

Theorem: \(p^*\text{-tw-MC(MSO)} \in \text{FPT}\)

More precisely, there exists a computable, non‑decreasing function \(f\) such that the problem can be decided in time

\[ f(tw(\mathcal{A}), |\phi|) \cdot |\mathcal{A}| + O(\|\mathcal{A}\|) \]

(For graphs with \(n\) vertices: \(f(tw(G), |\phi|) \cdot n\).)

Refinements (Cardinality and Optimization)

Refinement 1 (bounded cardinality):

\(p^*\text{-tw-MC}_{\le}(\text{MSO})\): decide \(\mathcal{A} \models \exists X (\text{card}_{\le m}(X) \land \phi(X))\).

FPT, running time \(f(tw, |\phi|) \cdot |\mathcal{A}| + O(\|\mathcal{A}\|)\).

Application: Vertex Cover, Dominating Set, Independent Set (exists set of size \(\le m\) satisfying \(\phi\)).

Refinement 2 (exact cardinality):

\(p^*\text{-tw-MC}_{=}(\text{MSO})\): \(\mathcal{A} \models \exists X (\text{card}_{= m}(X) \land \phi(X))\).

FPT, time \(f(tw, |\phi|) \cdot |\mathcal{A}|^2 + O(\|\mathcal{A}\|)\).

Optimization version:

Maximise or minimise an affine function \(\alpha(|X_1|,\dots,|X_p|)\) over sets \(X_1,\dots,X_p\) satisfying an MSO formula \(\phi(X_1,\dots,X_p)\).

FPT parameterized by \(tw(G)+|\phi|\), time \(f(tw,|\phi|) \cdot n\).

Applications (via MSO\(_2\) and tree‑width)

Using Courcelle’s theorem (and its refinements) we immediately obtain that the following parameterized problems are in FPT when parameterized by tree‑width:

  • \(p^*\text{-tw-COLORABILITY}\): existence of an \(\ell\)-colouring (MSO\(_1\) sentence).
  • \(p^*\text{-tw-HAMILTONICITY}\): expressed in MSO\(_2\) (using edge sets).
  • \(p^*\text{-tw-VERTEX-COVER}\) (size \(\le \ell\)) — Refinement 1.
  • \(p^*\text{-tw-INDEPENDENT-SET}\) — Refinement 1.
  • \(p^*\text{-tw-FEEDBACK-VERTEX-SET}\) — MSO\(_2\) formula + Refinement 1.
  • \(p^*\text{-tw-CROSSING-NUMBER}\): MSO\(_2\) sentence expressing that the crossing number is \(\le k\) (using topological minor characterisation and induction); parameter \(tw + k\).
  • \(p^*\text{-tw-max-2-edge-colorable-subgraph}\) — optimisation version.

Courcelle’s Theorem for Clique‑Width

Clique‑width (\(clw(G)\)) is another width measure for graphs (defined via \(k\)‑expressions). MSO\(_1\) is the counterpart of MSO(\(\tau_G\)) without edge‑set quantifiers.

Theorem (Courcelle, Makowsky, Rotics 2000):
\(p^*\text{-clw-MC(MSO}_1) \in \text{FPT}\). Given a graph \(G\) and an MSO\(_1\) sentence \(\phi\), the problem can be solved in time \(f(clw(G), |\phi|) \cdot n\). There is also an optimisation version.

Key difference: Only MSO\(_1\)‑expressible properties can be handled by the clique‑width theorem. Properties requiring edge‑set quantification (MSO\(_2\)) are generally not covered.

Examples:

  • \(p^*\text{-clw-VERTEX-COVER} \in \text{FPT}\) (MSO\(_1\) expressible).
  • \(p^*\text{-clw-HAMILTONICITY}\) is not MSO\(_1\) expressible; indeed it is not FPT (unless a collapse) but belongs to XP (Bergougnoux et al. 2020).
  • \(p^*\text{-clw-max-2-edge-colorable-subgraph}\) is open; the property is naturally in MSO\(_2\), not known to be in MSO\(_1\).

Graph Minors and Non‑Uniform FPT

Graph minor: obtained by edge deletions, vertex deletions, and edge contractions.
Minor‑closed class: closed under taking minors.
Graph Minor Theorem (Robertson–Seymour): every minor‑closed class can be characterised by a finite set of excluded minors.

Parameterized minor test: \(p\text{-MINOR} \in \text{FPT}\); deciding whether \(H\) is a minor of \(G\) is FPT parameterized by \(|H|\), running in time \(f(|H|) \cdot |G|^3\).

Consequence: every minor‑closed graph property is decidable in cubic time.

Non‑uniform FPT (nu‑FPT)

A parameterized problem \(\langle Q, \kappa \rangle\) is non‑uniformly FPT if for every \(k \in \mathbb{N}\) there exists an algorithm \(A_k\) deciding instances with parameter \(k\) in time \(\le f(k) \cdot p(|x|)\), but the algorithms for different \(k\) may not be constructed uniformly from \(k\).

Application: Let \(\langle Q, \kappa \rangle\) be a graph problem such that for each \(k\), either \(\{G \in Q : \kappa(G)=k\}\) or \(\{G \notin Q : \kappa(G)=k\}\) is minor‑closed. Then \(\langle Q, \kappa \rangle \in \text{nu-FPT}\).

Examples: \(p\text{-VERTEX-COVER}\) (yes‑instances minor‑closed), \(p\text{-FEEDBACK-VERTEX-SET}\), \(p\text{-DISJOINT-CYCLES}\) (no‑instances minor‑closed).

First‑Order Meta‑Theorem: Seese (1995)

A class \(\mathcal{G}\) of graphs has bounded degree if \(\exists d\) such that \(\Delta(G) \le d\) for all \(G \in \mathcal{G}\).

Theorem (Seese 1995):

For any bounded‑degree class \(\mathcal{G}\), the model checking problem for FO sentences is FPT parameterized by \(|\phi|\).

Time: \(f(|\phi|) \cdot |G|\) (linear in the graph size).

Contrast with the trivial algorithm (time \(O(|\phi| \cdot |A|^w \cdot w)\)) – the degree restriction allows an FPT algorithm via locality techniques.

Summary

  • Courcelle’s theorem and its refinements provide a sweeping meta‑theorem: any MSO‑definable property can be decided in FPT time on structures / graphs of bounded tree‑width.
  • Similar results hold for bounded clique‑width, but only for MSO\(_1\)‑definable properties.
  • Using graph minors, many problems are shown to be in non‑uniform FPT (via excluded minor characterisations).
  • First‑order logic admits its own meta‑theorems under structural restrictions (e.g., bounded degree).
  • Meta‑theorems give quick FPT membership proofs, but the hidden constants are usually enormous; ad‑hoc dynamic programming is often much more practical.

Exercises

For these problems, we use:

  • \(\tau_G\): The standard graph vocabulary where the universe consists of vertices, and there is a binary relation \(E(x,y)\) representing edges.
  • \(\tau_{HG}\): The incidence graph vocabulary where the universe consists of both vertices and edges, and there is a binary relation \(I(v,e)\) indicating that vertex \(v\) is incident to edge \(e\).
  • \(MSO_1\): Monadic Second-Order logic allowing quantification over vertices and sets of vertices.
  • \(MSO_2\): Monadic Second-Order logic allowing quantification over vertices, sets of vertices, edges, and sets of edges.

1. Cycle of length precisely \(k\) (First-Order Logic over \(\tau_G\))

To express that a graph contains a cycle of length exactly \(k\) as a subgraph, we assert the existence of \(k\) distinct vertices that are sequentially adjacent, with the last vertex connecting back to the first.

\[\exists x_1 \exists x_2 \dots \exists x_k \left( \bigwedge_{1 \le i < j \le k} x_i \neq x_j \land \left( \bigwedge_{i=1}^{k-1} E(x_i, x_{i+1}) \right) \land E(x_k, x_1) \right)\]

Note: If you need an induced cycle (meaning no chordal edges exist between the cycle vertices), you would append:

\(\dots \land \bigwedge_{|i-j| \pmod k \neq 1} \neg E(x_i, x_j)\)

2. Dominating set of \(\le k\) elements (\(MSO_1\) over \(\tau_G\))

A set of vertices \(D\) is a dominating set if every vertex in the graph is either in \(D\) or adjacent to a vertex in \(D\). We can express that \(D\) has at most \(k\) elements by asserting there exist \(k\) vertices that cover all members of \(D\).

\[ \exists D \left( \left[ \exists x_1 \dots \exists x_k \forall y (y \in D \rightarrow \bigvee_{i=1}^k y = x_i) \right] \land \forall v \left( v \in D \lor \exists u (u \in D \land E(u, v)) \right) \right) \]

3. Feedback Vertex Set (\(MSO_2\) over \(\tau_{HG}\))

A vertex set \(S\) is a feedback vertex set if its removal leaves the graph acyclic (a forest). Equivalently, every cycle in the graph must contain at least one vertex from \(S\).

In \(MSO_2\), a cycle can be identified by the existence of a non-empty set of edges \(F\) where every vertex incident to \(F\) is connected to at least two edges in \(F\). Therefore, \(feedback(S)\) asserts that no such cycle exists entirely outside of \(S\):

\[ feedback(S) \equiv \neg \exists F \left( \exists e (e \in F) \land \forall e (e \in F \rightarrow \forall v (I(v,e) \rightarrow v \notin S)) \land \forall v (\text{Inc}(v, F) \rightarrow \text{Deg}_{\ge 2}(v, F)) \right) \]

Where the helper predicates are defined as:

  • \(\text{Inc}(v, F) \equiv \exists e (e \in F \land I(v, e))\)
  • \(\text{Deg}_{\ge 2}(v, F) \equiv \exists e_1 \exists e_2 (e_1 \in F \land e_2 \in F \land e_1 \neq e_2 \land I(v, e_1) \land I(v, e_2))\)

4. Connected Graph (\(MSO_1\) over \(\tau_G\))

A graph is connected if there is no way to partition the vertices into two non-empty sets with no edges between them. In other words, for every non-empty proper subset of vertices \(A\), there must be an edge connecting a vertex in \(A\) to a vertex outside of \(A\).

\[ \forall A \left( \left[ \exists x (x \in A) \land \exists y (y \notin A) \right] \rightarrow \exists u \exists v (u \in A \land v \notin A \land E(u, v)) \right) \]

5. Path from \(x\) to \(y\) (\(MSO_2\) over \(\tau_{HG}\))

For a set of edges \(Z\) to form a simple path from \(x\) to \(y\), it must satisfy three conditions:

  1. If \(x = y\), \(Z\) must be empty.
  2. If \(x \neq y\), the endpoints \(x\) and \(y\) must have a degree of exactly 1 within \(Z\), and all other vertices incident to \(Z\) must have a degree of exactly 2.
  3. The edge set \(Z\) must be connected (to prevent isolated cycles detached from the main path).
\[ path(x, y, Z) \equiv (x = y \land \forall e (e \notin Z)) \lor \left( x \neq y \land \text{Deg}_1(x, Z) \land \text{Deg}_1(y, Z) \land \forall v ((\text{Inc}(v, Z) \land v \neq x \land v \neq y) \rightarrow \text{Deg}_2(v, Z)) \land \text{Connected}(Z) \right) \]

Where the helper predicates are defined as:

  • \(\text{Inc}(v, Z) \equiv \exists e (e \in Z \land I(v, e))\)
  • \(\text{Deg}_1(v, Z) \equiv \exists e (e \in Z \land I(v, e) \land \forall e' ((e' \in Z \land I(v, e')) \rightarrow e' = e))\)
  • \(\text{Deg}_2(v, Z) \equiv \exists e_1 \exists e_2 (e_1 \in Z \land e_2 \in Z \land e_1 \neq e_2 \land I(v, e_1) \land I(v, e_2) \land \forall e' ((e' \in Z \land I(v, e')) \rightarrow (e' = e_1 \lor e' = e_2)))\)
  • \(\text{Connected}(Z) \equiv \forall A \left( (\exists u (u \in A \land \text{Inc}(u, Z)) \land \exists v (v \notin A \land \text{Inc}(v, Z))) \rightarrow \exists e (e \in Z \land \exists u' \exists v' (I(u', e) \land I(v', e) \land u' \in A \land v' \notin A)) \right)\)

6. Hamiltonicity (\(MSO_2\) over \(\tau_{HG}\))

A graph is Hamiltonian if it contains a spanning cycle—a cycle that visits every vertex exactly once. This means we can find a subset of edges \(H\) such that every vertex in the graph has a degree of exactly 2 in \(H\), and \(H\) is fully connected across any possible vertex cut.

\[ \exists H \left( \forall v \text{Deg}_2(v, H) \land \forall A \left( [ \exists x (x \in A) \land \exists y (y \notin A) ] \rightarrow \exists e (e \in H \land \exists u \exists v (I(u, e) \land I(v, e) \land u \in A \land v \notin A)) \right) \right) \]

(Note: \(\text{Deg}_2(v, H)\) uses the exact same definition outlined in Problem 5).