Sall, Amadou
(2026).
« Solveurs MaxSAT anytime : conception d'un banc d'essai et développement d'un solveur de recherche locale » Mémoire.
Montréal (Québec, Canada), Université du Québec à Montréal, Maîtrise en informatique.
Fichier(s) associé(s) à ce document :
Résumé
Ce mémoire étudie les solveurs MaxSAT anytime, c’est-à-dire des algorithmes capables de produire rapidement une solution valide puis d’en améliorer progressivement la qualité sous une contrainte de temps. Le travail poursuit deux objectifs complémentaires : proposer un cadre d’évaluation mieux adapté à la dynamique temporelle de ces solveurs et disposer d’une base expérimentale modulaire pour analyser finement plusieurs mécanismes de recherche locale. La première contribution est MaxSAT Runner, un banc d’essai qui capture les améliorations de coût au fil de l’exécution, reconstruit des trajectoires anytime, agrège plusieurs répétitions et produit des visualisations ainsi que des indicateurs comparatifs adaptés à l’analyse temporelle. La seconde contribution est EvalMaxSAT Anytime, une base expérimentale de solveur pour Weighted Partial MaxSAT, conçue pour étudier de manière contrôlée l’effet du redémarrage, de la pondération dynamique et du débiaisage dans la sortie des minima locaux. Les expériences montrent que MaxSAT Runner permet de distinguer des comportements qui restent invisibles dans une lecture fondée uniquement sur le coût final, tandis qu’EvalMaxSAT Anytime met clairement en évidence le rôle structurant de la pondération dynamique et l’apport plus nuancé du débiaisage selon l’horizon temporel et le type d’instances considéré.
_____________________________________________________________________________
MOTS-CLÉS DE L’AUTEUR : MaxSAT anytime, évaluation expérimentale, recherche locale stochastique, trajectoires de convergence, pondération dynamique.