> Si c'est exponentiel, c'est juste que c'est inefficace
Petit jeu: Calculer 2^64. (inspiré du célèbre problème de l'échiquier). En déduire le nombre d'opérations qu'il faut pour vérifier un programme a 64 variables si l'algo est en 2^nombre de variables. Convertir ce nombre d'opérations en temps (unité de temps laissée au choix du lecteur, entre la seconde et le million d'annéés).
Question 2: compter le nombre de variables dans un programme réél et refaire le calcul précédant.
Question 3: Programmer la suite de fibbonacci non optimisée, faire tourner le programme pour n = 1, n = 10, n = 100. Revenir poster un commentaire ici quand le dernier calcul sera terminé.
Conclusion: Revenir ici disserter sur le fait qu'un algo exponentiel, c'est pas grave, c'est juste inefficace.
En pratique, les algos de verif sont tous exponentiels dans le pire cas (et encore, la question est souvent indécidable), et la difficulté est de trouver le moyen de ne pas être dans le pire cas. Avec du model checking symbolique par exemple, des problèmes qui auraient mis des milliards d'années de calcul en model checking enumératif peuvent être résolu en une fraction de seconde (cf. le fameux papier 10^20 states and beyond). Mais ça ne veut pas dire que ça marchera toujours.
[^] # Re: exponentiel => indecidable
Posté par Matthieu Moy (site web personnel) . En réponse au journal couverture de code. Évalué à 4.
Petit jeu: Calculer 2^64. (inspiré du célèbre problème de l'échiquier). En déduire le nombre d'opérations qu'il faut pour vérifier un programme a 64 variables si l'algo est en 2^nombre de variables. Convertir ce nombre d'opérations en temps (unité de temps laissée au choix du lecteur, entre la seconde et le million d'annéés).
Question 2: compter le nombre de variables dans un programme réél et refaire le calcul précédant.
Question 3: Programmer la suite de fibbonacci non optimisée, faire tourner le programme pour n = 1, n = 10, n = 100. Revenir poster un commentaire ici quand le dernier calcul sera terminé.
Conclusion: Revenir ici disserter sur le fait qu'un algo exponentiel, c'est pas grave, c'est juste inefficace.
En pratique, les algos de verif sont tous exponentiels dans le pire cas (et encore, la question est souvent indécidable), et la difficulté est de trouver le moyen de ne pas être dans le pire cas. Avec du model checking symbolique par exemple, des problèmes qui auraient mis des milliards d'années de calcul en model checking enumératif peuvent être résolu en une fraction de seconde (cf. le fameux papier 10^20 states and beyond). Mais ça ne veut pas dire que ça marchera toujours.