• PhD defended on :
  • Nov 22, 2007

jeudi 22 novembre 2007 - 14h00 - Salle des thèses

Résumé

Le cadre Problème de Satisfaction de Contraintes (ou CSP pour Constraint Satisfaction Problem) regroupe les problèmes modélisables sous la forme de contraintes. Pour résoudre ce type de problèmes, une approche classique, et complète, consiste à alterner prises de décisions (assignations de variables) et processus de propagation de contraintes (réduction de l’espace de recherche). Au lieu de remettre en cause systématiquement le dernier choix effectué lorsqu’un conflit (i.e. l’impossibilité de trouver une solution sur la base des décisions déjà prises) apparaît, il peut être intéressant d’identifier les raisons précises de cet échec. Nous proposons dans cette thèse plusieurs techniques d’analyse et d’exploitation des conflits qui permettent de réduire de façon significative l’effort de recherche nécessaire à la résolution des problèmes de satisfaction de contraintes. Nous montrons tout d’abord qu’il est possible de guider efficacement la recherche en se basant sur les derniers conflits rencontrés. L’approche que nous proposons permet de lutter contre le thrashing (le fait de reproduire plusieurs fois les mêmes erreurs) en orientant la recherche sur l’origine du dernier conflit rencontré. Une autre solution connue consiste à effectuer des redémarrages : l’algorithme de recherche est relancé plusieurs fois pour diversifier la recherche. Cependant, dans ce contexte, il n’est pas exclu d’explorer inutilement plusieurs fois les mêmes portions de l’espace de recherche. Pour éviter cela, nous proposons une technique consistant à calculer a posteriori, i.e. à chaque redémarrage, les explications des échecs rencontrés au cours de la recherche sous la forme d’un ensemble de nogoods (ensembles d’assignations de variables perçues comme de nouvelles contraintes). Ceux-ci sont enregistrés dans une base exploitée grace à une structure de données paresseuse : les watched literals. Finalement nous mettons en évidence le fait que des situations (i.e. des états de la recherche à un instant donné) similaires peuvent apparaître au cours de la recherche. Nous introduisons des opérateurs originaux, basés sur la détection d’états partiels inconsistants, permettant l’identification de ces situations jugées équivalentes. Un état partiel inconsistant représente un sous-ensemble de l’état de la recherche à un instant donné, suffisant pour démontrer l’absence de solution à partir de cet état. Nous montrons également que ces opérateurs permettent de détecter et casser dynamiquement certaines formes de symétries.

Composition du jury

  • Gérard Verfaillie (rapporteur) ONERA Toulouse
  • Narendra Jussien (rapporteur) Ecole des Mines de Nantes
  • Christian Bessière LIRMM Montpellier
  • Ulrich Junker ILOG Valbonne
  • Eric Grégoire (directeur de thèse) CRIL Lens
  • Christophe Lecoutre CRIL Lens
  • Lakhdar Sais CRIL Lens
  • Vincent Vidal CRIL Lens