# Logique des graphes

Dans les domaines mathématiques de la théorie des graphes et de la théorie des modèles finis, la logique des graphes traite de la spécification formelle de propriétés de graphe en utilisant des propositions de la logique mathématique. Il existe plusieurs variantes suivant les types d'opérations logiques qui peuvent être utilisées dans ces propositions. La logique du premier ordre des graphes concerne les propositions dans lesquelles les variables et les prédicats concernent les sommets et les arêtes individuels d'un graphe, tandis que la logique monadique de graphe du second ordre permet une quantification sur des ensembles de sommets ou d'arêtes. Les logiques basées sur les plus petits opérateurs de point fixe permettent des prédicats plus généraux sur des tuples de sommets, mais ces prédicats ne peuvent être construits qu'en utilisant des opérateurs de point fixe, ce qui limite leur puissance.
Une proposition $S$ peut être vraie pour certains graphes et fausse pour d'autres; un graphe $G$ est un modèle de $S$, écrire $G\models S$, si $S$ est vraie sur les sommets et la relation d'adjacence de $G$. Le problème algorithmique de vérification du modèle (model checking) est relatif au fait de savoir si un graphe est un modèle d'une proposition donnée. Le problème algorithmique de satisfiabilité se demande s'il existe un graphe modélisant une proposition donnée. Bien que la vérification de modèle et la satisfiabilité soient difficiles en général, plusieurs méta-théorèmes algorithmiques majeurs montrent que les propriétés exprimées de cette manière peuvent être testées efficacement pour d'importantes classes de graphes.
D'autres sujets de recherche en logique des graphes incluent des études sur la probabilité qu'un graphe aléatoire modélise une proposition spécifiée pour un type particulier de logique, ainsi que des méthodes de compression des données s'intéressant à la recherche de propositions logiques modélisées par un graphe unique.

## Logique du premier ordre

Dans le logique du premier ordre sur les graphes, une propriété de graphe est exprimée sous la forme d'une phrase logique quantifiée dont les variables représentent les sommets du graphe, et reposant sur les prédicats d'égalité et d'adjacence.

### Exemples

Par exemple, la condition qu'un graphe n'ait pas de sommets isolés peut être exprimée par la proposition :$\forall u\exists v(u\sim v)$où le $\sim$ symbole indique la relation d'adjacence non dirigée entre deux sommets. Cette proposition peut être interprétée comme signifiant que pour chaque sommet $u$ il existe un autre sommet $v$ qui lui est adjacent.
Le problème d'isomorphisme de sous-graphe pour un sous-graphe fixe $H$ cherche à déterminer si $H$ apparaît comme un sous-graphe dans un graphe $G$. Il peut être exprimé par une proposition qui énonce l'existence de sommets (un pour chaque sommet de $H$) tels que, pour chaque arête de $H$, la paire de variables correspondante représente des sommets adjacents et tels que, pour chaque paire restante de sommets de $H$, la paire de variables correspondante représente des sommets distincts ; voir l'illustration. Le problème de clique (pour une taille de clique fixe) en est un cas particulier, il peut être exprimé par une proposition indiquant l'existence d'un nombre de sommets égal à la taille de la clique qui soient tous adjacents entre eux.

### Axiomes

