Direction de recherche : Fabrice KORDON

Co-encadrement : BAARIR Souheib, KORDON Fabrice, SOPENA Julien

Vers une parallélisation efficace de la résolution du problème de satisfaisabilité

Les solveurs résolvants le problème de SATisfiabilité booléenne sont utilisés avec succès dans de nombreux contextes : vérification de programmes et de matériels, cryptographie, bio-informatique, preuve automatique de théorème, etc. Ceci est dû à leur capacité à résoudre d'énormes problèmes pouvant contenir des millions de variables et des dizaines de millions de contraintes. Alors que la plupart des solveurs SAT ont longtemps été séquentiels, l'émergence des machines multi-cœurs a ouvert de nouvelles perspectives dans ce domaine.

Il existe de nombreux solveurs SAT parallèles différents par leurs stratégies, langages de programmation, bibliothèques utilisées, etc. Il est donc difficile de comparer l'efficacité de différentes stratégies dans un cadre unifié et équitable. De plus, l'introduction de nouvelles approches nécessite une compréhension approfondie de l'implémentation des solveurs déjà existants.

Cette thèse présente Painless : une plateforme générique et modulaire permettant l'implémentation de solveurs SAT parallèles efficaces pour les machines multi-cœurs. Elle offre une implémentation des composants de base et sa modularité permet aux utilisateurs de créer facilement leurs solveurs parallèles basés sur de (nouvelles) stratégies.

Painless a permis de construire et tester de nombreux solveurs. Nous avons pu imiter le comportement de trois solveurs de l'état de l'art tout en factorisant de nombreuses parties du code. L'efficacité de Painless a été soulignée par le fait que ces implémentations sont au moins aussi efficaces que les originales. De plus, lors de la participation à la compétition annuelle internationale de solveurs SAT parallèles, l'un de nos solveurs s'est classé 3ème en 2017 et un autre 1er en 2018.

Nous avons utilisé Painless pour mener des expériences équitables avec des solveurs de type diviser pour régner. Celles-ci nous ont permis de mettre en lumière des compositions originales d'heuristiques plus performantes que celles déjà présentes dans l’état de l’art.

Enfin nous avons été en mesure de créer et tester de nouvelles stratégies exploitant la structure modulaire des formules SAT. L'approche que nous avons proposée utilise la topologie de la formule pour guider le solveur vers des zones plus riches en informations, permettant ainsi l’accélération de la résolution parallèle du problème.

Publications 2017-2020

• 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)
• 2019
  • L. Le Frioux : “Vers une parallélisation efficace de la résolution du problème de satisfaisabilité”, soutenance de thèse, soutenance 03/07/2019, direction de recherche Kordon, Fabrice, co-encadrement : Baarir, Souheib, Kordon, Fabrice, Sopena, Julien (2019)
  • L. Le Frioux, S. Baarir, J. Sopena, F. Kordon : “Modular and Efficient Divide-and-Conquer SAT Solver on Top of the Painless Framework”, TACAS 2019 - 25^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 11427, Lecture Notes in Computer Science, Prague, Czechia, pp. 135-151 (2019)
• 2017
  • L. Le Frioux, S. Baarir, J. Sopena, F. Kordon : “PaInleSS: a Framework for Parallel SAT Solving”, The 20^th International Conference on Theory and Applications of Satisfiability Testing, vol. 10491, Lecture Notes in Computer Science, Melbourne, Australia, pp. 233-250, (Springer) (2017)