UQAM - Université du Québec à Montréal
Archive de publications électroniques
UQAM ›  Archive de publications électroniques ›  Méthode SAT et algorithme DPLL appliqués à un problème de recherche opérationnelle

Méthode SAT et algorithme DPLL appliqués à un problème de recherche opérationnelle

Rahmoune, Nabila (2006). « Méthode SAT et algorithme DPLL appliqués à un problème de recherche opérationnelle » 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
1607Kb

Résumé

La littérature fait état des travaux de recherches qui ont été menés pour la résolution des problèmes d'ordonnancement de production. La complexité de ces problèmes rend nécessaire l'emploi de stratégies de recherche de solutions évoluées. Parmi celle-ci figure le formalisme du calcul propositionnel, le plus souvent sous forme normale conjonctive (FNC) associé au problème de satisfiabilité (SAT). Le présent travail de recherche a pour but d'intégrer les formalismes d'approches de résolution des problèmes SAT pour la résolution du problème d'ordonnancement de production, soit le problème d'ordonnancement de véhicules, proposé dans le cadre du challenge ROADEF'2005. Dans un premier temps, les principaux algorithmes pour la résolution de problème SAT sont présentés, particulièrement les algorithmes basés sur le retour en arrière tels que le retour-arrière (Backtracking) et le retour ponctuel (Backjumping) étendus sur les TL-clauses (True-Literal clauses). Ce travail de recherche couvre le développement de trois approches de résolutions du problème SAT appliquées au problème d'ordonnancement de véhicules. Pour chaque approche un encodage en FNC/TL traduisant les contraintes du problème ainsi que l'objectif à optimiser sont effectués. Ces FNC/TL sont générées en format DIMACS à l'aide du logiciel développé par l'auteur. Ensuite, une stratégie de résolution est décrite, en fixant à chaque fois l'objectif à optimiser. Dans la première approche, le problème est traité globalement. Les deux autres approches subdivisent le problème initial en sous-problèmes. Finalement une comparaison des trois approches est décrite. Les instances du problème proposées par le challenge ROADEF'2005 sont utilisées comme base d'évaluation des approches développées. Les résultats obtenus sont comparés aux meilleurs résultats obtenus par le gagnant du challenge ROADEF'2005, à l'aide du logiciel suggéré par le challenge, soit exeCarSeq. Une analyse détaillée des résultats montre que notre stratégie de résolution du problème d'ordonnancement de véhicules est une voie prometteuse. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Forme normale conjonctive, Problème de satisfiabilité, Problème d'ordonnancement de véhicules, TL-clauses, Encodage en FNC/TL.

Type de document : Mémoire accepté
État du document : Non publié
Informations complémentaires : Le mémoire a été numérisé tel que transmis par l'auteur.
Mots-clés : Logique propositionnelle, Algorithme, Test de satisfaisabilité, Résolution de problème, Gestion des travaux
Unité d'appartenance : Faculté des sciences > Département d'informatique
Code ID : 3180
Déposé par : RB Service des bibliothèques
Déposé le : 16 juill. 2010 11:57
Dernière modification : 02 déc. 2010 09:36

Modifier les métadonnées de ce document.

Voir les statistiques sur cinq ans...