Théorème de Courcelle

En algorithmique et en théorie de la complexité, le théorème de Courcelle est le suivant :

Théorème de Courcelle — toute propriété de la logique monadique du second ordre est décidable en temps linéaire dans la classe des graphes avec une largeur arborescente bornée.

C'est un métathéorème, dans le sens où il concerne une classe de problèmes algorithmiques. Le théorème est dû à Bruno Courcelle^[1]^,^[2]^,^[3]^,^[4]. Dans le contexte de ce théorème, un graphe est donné par un ensemble de sommets $S$ et une relation d'adjacence $\mathrm {adj}$ , et la restriction à la logique monadique signifie que la propriété étudiée peut contenir des quantificateurs sur des ensembles de sommets (quantificateurs du second ordre sur des prédicats monadiques), mais pas de quantificateurs sur des ensembles d'arcs (ces quantificateurs du second ordre porteraient sur des prédicats binaires).

Exemple

La propriété, pour un graphe, d'être coloriable en trois couleurs, s'exprime par l'existence de trois ensembles de sommets $R,V,B$ que l'on peut définir par la formule monadique du second ordre suivante

{\begin{aligned}\exists \,R,V,B\,&{\bigl (}\forall s\in S\,(s\in R\lor s\in V\lor s\in B){\bigr )}\land \\&{\bigl (}\forall s,t\,((s\in R\land t\in R)\lor (s\in V\land t\in V)\lor (s\in B\land t\in B))\to \lnot \mathrm {adj} (s,t){\bigr )}.\end{aligned}}

La première partie de la formule assure que les trois ensembles couvrent tous les sommets (tout sommet a une couleur) et la deuxième partie exprime que ces trois ensembles forment un ensemble indépendant. Ainsi, le théorème de Courcelle dit que la 3-coloriabilité d'un graphe en la largeur d'arborescence bornée peut être testée en temps linéaire.

Une des approches de preuve du théorème de Courcelle utilise la construction d'un automate d'arbres ascendant qui réalise la décomposition arborescente du graphe pour le reconnaitre^[3].

Notes et références

↑ Bruno Courcelle, « The monadic second-order logic of graphs. I. Recognizable sets of finite graphs », Information and Computation, vol. 85, n^o 1,‎ 1990, p. 12–75 (DOI 10.1016/0890-5401(90)90043-H, MR 1042649).
↑ (en) Bruno Courcelle, « Graph Structure and Monadic Second-Order Logic: Language Theoretical Aspects », Automata, Languages and Programming, Springer, Berlin, Heidelberg,‎ 7 juillet 2008, p. 1–13 (ISBN 9783540705741, DOI 10.1007/978-3-540-70575-8_1, présentation en ligne).
↑ ^{a et b} Joachim Kneis et Alexander Langer, « A practical approach to Courcelle's theorem », Electronic Notes in Theoretical Computer Science, vol. 251,‎ 2009, p. 65–81 (DOI 10.1016/j.entcs.2009.08.028).
↑ Michael Lampis, « Algorithmic meta-theorems for restrictions of treewidth », dans Mark de Berg et Ulrich Meyer (éditeurs), Proc. 18th Annual European Symposium on Algorithms, Springer, coll. « Lecture Notes in Computer Science » (n^o 6346), 2010 (DOI 10.1007/978-3-642-15775-2_47), p. 549–560 DOI 10.1007/978-3-642-15775-2_47.

Article connexe

Théorème de Robertson-Seymour

Portail de l'informatique théorique

[Courcelle-a-1] Bruno Courcelle, « The monadic second-order logic of graphs. I. Recognizable sets of finite graphs », Information and Computation, vol. 85, n^o 1,‎ 1990, p. 12–75 (DOI 10.1016/0890-5401(90)90043-H, MR 1042649).

[Courcelle-2] (en) Bruno Courcelle, « Graph Structure and Monadic Second-Order Logic: Language Theoretical Aspects », Automata, Languages and Programming, Springer, Berlin, Heidelberg,‎ 7 juillet 2008, p. 1–13 (ISBN 9783540705741, DOI 10.1007/978-3-540-70575-8_1, présentation en ligne).

[Langer-3] {a et b} Joachim Kneis et Alexander Langer, « A practical approach to Courcelle's theorem », Electronic Notes in Theoretical Computer Science, vol. 251,‎ 2009, p. 65–81 (DOI 10.1016/j.entcs.2009.08.028).

[Meyer-4] Michael Lampis, « Algorithmic meta-theorems for restrictions of treewidth », dans Mark de Berg et Ulrich Meyer (éditeurs), Proc. 18th Annual European Symposium on Algorithms, Springer, coll. « Lecture Notes in Computer Science » (n^o 6346), 2010 (DOI 10.1007/978-3-642-15775-2_47), p. 549–560 DOI 10.1007/978-3-642-15775-2_47.

[1]

[2]

[3]

[4]