Fiche de VALLADE Vincent

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