Parallélisation CSP / SAT (Stage Master 2)

30 Novembre 2024

Nouvelles les plus récentes

(Liste de toutes les brèves)

Entretien dans le Hors Série Science et Vie sur l'IA

(20 Octobre 2025)

Cela fait déjà quelques temps que j'ai le privilège de répondre, parfois, aux questions de journalistes au sujet des impacts de l'IA sur la société, grâce à la chaire IA...


Après Midi IA-ACT de la Chaire IA Digne de Confiance

(6 Octobre 2025)

Le 13 Octobre : après-midi de présentation et d'échanges sur l'IA Act ! **Écouter, questionner et comprendre l'IA-Act** - Un après-midi d'explications, d'éclairages théoriques et de retours d’expériences appliqués pour...


Table Ronde Science & Vie - Fête de la Science

(1 Octobre 2025)

La veille du lancement officiel de la fête de la science 2025, et dans les locaux du Ministère de l'Enseignement Supérieur, j'ai pu participer à un table ronde organisée par...


Formation à l'I.A. à l'Aérocampus

(4 Juillet 2025)

L'aérocampus de Nouvelle Aquitaine est un centre de formation pour les techniciens de l'aéronautique. C'est un campus à part, où l'industrie y est prépondérante. On y monte et démonte des...


Jury d'agrégation 2025

(23 Juin 2025)

Depuis 2022, la France s'est enfin dotée d'une agrégation externe d'informatique. Je me souviens (au collège) de mes cours d'informatique (sur des PC équipés de disques souples 5"1/4 et des...

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

(Dernière Modification: 22 Février 2025 )
(english version)
(liste de toutes les brèves)