GHODBANE Mohamed Imad Eddine

Shared Clausebase for Manycore SAT Solving

Cette thèse traite du problème de satisfiabilité booléenne (SAT), un problème NP-complet central ayant des applications en vérification, en démonstration automatique de théorèmes et en bioinformatique. Bien que des approches parallèles telles que Divide and Conquer et Portfolio aient été explorées, les solveurs SAT existants s'adaptent mal aux machines manycore. Une limitation majeure réside dans l'utilisation de la mémoire : chaque instance du solveur conserve sa propre base de connaissances, entraînant une consommation excessive de mémoire lorsque le nombre de c?urs augmente. La recherche se concentre sur la conception de mécanismes de partage efficace de la mémoire entre les c?urs sans perte de performance. Cela implique la création de nouveaux algorithmes, de structures de données concurrentes et l'optimisation d'aspects bas niveau tels que la gestion de la mémoire et du cache. Une attention particulière sera portée à la base de clauses apprises (learnt-clause database), une structure très consommatrice de mémoire actuellement dupliquée sur chaque c?ur, qui pourrait être partagée de manière plus efficace.