Informations professionnelles
Statut: Docteur ED
ED: EDITE
Unité de recherche: LIP6
Employeur: Sorbonne Université
Date de debut de thèse: 1 octobre 2018
Date soutenance de thèse: 27 juin 2023
Directeur de thèse: Fabrice KORDON (LIP6)
Directeur de thèse: Souheib BAARIR (LIP6)
Encadrant : Julien SOPENA (LIP6)
Sujet de thèse: Groupes de partage pour solveurs SAT parallèles
ED: EDITE
Unité de recherche: LIP6
Employeur: Sorbonne Université
Date de debut de thèse: 1 octobre 2018
Date soutenance de thèse: 27 juin 2023
Directeur de thèse: Fabrice KORDON (LIP6)
Directeur de thèse: Souheib BAARIR (LIP6)
Encadrant : Julien SOPENA (LIP6)
Sujet de thèse: Groupes de partage pour solveurs SAT parallèles
Soutenance de thèse
Données générales
Titre : Contribution à la résolution parallèle du problème SAT
Date : 27 juin 2023
Heure: 10:00
Résumé : Cette thèse présente des contributions multiples et orthogonales à l'amélioration de la résolution parallèle du problème de satisfiabilité booléenne (ou problème SAT). Les contributions apportées par cette thèse se concentrent sur la qualité du partage de l'information entre les différents travailleurs d'un solveur SAT parallèle. Une première contribution présente une méthode efficace pour mettre en œuvre un algorithme asynchrone de réduction de la taille de l'information partagées. Une deuxième contribution combine les informations extraites de la structure particulière de la formule propositionnelle avec les informations extraites dynamiquement pendant la résolution du problème par le solveur afin de créer un filtre qui maximise la qualité de l'information partagée. Enfin, une dernière contribution porte sur l'intégration d'un composant permettant de déterminer de manière probabiliste la valeur de vérité des variables permettant de rendre une formule satisfaisable.
Lieu : Sorbonne Université, 4 place Jussieu 75005 Paris Couloir 25-26, 1er étage, salle 105
Date : 27 juin 2023
Heure: 10:00
Résumé : Cette thèse présente des contributions multiples et orthogonales à l'amélioration de la résolution parallèle du problème de satisfiabilité booléenne (ou problème SAT). Les contributions apportées par cette thèse se concentrent sur la qualité du partage de l'information entre les différents travailleurs d'un solveur SAT parallèle. Une première contribution présente une méthode efficace pour mettre en œuvre un algorithme asynchrone de réduction de la taille de l'information partagées. Une deuxième contribution combine les informations extraites de la structure particulière de la formule propositionnelle avec les informations extraites dynamiquement pendant la résolution du problème par le solveur afin de créer un filtre qui maximise la qualité de l'information partagée. Enfin, une dernière contribution porte sur l'intégration d'un composant permettant de déterminer de manière probabiliste la valeur de vérité des variables permettant de rendre une formule satisfaisable.
Lieu : Sorbonne Université, 4 place Jussieu 75005 Paris Couloir 25-26, 1er étage, salle 105
Rapporteurs/ Rapporteuses
| Personne | Qualité | Etablissement |
|---|---|---|
| M. Klai Kais | Maître de Conférences (HDR) | Laboratoire d'Informatique de Paris Nord |
| M. Couvreur Jean-michel | Professeur des universités | Laboratoire d'Informatique Fondamentale d'Orléans, Univ. d'Orléans |
Composition du jury
| Personne | Qualité | Etablissement |
|---|---|---|
| M. Klai Kais | Maître de Conférences (HDR) | Laboratoire d'Informatique de Paris Nord |
| M. Couvreur Jean-michel | Professeur des universités | Laboratoire d'Informatique Fondamentale d'Orléans, Univ. d'Orléans |
| Mme. Klaudel Hanna | Professeure des universités | Informatique, BioInformatique, Systèmes Complexes |
| M. Le berre Daniel | Professeur des universités | Centre de Recherche en Informatique de Lens, Univ. d'Artois |
| M. Sopena Julien | Maître de Conférences | LIP6, Sorbonne Université |
| M. Baarir Souheib | Maître de Conférences (HDR) | LIP6, Univ. de Nanterre |
| M. Kordon Fabrice | Professeur des universités | LIP6, Sorbonne Université |