Direction de recherche : Souheib BAARIR, Fabrice KORDON

Co-encadrement : SOPENA Julien

Groupes de partage pour solveurs sat parallèles

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). Une instance du problème SAT est une formule booléenne de forme particulière représentant, en général, les variables et les contraintes d'un problème du monde réel, tel que la planification multi-contraintes, la vérification matérielle et logicielle ou la cryptographie. La résolution du problème SAT consiste à déterminer s'il existe une affectation des variables qui permet de satisfaire la formule. Un algorithme capable de fournir une réponse à ce problème est appelé un solveur SAT. Cet algorithme a une complexité exponentielle, en effet le problème SAT est le premier problème à avoir été déterminé NP-complet. De nombreux algorithmes et heuristiques ont été développés pour accélérer la capacité de résolution de ce problème, principalement dans un contexte séquentiel. L’omniprésence de machines multicoeurs a encouragé des efforts considérables dans la résolution parallèle du problème SAT. Cette thèse s’inscrit dans le prolongement de ces efforts.
Dans le contexte parallèle, le partage d'informations est un élément clé de l'efficacité. Il est généralement mis en œuvre sous forme de nouveaux lemmes échangés entre les différents participants à la stratégie de résolution parallèle (c'est-à-dire les solveurs séquentiels sous-jacents).
Nous présentons dans cette thèse plusieurs stratégies pour améliorer ce partage. Premièrement, en affinant la sélection des informations à partager, grâce à l'exploitation de la structure des communautés exposées par les instances SAT du monde industriel. Deuxièmement, en ajoutant la possibilité de réduire la taille de l'information et de prévenir le partage d'informations redondantes.

Publications 2020-2023

• 2023
  • V. Vallade : “Groupes de partage pour solveurs sat parallèles”, soutenance de thèse, soutenance 27/06/2023, direction de recherche Baarir, Souheib Kordon, Fabrice, co-encadrement : Sopena, Julien (2023)
• 2020
  • V. Vallade, L. Le Frioux, S. Baarir, J. Sopena, V. Ganesh, F. Kordon : “Community and LBD-Based Clause Sharing Policy for Parallel SAT Solving”, SAT 2020 - 23^rd International Conference on Theory and Applications of Satisfiability Testing, vol. 12178, Lecture Notes in Computer Science, Alghero / Virtual, Italy, pp. 11-27 (2020)
  • V. Vallade, L. Le Frioux, S. Baarir, J. Sopena, F. Kordon : “On the Usefulness of Clause Strengthening in Parallel SAT Solving”, NFM 2020 - 12^th NASA Formal Methods Symposium, Moffett Field / Virtual, United States (2020)