• Home
  • Page : 'emploi' inconnue (menus.php)

 Thesis : Vers un solveur SAT distribué efficace

PhD school thesis
La distribution de solveurs SAT est donc aujourd’hui un enjeu majeur, comme en témoigne la création pour la première fois d’une catégorie dédiée à la compétition internationale des solveurs SAT, avec le soutien d’Amazon EC2.
La conception de tels solveurs pourra s’inspirer des nombreux travaux menés par la com- munauté ces dernières années pour paralléliser la résolution des problèmes SAT afin d’exploiter au mieux les architectures multicœurs. Cependant elle pose de nouveaux problème en effet le coût de la communication sera bien plus important qu’en mémoire partagé. Les algorithmes devront donc être repensés pour optimiser les informations échangées entre les différentes ins- tances. Et dans ce domaine tout reste à faire, comme le montrent les résultats de la compétition où, malgré l’utilisation de 100 machines, les meilleurs participants n’ont été qu’à peine plus performants que les solveurs parallèles multicoeurs.
L’objectif de cette thèse est donc de concevoir et implémenter un solveur SAT distribué réellement efficace. Pour y arriver, le doctorant devra non seulement repenser les algorithmes du solveur, mais aussi attacher une très grande importance à l’efficacité de la distribution, tout en gardant à l’esprit que chaque noeud exécute un solveur multithreadé. Les problèmes de synchronisation, tant locales que distants, seront donc au cœur de cette thèse.

Ce projet de recherche doctoral fait l’objet d’une demande de financement auprès de « Ecole Doctorale d‘Informatique, Télécommunication et d‘Electronique (EDITE) », le candidat retenu par son porteur devra donc participer au concours correspondant (prévoir un dossier et une audition) en vue d’obtenir le financement effectif.

More details here

Contact :Souheib Baarir, Claude Dutheillet