Théorème de Courcelle

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

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 ${\displaystyle S}$ et une relation d'adjacence ${\displaystyle \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).

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

${\displaystyle {\begin{aligned}\exists \,R,V,B\,&{\bigl (}\forall 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].

• Théorème de Robertson-Seymour

• Portail de l'informatique théorique