Démarrage Février 2025
SAT, Logique, Programmation par Contraintes, Parallélisation
Localisation: LaBRI, Laboratoire Bordelais de Recherche en Informatique, Talence, France
(Ce stage de Master est financé par le Google Award 2024)
Description du projet de master proposé
Le résolution du problème SAT (Satisfiabilité d’une formule logique en logique propositionnelle) a connu des progrès considérables ces dernières années, malgré une quasi impossibilité théorique (SAT est l’archétype des problèmes NP-Complets). Ces progrès, illustrés notamment par les performances du SAT solveur Glucose [1] co-développé au LaBRI, se heurtent pourtant depuis quelques années aux nouveaux modèles architecturaux des machines. Il est en effet difficile d’exploiter au mieux les architectures parallèles, voire massivement parallèles, des machines récentes.
Ce stage vise à revisiter les méthodes actuelles de partage de travail des solveurs SAT, en se concentrant spécifiquement sur les formules SAT dérivées de problèmes initialement exprimés sous forme de contraintes, pouvant présenter des structures particulières, ou dont des méthodes plus haut niveau peuvent aider à analyser. L’étude se limite à une machine unique à mémoire partagée, excluant de l’étude le cas du cloud computing. Les approches récentes de parallélisation massive de SAT exploitent divers paradigmes de séparation de l’espace de recherche, parmi lesquels le “Cube and Conquer” [2]. Cette méthode consiste à diviser le problème principal en milliers, voire centaines de milliers, de sous-problèmes plus petits, qui sont ensuite distribués en fonction de la disponibilité des cœurs de calcul.
Dans ce stage, nous proposons d’étudier comment l’on peut profiter des calculs déjà effectués sur les coeurs pour sélectionner plus précisément le prochain sous problème à résoudre.
L’objectif de ce stage de Master 2 est de proposer des mesures permettant de partager les pour la résolution pratique du problème SAT.
[1] The Glucose SAT Solver, Gilles Audemard, Laurent Simon, IJAIT’s Volume No.27, Issue No. 01.2018
[2] Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads, Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A., HVC 2011. Lecture Notes in Computer Science, vol 7261.
(Le post annoncant l’obtention du Google Award).
Candidat
Le/La candidat.e devra avoir de solides connaissances en Programmation.
Contact: Laurent Simon