Le but de cette thèse consiste tout d'abord à étudier les méthodes de parallélisation du problème SAT et les algorithmes de types essaims d'abeilles ou colonies de fourmis. Une fois cette étude faite, nous proposons une nouvelle approche de parallélisation du problème SAT basée sur les essaims d'abeilles. Chaque abeille est associée à un démonstrateur SAT (de différents types : CDCL, recherche locale, look ahead) et à chaque étape un certain nombre d'informations sont échangées afin d'améliorer les insectes pour l'étape suivante. De plus chaque abeille travaillera sur un sous problème du problème original décomposé sous forme de cubes. Ce sujet comprte 4 étapes principales :

  • La première étape consiste à caractériser l'état dans lequel se trouve un solveur. Plus précisément, à déterminer si le démonstrateur est proche ou pas de la solution. Cette étape nécessite des connaissances en statistiques et probabilités. Dans le même temps, il est nécessaire de déterminer le type d'informations que les démonstrateurs peuvent s'échanger (valeur des heuristiques, clauses apprises, équivalences entre littéraux...).
  • Ensuite, un premier prototype de colonies d'abeilles travaillant sur des sous-formules de la formule initiale sera implanté. Cette implantation sera réalisée dans un cluster de machines (chaque abeille sera associé à un noeud du cluster).
  • La troisième étape généralisera l'approche précédente à d'autres paradigmes combinatoires comme les problèmes CSP, les pseudo booléens
  • Enfin, une mise en place d'un service dans le cloud sera étudier. Ce service pourra faire plus que lancer des problèmes combinatoires sur des colonies d'abeilles. En effet, il pourra dans le même temps apprendre des informations relatives aux formules comme cela est fait dans les algorithmes de type portfolio comme Satzilla