Parallélisation CSP / SAT (Stage Master 2)

30 Novembre 2024

Nouvelles les plus récentes

(Liste de toutes les brèves)

Entretien Hebdo Eco à TV7

(20 Février 2025)

Mercredi dernier, j'ai pu répondre aux questions de Stéphanie Lacazze, de Sud Ouest, dans le cadre de l'[hebdo éco](https://www.sudouest.fr/lachainetv7/economie/l-hebdo-eco/) de TV7. C'est une chaîne de TV locale du groupe Sud...


Lancement du Diplôme d'Établissement en IA

(13 Février 2025)

Le diplôme d'établissement "Experts en I.A." vient de prendre corps, tout juste le lendemain du sommet de l'IA à Paris (un temps d'avance !). Cette formation a été proposée grâce...


Page sur la Convention IA

(9 Février 2025)

Après des mois de travaux préliminaires, nous lançons officiellement le recrutement d'étudiants pour la convention citoyenne étudiante qui aura lieu dans les locaux de Bordeaux Métropole le Week End du...


IA dans la Formation Initiale

(30 Janvier 2025)

L’IA et la formation : de l’université au monde professionnel Avec Juliette Mattioli, "Expert Fellow" en IA chez Thalès, nous avons eu le plaisir de présenter, en deux heures, les...


IA & Formations

(24 Janvier 2025)

Dans le cadre d'une série de rencontres et de conférences organisées par France Travail (avec plus de 400 visiteurs au total), dans les locaux de Bordeaux Métropole, j'ai eu le...

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)