Parcours de graphe, algorithme générique

Répertoire GitHub correspondant à cet article : https://github.com/peportier/ia-parcours

Dérivation du programme à partir de sa spécification

Première esquisse

Étant donné un graphe orienté et un nœud de ce graphe, nous cherchons à calculer l'ensemble des nœuds atteignables à partir de .

Nous notons la fonction "successeur" qui retourne les voisins directs d'un ensemble de nœuds.

Nous définissons la fonction ("atteignable") :

L'ensemble des nœuds atteignables à partir de possède la propriété : En particulier, .

L'ensemble des nœuds atteignables à partir de l'ensemble de nœuds est le plus petit ensemble qui inclut et qui possède la propriété ci-dessus. Sans cette précision, cette propriété ne permettrait pas de définir . Par exemple, quelque soit , l'ensemble de tous les nœuds du graphe satisferait cette égalité.

Il faudrait également montrer qu'un plus petit ensemble solution existe. C'est-à-dire, montrer qu'étant données et deux solutions (i.e., et ), est également solution. Il s'en suit qu'étant donné , il existe un plus petit ensemble solution incluant (viz. l'intersection de tous les ensembles qui sont solution et qui incluent ).

Il s'agit de calculer un programme dont la post-condition est l'équation d'inconnue suivante :

Pour fixer les idées, nous pouvons avoir à l'esprit un exemple de graphe orienté (mais attention à ne pas être trop influencé par une configuration particulière...).

ellipse

Nous avons par exemple :

Nous cherchons une manière d'affaiblir la postcondition dans l'idée de découvrir un invariant. Nous remarquons :

Nous avons donc l'idée d'invariant :

Et nous pouvons progresser vers la solution grâce à l'affectation :

Mais, sous quelle condition devons-nous sortir de la boucle ? Nous remarquons :

Nous avons donc montré que :

D'où une première version du programme (le symbole ⍝ est utilisé pour introduire un commentaire):

Optimisation

Le programme que nous avons dérivé peut calculer plusieurs fois les successeurs d'un même nœud. Nous modifions l'invariant pour distinguer les nœuds dont les successeurs nous sont déjà connus (notés et que nous appellerons aussi les nœuds noirs) de ceux déjà rencontrés mais dont les successeurs nous sont encore inconnus (notés et que nous appellerons aussi les nœuds gris). Nous appellerons les nœuds encore non considérés : les nœuds blancs.

Ce qui nous amène à un nouveau programme optimisé :

Le programme termine-t-il ? Le nombre de nœuds qui ne sont pas dans est au moins égal à . A chaque itération, ce nombre décroît du nombre de nœuds de ( car ). Or le nombre de nœuds de est strictement positif à cause de la clause garde de la boucle ( ). Ainsi, nous avons isolé une fonction monotone stricte et bornée ("bound function") qui prouve la terminaison du programme.

Implémentation

Nous proposons maintenant une implémentation du programme qui, étant donné un graphe orienté et un nœud de ce graphe, calcule l'ensemble des nœuds atteignables à partir de .

Nous utiliserons le langage C++11. Pour compiler le programme vous pourrez utiliser la commande : g++ -std=c++11 -g src.cpp -o prog en phase de développement, et la commande : g++ -std=c++11 -O3 src.cpp -o prog (i.e. avec optimisations) pour améliorer la performance.

 

Chaque nœud porte une valeur entière et une liste de voisins directs.

 

Nous calculons la fermeture de la relation de voisinage avec l'algorithme dérivé plus haut.

 

Le code principal affichera simplement la liste des noeuds atteignables à partir d'un noeud source.