• Doctorant:
  • Julien Vion
  • Thèse soutenue le :
  • 30 nov. 2007 • IUT de Lens (amphi SRC)

Résumé

Nous proposons plusieurs techniques visant à résoudre en pratique le problème NP-complet de satisfaction de contraintes de manière totalement générique, c’est à dire indépendamment de la nature du problème à résoudre (par “boite noire”). Nous distinguons deux grands axes de techniques de résolution de CSP : l’inférence et la recherche. Nous avons contribué à l’amélioration des techniques d’inférence en nous concentrant sur la propriété centrale qu’est la consistance d’arc : optimisations des algorithmes établissant la consistance d’arc, comportement de plusieurs algorithmes d’inférence en limitant leur action aux bornes des domaines discrets, et enfin une alternative intéressante à la consistance de chemin : la consistance duale. Cette propriété nous a amenés à concevoir des algorithmes capables d’établir la consistance de chemin de manière très efficace en pratique. Nous nous sommes alors intéressé à la variante conservative de la consistance duale, c’est à dire limitée aux contraintes existant dans le problème. La consistance duale conservative est plus forte que la consistance de chemin conservative, et l’algorithme proposé pour établir la consistance duale conservative est en pratique très souvent beaucoup plus rapide que les algorithmes connus d’établissement de la consistance de chemin conservative.

Par ailleurs, nous avons également cherché à améliorer les algorithmes de recherche, et en particulier MGAC, tout d’abord en équipant celui-ci d’heuristiques de choix de valeurs, souvent négligées par la communauté scientifique. Nous nous sommes pour cela basés sur l’heuristique de Jeroslow-Wang, bien connue dans le cadre de la résolution du problème SAT. En utilisant les deux techniques de conversion de problèmes CSP vers SAT les plus utilisées, nous sommes parvenus à montrer comment cette heuristique se comporterait sur le problème SAT issu de la conversion d’un CSP quelconque. Enfin, nous avons cherché à utiliser une hybridation entre un algorithme de recherche locale basé sur la pondération des contraintes et un algorithme MGAC, afin, d’une part, de mieux guider l’heuristique de choix de variables dom/wdeg, et, d’autre part, pour exploiter la réfutation de sous-arbres effectuée par MGAC via l’apprentissage de nogoods.

De manière transversale, l’ensemble des techniques développées dans le cadre de cette thèse a amené à la résolution d’une API pour le langage Java, capable de résoudre un CSP au sein d’une application Java quelconque. Cette API a été développée dans l’optique “boîte noire” : le moins de paramètres et d’expertise possibles sont demandés à l’utilisateur. Un prouveur basé sur CSP4J a concouru lors les compétitions internationales de prouveurs CSP avec des résultats encourageants.

Composition du jury

Rapporteurs

  • Philippe Jégou
  • Bertrand Neveu

Directeurs de thèse

  • Christophe Lecoutre
  • Lakhdar Saïs

Examinateurs

  • Éric Grégoire,
  • Chu Min Li