Solveurs MaxSAT anytime : conception d'un banc d'essai et développement d'un solveur de recherche locale

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 :
[img]
Prévisualisation
PDF
Télécharger (4MB)

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.

Type: Mémoire accepté
Informations complémentaires: Fichier numérique reçu en format PDF.
Directeur de thèse: Avellaneda, Florent
Mots-clés ou Sujets: Problème de satisfiabilité maximale / MaxSAT / Solveurs / Algorithmes anytime
Unité d'appartenance: Faculté des sciences > Département d'informatique
Déposé par: Service des bibliothèques
Date de dépôt: 03 sept. 2026 07:56
Dernière modification: 03 sept. 2026 07:56
Adresse URL : https://archipel.uqam.ca/secure/id/eprint/20252

Statistiques

Voir les statistiques sur cinq ans...