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 peut être vraie pour certains graphes et fausse pour d'autres; un graphe est un modèle de , écrire , si est vraie sur les sommets et la relation d'adjacence de . Le problème algorithmique de vérification du modèle () 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 vignette|Le graphique illustré ici apparaît comme le sous-graphe d'un graphe non orienté si et seulement si modélise la proposition .
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 :où le 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 il existe un autre sommet qui lui est adjacent.
Le problème d'isomorphisme de sous-graphe pour un sous-graphe fixe cherche à déterminer si apparaît comme un sous-graphe dans un graphe . Il peut être exprimé par une proposition qui énonce l'existence de sommets (un pour chaque sommet de ) tels que, pour chaque arête de , la paire de variables correspondante représente des sommets adjacents et tels que, pour chaque paire restante de sommets de , 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
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 vignette|Le Graphe de Rado, un graphe infini qui modélise exactement les propositions de la logique du premier ordre qui sont presque toujours vraies sur les graphes finis ! Glebskiĭ et al. (1969) et de manière indépendante, Fagin (1976) ont prouvé 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 une proposition et un graphe pris aléatoirement parmi tous les graphes à sommets. Quand tend vers l'infini, la probabilité que soit un modèle de tend ou bien vers zéro ou bien vers un .De plus, il existe un graphe infini spécifique, le graphe de Rado , 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 : Le même résultat reste vrai pour les graphes aléatoires binomiaux pour lesquels chaque arête est incluse indépendamment des autres avec une probabilité fixe. Et ce 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 à -sommets qui modélisent cette propriété, avec un retard polynomial (en fonction de ) 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 , 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 avec , tant que n'est pas un rapport superparticulaire. Si 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 variables distinctes, alors la propriété qu'elle décrit peut être testée dans des graphes de sommets en examinant tous les -tuples de sommets ; cependant, cette recherche par force brute ne donne pas un algorithme particulièrement efficace, puisqu'il est de complexité . 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 pour une fonction et une constante qui soient indépendants de et . 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 dont l'exposant est proportionnel à .
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 , définit un graphe si est le seul graphe qui modélise . Pour tout graphe il existe au moins une proposition le définissant ; par exemple, on peut définir n'importe quel - graphe de sommet par une phrase avec 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 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 est présent, et qu'aucune arête n'existe qui ne soit pas dans . 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 . La 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 . 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 à , 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.