<i>Pour le solveur SAT, rien que le fait qu'on doive lire tous les paquets est lourds. Il y a peut-être moyen de l'éviter, mais le but est de construire un problème à base de clauses, une ou plusieurs clauses par paquets. Oui, ce sont des clauses simples (comme dit dans la page Zypp, ça doit faire quelques mois que je lis presque tous les jours ce wiki et la doc Doxygen de libzypp), mais il y en a beaucoup.</i>
A te lire, j'ai vraiment l'impression qu'on parle de 2 choses totalement différentes et que tu n'a pas saisi comment le solver d'openSUSE fonctionne. Tu devrais aussi lire la doc de Daniel Burrows et celle du projet EDOS, ainsi que jeter un oeil au fonctionnement du SatSolver ZYpp en utilisation réelle.
Pour mémoire, voici le fonctionnement basic de ZYpp :
1/ teléchargement des métadonnées depuis les dépôts
2/ transformation des métadonnées en fichiers binaires .solv, qui contiennent les règles de dépendances de chacun des paquets
3/ calcul des dépendances
4/ application du résultat
L'étape 1/ est "bottleneck", elle ne dépend pas du solveur, mais du format des md-data et de la qualité de la connexion aux dépôts.
L'étape 2/ utilise une "dictionary approach" pour stocker les dépendances sous la forme d'un nombre 32bits unique, permettant une comparaison très rapide de 2 chaines de "charactères", principe de base du solveur SAT, un espace disque moindre, puisqu'un nombre est plus petit qu'une chaine de charactère (j'ai 4.7 Mo, 4.5 Mo, 3.6 Mo, 406 Ko pour les 4 plus gros dépôts activés qui représentent à eux seul un peu plus de 16'000 paquets, 1.4 Mo pour ma base RPM locale .solv, et mes 14 autres ne font que quelques Ko) et la representation mémoire ne prend pas plus de place sur un système 64bits où un pointer est 2x la taille d'un nombre 32bits (cf. doc SatSolver).
Un refresh forcé de ces fichiers me prends ~9 secondes, mais est surévalué puisque le dépôt principal, qui ne change jamais, est recré (5 sec est plus realiste pour une utilisation standard.. et encore).
L'étape 3/ me calcul les dépendances (par exemple un dist-upgrade me propose une solution en ~2.5 secondes), enfin l'étape 4/ valide les changements et télécharge les paquets proposés.
Au final, le calcul des dépendances est extrêmement rapide malgré le fait qu'un grand nombre de paquets sont pris en compte en mémoire (~2.5 secondes pour +16'000 paquets). J'ai l'impression que le problème que tu essaies de résoudre n'existe tout simplement pas avec un solver sat couplé avec une approche metadonnés-binaire telle qu'implémentée par ZYpp. De plus, la résolution est complète.
[^] # Re: SAT, une artillerie lourde ?
Posté par Spyhawk . En réponse au journal Résolution des dépendances par système de branches. Évalué à 5.
A te lire, j'ai vraiment l'impression qu'on parle de 2 choses totalement différentes et que tu n'a pas saisi comment le solver d'openSUSE fonctionne. Tu devrais aussi lire la doc de Daniel Burrows et celle du projet EDOS, ainsi que jeter un oeil au fonctionnement du SatSolver ZYpp en utilisation réelle.
Pour mémoire, voici le fonctionnement basic de ZYpp :
1/ teléchargement des métadonnées depuis les dépôts
2/ transformation des métadonnées en fichiers binaires .solv, qui contiennent les règles de dépendances de chacun des paquets
3/ calcul des dépendances
4/ application du résultat
L'étape 1/ est "bottleneck", elle ne dépend pas du solveur, mais du format des md-data et de la qualité de la connexion aux dépôts.
L'étape 2/ utilise une "dictionary approach" pour stocker les dépendances sous la forme d'un nombre 32bits unique, permettant une comparaison très rapide de 2 chaines de "charactères", principe de base du solveur SAT, un espace disque moindre, puisqu'un nombre est plus petit qu'une chaine de charactère (j'ai 4.7 Mo, 4.5 Mo, 3.6 Mo, 406 Ko pour les 4 plus gros dépôts activés qui représentent à eux seul un peu plus de 16'000 paquets, 1.4 Mo pour ma base RPM locale .solv, et mes 14 autres ne font que quelques Ko) et la representation mémoire ne prend pas plus de place sur un système 64bits où un pointer est 2x la taille d'un nombre 32bits (cf. doc SatSolver).
Un refresh forcé de ces fichiers me prends ~9 secondes, mais est surévalué puisque le dépôt principal, qui ne change jamais, est recré (5 sec est plus realiste pour une utilisation standard.. et encore).
L'étape 3/ me calcul les dépendances (par exemple un dist-upgrade me propose une solution en ~2.5 secondes), enfin l'étape 4/ valide les changements et télécharge les paquets proposés.
Au final, le calcul des dépendances est extrêmement rapide malgré le fait qu'un grand nombre de paquets sont pris en compte en mémoire (~2.5 secondes pour +16'000 paquets). J'ai l'impression que le problème que tu essaies de résoudre n'existe tout simplement pas avec un solver sat couplé avec une approche metadonnés-binaire telle qu'implémentée par ZYpp. De plus, la résolution est complète.