Pour les graphes non orientés simples, la théorie du premier ordre des graphes inclut les axiomes
    $\forall u{\bigl\lnot (u\sim u){\bigr )}$ (le graphe ne contient aucune boucle), et
    $\forall u\forall v(u\sim v)\Rightarrow (v\sim u){\bigr )}$ (le graphe n'est pas orienté).
D'autres types de graphes, tels que les graphes orientés, peuvent impliquer des axiomes différents, et la formulation logique de propriété sur les multigraphes nécessitent un traitement spécial, comme avoir plusieurs relations de bord ou des variables séparées pour les sommets et les arêtes.

### Loi zéro-un

Glebskiĭ et al. (1969) et de manière indépentante, Fagin (1976) ont prouvés une loi zéro-un pour la logique du premier ordre sur les graphes ; la preuve de Fagin reposant sur le théorème de compacité. Ce résultat implique que toute proposition du premier ordre est ou bien presque toujours vraie, ou bien presque toujours fausse sur les graphes d'Erdös-Rényi. Ainsi, soit $S$ une proposition et $G_{n}$ un graphe pris aléatoirement parmi tous les graphes à $n$ sommets. Quand $n$ tend vers l'infini, la probabilité que $G_{n}$ soit un modèle de $S$ tend ou bien vers zéro ou bien vers un .$\lim _{n\to \infty }\operatorname {Pr} [G_{n}\models S]\in \{0,1\}.$De plus, il existe un graphe infini spécifique, le graphe de Rado $R$, tel que les propositions modélisées par le graphe de Rado sont exactement celles pour lesquelles la probabilité d'être modélisée par un graphe fini aléatoire tend vers un : $R\models S\quad \Longleftrightarrow \quad \lim _{n\to \infty }\operatorname {Pr} [G_{n}\models S]=1.$Le même résultat reste vraie pour les graphes aléatoires binomiaux pour lesquels chaque arête est incluse indépendamment des autres avec une probabilité fixe. Et ceux sont les mêmes propositions qui tendent vers un (et donc vers zéro).
Déterminer si une proposition donnée a une probabilité tendant vers zéro ou vers un est un problème PSPACE-complet. Mais si une propriété de graphe du premier ordre a une probabilité tendant vers un pour les graphes aléatoires, alors il est possible de lister tous les graphes à $n$-sommets qui modélisent cette propriété, avec un retard polynomial (en fonction de $n$) par graphe.
Une analyse similaire peut être effectuée pour des graphes aléatoires non uniformes, où la probabilité d'inclure une arête est une fonction du nombre de sommets, et où la décision d'inclure ou d'exclure une arête est prise indépendamment avec une probabilité égale pour toutes les arêtes. Cependant, pour ces graphes, la situation est plus compliquée. Dans ce cas, une propriété du premier ordre peut avoir un ou plusieurs seuils, de sorte que lorsque la probabilité d'inclusion de chaque arête est bornée par ce seuil alors la probabilité d'avoir la propriété donnée tend vers zéro ou un. Ces seuils ne peuvent jamais être une puissance irrationnelle de $n$, donc les graphes aléatoires où la probabilité d'inclusion d'arête est une puissance irrationnelle obéissent à une loi zéro-un analogue à celle des graphes uniformément aléatoires. Une loi similaire zéro-un est valable pour les graphes aléatoires très clairsemés qui ont une probabilité d'inclusion d'arête de $n^{-c}$ avec $c>1$, tant que $c$ n'est pas un rapport superparticulaire. Si $c$ est superparticulaire, la probabilité d'avoir une propriété donnée peut tendre vers une limite qui n'est ni zéro ni un, mais cette limite peut être calculée efficacement. Il existe des propositions du premier ordre qui ont une infinité de seuils.

### Complexité paramétrée

Si une proposition du premier ordre comprend $k$ variables distinctes, alors la propriété qu'elle décrit peut être testée dans des graphes de $n$ sommets en examinant tous les $k$-tuples de sommets ; cependant, cette recherche par force brute ne donne pas un algorithme particulièrement efficace, puisqu'il est de complexité $O(n^{k})$. Le problème de vérifier si un graphe modélise une proposition donnée du premier ordre inclut comme cas particuliers le problème d'isomorphisme de sous-graphe (dans lequel la phrase décrit les graphiques qui contiennent un sous-graphique fixe) et le problème de clique (dans lequel la phrase décrit des graphiques qui contiennent des sous-graphiques complets d'une taille fixe). Le problème de clique est reconnu difficile pour L(1), le premier niveau d'une hiérarchie de problèmes difficiles du point de vue de la complexité paramétrée. Par conséquent, il est peu probable qu'il existe un algorithme à paramètres fixes, dont le temps d'exécution prenne la forme $O(f(k)n^{c})$ pour une fonction $f$ et une constante $c$ qui soient indépendants de $k$ et $n$. Plus fortement, si l'hypothèse du temps exponentiel est vraie, alors la recherche de clique et donc la vérification d'un modèle du premier ordre prendraient nécessairement un temps proportionnel à une puissance de $n$ dont l'exposant est proportionnel à $k$.
Sur certaines classes restreintes de graphes, la vérification des propositions du premier ordre peut être beaucoup plus efficace. En particulier, chaque propriété de graphe exprimable sous la forme d'une proposition du premier ordre peut être testée en temps linéaire pour les graphes d'expansion limitée. C'est-à-dire les graphes pour lesquels tous les mineurs superficiels sont des graphes clairsemés, avec un rapport des arêtes aux sommets bornés par une fonction de la profondeur du mineur. Plus généralement encore, la vérification d'un modèle du premier ordre peut être effectuée en temps quasi linéaire pour des graphes denses nulle part, des classes de graphes pour lesquelles, à chaque profondeur possible, il existe au moins un mineur peu profond interdit. Inversement, s'il existe un algorithme permettant la vérification de toute proposition du premier ordre en temps polynomial pour une famille de graphe donnée, alors cette famille doit être nulle part dense.

