Justement. Est-il normal, pour par exemple mettre à jour Wormux, d'avoir à gérer 16000 paquets. Là, ça prend 2,5 secondes, ce qui est correct. Maintenant, si t'as 160 000 paquets, ça va prendre 25 secondes, et là ça fait mal, très mal (et 160 000 paquets, c'est une affaire d'années).
Il me semble qu'un problème SAT est une suite de clauses, comme ceci (format utilisé par MiniSAT en entrée) :
-1 2 3
3 4 -5
...
Construire une telle liste nécessite de lire tous les paquets de la base de donnée, c'est à dire un minimum un for() sur les paquets.
Pour chaque paquet, il faut lister ses dépendances (ce qui est rapide en binaire), etc. Au final, la construction du problème prend presque autant de temps que sa résolution.
[^] # Re: SAT, une artillerie lourde ?
Posté par steckdenis . En réponse au journal Résolution des dépendances par système de branches. Évalué à 1.
Justement. Est-il normal, pour par exemple mettre à jour Wormux, d'avoir à gérer 16000 paquets. Là, ça prend 2,5 secondes, ce qui est correct. Maintenant, si t'as 160 000 paquets, ça va prendre 25 secondes, et là ça fait mal, très mal (et 160 000 paquets, c'est une affaire d'années).
Il me semble qu'un problème SAT est une suite de clauses, comme ceci (format utilisé par MiniSAT en entrée) :
-1 2 33 4 -5
...
Construire une telle liste nécessite de lire tous les paquets de la base de donnée, c'est à dire un minimum un for() sur les paquets.
Pour chaque paquet, il faut lister ses dépendances (ce qui est rapide en binaire), etc. Au final, la construction du problème prend presque autant de temps que sa résolution.
Maintenant, je me trompe peut-être.