• Thèse soutenue le :
  • 2014-12-10

Résumé

Cette thèse présente différentes techniques permettant de résoudre le problème de satisfaction de formule booléenes utilisant le parallélisme et du calcul distribué. Dans le but de fournir une explication la plus complète possible, une présentation détaillée de l’algorithme CDCL est effectuée, suivi d’un état de l’art. De ce point de départ, deux pistes sont explorées. La première est une amélioration d’un algorithme de type portfolio, permettant d’échanger plus d’informations sans perte d’efficacité. La seconde est une bibliothèque de fonctions avec son interface de programmation permettant de créer facilement des solveurs SAT distribués.

Composition du jury

Rapporteurs

  • SIMON Laurent, Université de Bordeaux
  • DEQUEN Gilles, Université de Picardie Jules Vernes

Examinateurs

  • KATSIRELOS George, Institut national de la recherche agronomique, Toulouse
  • AUDEMARD Gilles, Université d’Artois (directeur de thèse)
  • JABBOUR Saïd, Université d’Artois (co-encadrant de thèse)
  • PIETTE Cédric, Université d’Artois (co-encadrant de thèse)