Annexe optionnelle — Preuve et complexité de l'algorithme de Dijkstra¶
VERSION corrigée
Cette annexe est facultative. Elle prolonge la Séance 6 pour les étudiantes à l'aise et curieuses d'aller plus loin dans la formalisation (preuve d'algorithme, complexité). Elle n'est pas nécessaire pour suivre la Séance 7 (implémentation) ni pour l'évaluation.
3- Preuve de l'algorithme de Dijkstra¶
Rappel de cours sur la preuve d'un algorithme:¶
réaliser la preuve (appelée aussi "correction totale"$*$) d’un algorithme, par deux vérifications : • Prouver (vérif.1) sa terminaison . • Prouver (vérif.2) sa correction (appelée aussi "correction partielle"$*$).
Terminaison (vérif.1) :¶
Consiste à vérifier que les calculs effectués par l’algorithme s’arrêtent bien. Notamment, lorsqu’une boucle conditionnelle est effectuée par l’algorithme, il est primordial de vérifier que l’on sort bien de cette boucle, en particulier si cette boucle est non bornée. Dans ce dernier cas, identifier un variant de boucle (quantité entière positive ou nulle) qui doit décroitre à chaque itération.
Travail à faire 3, "preuve" de l'algorithme de Dijkstra: terminaison¶
Montrer la terminaison de cet algorithme en raisonnant sur son écriture (proposée au Taf2). Pour cela, répondre au QCM2 ci-dessous.
$QCM2:$ Dans l'écriture de l'algorithme de Dijkstra proposée au Taf2, pour montrer sa terminaison, on peut raisonner comme suit: $Rep1:$ La boucle conditionnelle 'Pour' porte sur le parcours des sommets voisins, donc la variable $s_{voisin}$ est le variant de boucle. A chaque itération, le plus proche sommet voisin est mis à jour. Donc quand tous les sommets ont été parcourus, l'algorithme donnera le plus court chemin. $Rep2:$ Dans cet algorithme, il y a une boucle conditionnelle non bornée, donc cela suffit pour montrer sa terminaison. $Rep3:$ La boucle conditionnelle non bornée 'Tant que' porte sur la condition du parcours exhaustif des sommets du graphe pondéré, donc la variable $E_{calculés}$ est le variant de boucle. A chaque itération, le sommet actuel de poids minimal est ajouté à $E_{calculés}$. Donc pour $n$ sommets, et en autant d'itérations, tous les sommets auront été parcourus et l'ensemble $E_{calculés}$ sera rempli. $Rep4:$ La boucle conditionnelle non bornée 'Tant que' porte sur la condition du parcours exhaustif des sommets du graphe pondéré, donc la variable $E_{sommet}$ est le variant de boucle. A chaque itération, le sommet actuel de poids minimal est retiré de $E_{sommet}$. Donc pour $n$ sommets, et en autant d'itérations, tous les sommets auront été parcourus et l'ensemble $E_{sommet}$ sera vide.
Réponse Taf3 : La bonne réponse: $Rep4:$ La boucle conditionnelle non bornée 'Tant que' porte sur la condition du parcours exhaustif des sommets du graphe pondéré, donc la variable $E_{sommet}$ est le variant de boucle. A chaque itération, le sommet actuel de poids minimal est retiré de $E_{sommet}$. Donc pour $n$ sommets, et en autant d'itérations, tous les sommets auront été parcourus et l'ensemble $E_{sommet}$ sera vide. Explications complémentaires: L'algorithme de Dijkstra dans sa fonction principale (ligne2) contient une boucle non bornée "Tant que" qui est le parcours exhaustif des sommets du graphe pondéré. Sa condition d'arrêt est lorsqu'il n'y a plus de sommets à explorer dans le graphe. Le "variant de boucle" est $E_{sommets}$ (ligne2), ensemble duquel est retiré (ligne4) le sommet de poids minimal actuel à chaque tour de boucle. Cet ensemble, au bout d'un nombre fini d'itérations (correspondant à $n$ sommets) sur la boucle "Tant que" sera vide; ce qui montre la terminaison de cet algorithme. référence sitographique: cours Bloc2 correction
Suite du rappel de cours sur la preuve d'un algorithme, Correction (vérif.2) :¶
Consiste à prouver que l’algorithme aboutit au résultat escompté en identifiant un "invariant de boucle". Cet invariant doit posséder une propriété vérifiable avant l’entrée dans la boucle, lors d'une itération n de la boucle, ainsi qu'à l'itération n+1 et enfin amène au résultat escompté à la sortie de la boucle.
Travail à faire 4, "preuve" de l'algorithme de Dijkstra: correction¶
L'algorithme détaillé des trois fonctions secondaires, de l'algorithme de Dijkstra proposé au Taf2 vous est donné ci-dessous.
Vous admettrez que $poids[s_{voisin}] ≥ poids[s_{mini} ] + Distance(s_{mini} , s_{voisin}) )$ est un invariant de boucle dans cet algorithme et qu'il est vérifiable à chaque itération de la boucle principale dans l'algorithme de Dijkstra .
1- Que signifie l'affirmation (démontrée) ci-dessus pour la correction de cet algorithme?
2- Conclure sur la preuve de l'algorithme de Dijkstra.
Réponse Taf4 : 1- L'affirmation " $poids[s_{voisin}] ≥ poids[s_{mini} ] + Distance(s_{mini} , s_{voisin}) )$ est un invariant de boucle dans cet algorithme et qu'il est vérifiable à chaque itération de la boucle principale de l'algorithme de Dijkstra" signifie que la correction de l'algoritme de Dijkstra est vérifiée. 2- Conclusion: puisque la terminaison (Taf3) et la correction (ci-dessus) sont vérifiées, alors la preuve de l'algorithme de Dijkstra est faite. référence sitographique: https://interstices.info/le-plus-court-chemin/?hlText=bellman https://perso.liris.cnrs.fr/christine.solnon/supportAlgoGraphes.pdf https://www.enseignement.polytechnique.fr/informatique/INF431/X12-2013-2014/inf431-poly.pdf
4- Complexité de l'algorithme de Dijkstra¶
Rappel de cours, complexité (temporelle) d'un algorithme¶
Le calcul de la complexité d’un algorithme permet de mesurer sa performance. Il en existe deux types :
- complexité spatiale : permet de quantifier l’utilisation de la mémoire
- complexité temporelle : permet de quantifier la vitesse d’exécution Réaliser un calcul de complexité temporelle d'un algorithme revient à compter le nombre d’opérations élémentaires (affectation, calcul arithmétique ou logique, comparaison…) effectuées par cet algorithme. On calculera le plus souvent la complexité dans le pire des cas, car elle est la plus pertinente. Pour simplifier, on s'interresse à l’ordre de grandeur (asymptotique), noté O (« grand O ») du calcul exact exhaustif (qui peut être complexe) consistant à négliger le nombre d'instructions éxécutées en 1 tour de boucle (en le ramenant à 1) devant n (nombre de données à traiter) tours de boucle (soit n tours dans une boucle 'Tant que'). Pour repère,quelques valeurs: pour un nombre n de données à traiter, l'ordre de grandeur de la complexité d'une boucle simple est O(n), de k boucles consécutives est k x O(n) et pour deux boucles imbriquées est O(n x n) = O(n²) .
Travail à faire 5, complexité (temporelle) de l'algorithme de Dijkstra¶
Déterminer l'ordre de grandeur de complexité de la version proposée de l’algorithme de Dijkstra en portant attention à l'agencement des boucles dans cet algorithme. Pour cela, répondre au QCM3 suivant.
$QCM3:$ Dans l'écriture de l'algorithme de Dijkstra proposée au Taf2, la fonction principale contient des boucles et pour déterminer sa complexité (en ordre de grandeur), on raisonne comme suit: $Rep1:$ Une boucle non bornée de complexité $O(n-1)≈ O(n)$ et une boucle bornée de complexité $O(n-2)≈ O(n)$ , toutes deux consécutives d'ou une complexité $2×O(n)$. $Rep2:$ Deux boucles bornées imbriquées, d'ou une complexité $O(n × n) = O(n²)$. $Rep3:$ Une boucle 'Pour' de complexité $O(n-1)≈ O(n)$ imbriquée dans une boucle 'Tant que' de complexité $O(n-1)≈ O(n)$, d'ou une complexité $O(n × n) = O(n²)$. $Rep4:$ Une boucle 'Tant que' de complexité $O(n-1)≈ O(n)$ consécutive à une boucle 'Pour' de complexité $O(n-1)≈ O(n)$, d'ou une complexité $2×O(n)$
Réponse Taf5 : La bonne réponse: $Rep3:$ Une boucle 'Pour' de complexité $O(n-1)≈ O(n)$ imbriquée dans une boucle 'Tant que' de complexité $O(n-1)≈ O(n)$, d'ou une complexité $O(n × n) = O(n²)$. Explications:
boucle 'Tant que' :¶
Pour $n$ sommets, l’algorithme de Dijkstra nécessite au plus $n–1$ étapes pour parcourir les sommets du graphe directement accessibles (au plus $n-1$) à partir du sommet de départ . $O(n-1)≈ O(n)$.
boucle 'Pour' :¶
Pour chaque sommet de $S_{calculés}$, la boucle 'Pour' itère sur les $n-2$ (au plus) sommets directement accessibles du sommet en cours d'évaluation. $O(n-2)≈ O(n)$.
imbriquation des 2 boucles:¶
Comme la 2ème boucle 'Pour' est imbriquée dans la 1ère boucle 'Tant que', le coût d'une telle structure de boucle est $O(n × n) = O(n²)$ A noter que cette complexité peut être réduite en changeant la structure de donnée, ce qui pourra faire un objet d'étude en terminale . référence sitographique: cours Bloc2 correction