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. Dans le contexte de ce théorème, un graphe est donné par un ensemble de sommets et une relation d'adjacence , 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 colorable en trois couleurs, s'exprime par l'existence de trois ensembles de sommets que l'on peut définir par la formule monadique du second ordre suivante
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.
Notes et références
Article connexe Théorème de Robertson-Seymour
Courcelle Catégorie:Théorie de la complexité des algorithmes Catégorie:Algorithme de la théorie des graphes