### Compression de données et isomorphisme de graphe

On dit qu'une proposition du premier ordre de la logique des graphes $S$, définit un graphe $G$ si $G$ est le seul graphe qui modélise $S$. Pour tout graphe il existe au moins une proposition le définissant ; par exemple, on peut définir n'importe quel $n$- graphe de sommet $G$ par une phrase avec $n+1$ variables, une pour chaque sommet du graphe, et une de plus pour indiquer la condition qu'il n'y a pas de sommet autre que les $n$ sommets de ce graphe. Des clauses supplémentaires sont ensuite ajoutées afin de s'assurer qu'il n'y a pas deux variables représentant le même sommet, que chaque arête de $G$ est présent, et qu'aucune arête n'existe qui ne soit pas dans $G$. Cependant, pour certains graphes, il existe des définitions reposant sur des propositions nettement plus courtes que cette version naïve.
Plusieurs invariants de graphe différent peuvent être définis à partir des propositions les plus simples (pour différentes notions de simplicité) qui définissent un graphe donné. En particulier le profondeur logique d'un graphe est défini comme étant le niveau minimum d'imbrication des quantificateurs (le rang du quantificateur) d'une proposition permettant de modéliser le graphe. La proposition naïve décrite décrite ci-dessus imbrique les quantificateurs de toutes ses variables, elle a donc une profondeur logique de $n+1$. Le largeur logique d'un graphe est définie comme le nombre minimum de variables dans une proposition qui le définit. Dans la proposition naïve décrite ci-dessus, ce nombre de variables est à nouveau de $n+1$. La profondeur logique et la largeur logique peuvent être bornées par une fonction de la largeur arborescente du graphe. De la même manière, la longueur logique est définie comme la longueur de la plus courte proposition modélisant le graphe. La proposition décrite ci-dessus a une longueur proportionnelle à $n^{2}$, mais il est toujours possible de définir un graphe par une proposition de longueur proportionnelle à son nombre d'arêtes.
Tous les arbres, et la plupart des graphes, peuvent être décrits par des propositions du premier ordre incluant seulement deux variables, mais étendues en comptant les prédicats. Pour les graphes qui peuvent être décrits par des propositions avec un nombre constant fixe de variables, il est possible de trouver une écriture canonique du graphe en temps polynomial (avec un exposant égal au nombre de variables). En comparant les canonisations, il est possible de résoudre le problème d'isomorphisme de graphe pour ces graphes en temps polynomial.

### Satisfaisabilité

Déterminer s'il existe un graphe fini non orienté modélisant une proposition donnée est un problème indécidable. Cela signifie qu'il n'existe pas d'algorithme générique permettant de répondre correctement à cette question pour toutes les propositions.
Certaines proposition du premier ordre ne sont modélisées par aucun graphe fini mais peuvent l'être par des graphes infinis. Par exemple, la propriété d'avoir exactement un sommet de degré un, avec tous les autres sommets ayant exactement un degré 2, peut être exprimé par une proposition du premier ordre. Cette propriété viole le lemme des poignées de main d'Euler pour les graphes finis mais peut être représenté par un bout infini. Cependant, il résulte de la solution négative au Problème d'Entscheidungsproblem (par Alonzo Church et Alain Turing dans les années 1930), que la satisfaisabilité des propositions de la logique du premier ordre reste indécidable pour les graphes qui ne sont pas contraints à être finis. Il est également indécidable de faire la distinction entre les propositions du premier ordre qui sont vraies pour tous les graphes et celles qui sont vraies pour les graphes finis mais fausses pour certains graphes infinis.

## Point fixe

Les logiques de graphe basées sur les plus petits points-fixes étendent la logique du premier ordre en autorisant les prédicats (propriétés des sommets ou des tuples de sommets) définis par des opérateurs de point-fixe spéciaux. Ce type de définition commence par une implication, une formule indiquant que lorsque certaines valeurs du prédicat sont vraies, d'autres le sont également. Un « point fixe » désigne alors prédicat pour lequel cette implication est valide. Il peut y avoir de nombreux points fixes, y compris le prédicat toujours vrai ; un « plus petit point fixe » est un point fixe qui a le moins de valeurs vraies possible. Plus précisément, ses valeurs vraies doivent l'être aussi pour tous les autres points fixes.
Par exemple, définissons la connexité : $C(u,v)$ comme vraie lorsque les deux sommets $u$ et $v$ sont connectés par un chemin dans un graphe donné, et faux sinon. Alors chaque sommet est connecté à lui-même, et quand $u$ est connecté à un voisin de $v$, il est également relié (par une étape de plus) à $v$. On peut exprimer ce raisonnement en termes logiques : $C$ est le plus petit point fixe de la formule$C(u,v)\leftarrow {\Bigl(u=v)\vee \exists w{\biglC(u,w)\wedge w\sim v{\bigr )}{\Bigr )}.$Ici, être un point fixe signifie que la vérité du côté droit de la formule implique la vérité du côté gauche, comme le suggère la flèche d'implication inversée. Dans ce cas, être le plus petit point fixe, implique qu'aucun sommet ne sera défini comme connecté à moins que leur connexité ne provienne d'une utilisation répétée de cette implication.
Plusieurs variantes des logiques de point fixe ont été étudiées. Dans la logique du plus petit point fixe, le côté droit de l'opérateur $\leftarrow$ dans la formule de définition doit utiliser le prédicat uniquement de manière positive (c'est-à-dire que chaque occurrence doit être imbriquée dans un nombre pair de négations) afin de bien définir le plus petit point-fixe. La logique du point fixe inflationniste est une autre variante (dont la puissance logique est équivalente), pour cette dernière, la formule n'a pas besoin d'être monotone mais le point fixe résultant est défini comme celui obtenu en appliquant de manière répétée des implications dérivées de la formule de définition à partir du prédicat dont toutes les valeurs sont fausses. D'autres variantes, permettant des implications négatives ou plusieurs prédicats définis simultanément, sont également possibles, mais ne fournissent aucun pouvoir de définition supplémentaire. Un prédicat, défini de l'une de ces manières, peut ensuite être appliqué à un tuple de sommets dans le cadre d'une proposition logique plus large.
Les logiques de points fixes, et les extensions de ces logiques qui autorisent également à compter des variables entières dont les valeurs vont de 0 au nombre de sommets, ont été utilisées en complexité descriptive, dans une tentative de fournir une description logique des problèmes de décision en théorie des graphes qui peuvent être décidés en temps polynomial. Le point fixe d'une formule logique peut toujours être construit en temps polynomial. On utilise pour cela un algorithme qui ajoute à plusieurs reprises des tuples à l'ensemble des valeurs pour lesquelles le prédicat est vrai jusqu'à atteindre un point fixe. Ainsi décider si un graphe modélise une proposition dans cette logique peut toujours être décidé en temps polynomial. Il n'est toutefois pas possible de formulé une proposition de cette logique (point fixe et comptage) pour toutes les propriétés de graphe vérifiables en temps polynomial$^,$. Cependant, pour certaines classes spéciales de graphes, les propriétés vérifiable en temps polynomial sont les mêmes que les propriétés exprimables en logique de point fixe avec comptage. Ceux-ci incluent les graphes aléatoires$^,$, les graphes d'intervalles$^,$ et (par une expression logique de la théorème de structure des graphes) chaque classe de graphes caractérisée par des mineurs interdits.

## Deuxième ordre

Dans le logique monadique du second ordre sur les graphes, les variables représentent des objets de quatre types différents : sommets, arêtes, ensembles de sommets et ensembles d'arêtes. Il existe deux variantes principales de la logique des graphes monadiques du second ordre : MSO$_1$ dans lequel seules les variables d'ensemble de sommets et de sommets sont autorisées, et MSO$_2$ dans lequel les quatre types de variables sont autorisés. Les prédicats sur ces variables incluent les tests d'égalité, les tests d'appartenance et soit l'incidence sommet-arête (si les variables sommet et arête sont autorisées), soit la contiguïté entre des paires de sommets (si seules les variables sommet sont autorisées). Des variations supplémentaires dans la définition autorisent des prédicats supplémentaires tels que des prédicats de comptage modulaires.

### Exemples

À titre d'exemple, le connexité d'un graphe non orienté peut être exprimé en MSO$_1$ comme la proposition : pour chaque partition des sommets en deux sous-ensembles non vides, il existe une arête d'un sous-ensemble à l'autre. Une partition des sommets peut être décrite par le sous-ensemble $S$ de sommets d'un côté de la partition, et chacun de ces sous-ensembles doit soit décrire une partition triviale (une partition dans laquelle l'un ou l'autre côté est vide), soit être traversé par une arête. C'est-à-dire qu'un graphique est connecté lorsqu'il modélise la proposition MSO$_1$ :$\forall S{\Bigl\forall x(x\in S)\vee \forall y{\bigl\lnot (y\in S){\bigr )}\vee \exists x\exists y{\biglx\in S\wedge \lnot (y\in S)\wedge x\sim y{\bigr )}{\Bigr )}.$Cependant, la connexité ne peut pas être exprimée dans une logique de graphe du premier ordre, ni dans une version existentielle de MSO$_1$ (le fragment de MSO$_1$ dans lequel tous les quantificateurs d'ensemble sont existentiels et apparaissent au début de la phrase) ni même dans une version existentielle de MSO$_2$.
L'existence d'une chaîne Hamiltonienne peut être exprimé dans MSO$_2$ par l'existence d'un ensemble d'arêtes qui forme un graphe 2-régulier connecté sur tous les sommets, avec la connexité exprimée comme ci-dessus et la 2-régularité exprimée comme l'incidence de deux mais pas trois arêtes distinctes à chaque sommet. Cependant, cette propriété n'est pas exprimable dans MSO$_1$, parce que MSO$_1$ n'est pas capable de distinguer les graphes bipartites complets avec un nombre égal de sommets de chaque côté de la bipartition (qui sont hamiltoniens) des graphes bipartites complets déséquilibrés (qui ne le sont pas).
Bien que cela ne fasse pas partie de la définition de MSO$_2$, l'orientation des graphes non orientés peuvent être représentés par une technique impliquant des Arbres de Trémaux. Cela permet également d'exprimer d'autres propriétés de graphe impliquant des orientations.

### Théorème de Courcelle

Selon le Théorème de Courcelle, toute propriété de MSO$_2$ peut être testée en temps linéaire sur des graphes dont la largeur arborescente est bornée, et toute propriété de MSO$_1$ peut être testée en temps linéaire sur des graphes dont la largeur de clique est bornée. Ce résultat pour les graphes de largeur arborescente bornée garanti aussi l'existence d'un algorithme LOG-SPACE. Une application de ce résultat est le développement d'un algorithme permettant de calculer le nombre de croisement d'un graphe en un temps raisonnable.

### Théorème de Seese

Le problème de satisfaisabilité pour une proposition de la logique monadique du second ordre, est le problème de déterminer s'il existe au moins un graphe (éventuellement dans une famille restreinte de graphes) pour lequel la proposition est vraie. Sans restriction, ce problème est indécidable. Cependant, la satisfaisabilité des propositions de MSO$_2$ décidable pour les graphes de largeur arborescente bornée et de satisfaisabilité des propositions MSO$_1$ est décidable pour les graphes de largeur de clique bornée. La preuve repose sur le théorème de Courcelle pour construire un automate capable de tester la propriété, puis à examiner l'automate pour déterminer s'il existe un graphe qu'il peut accepter. L'inverse est partiellement vraie, Seese (1991) a prouvé que, lorsqu'une famille de graphes est décidable pour MSO$_2$, cette famille doit avoir une largeur arborescente bornée. Seese a également conjecturé que chaque famille de graphes décidable pour MSO$_1$ doit avoir une largeur de clique bornée. Cela n'a toutefois été prouvé, que dans une version faible autorisant les prédicats de comptage modulaires.