Projets scientifiques

La résolution du problème SAT est au cœur de la vérification formelle, de la planification, de la cryptanalyse et de nombreuses applications industrielles. Painless (https://lip6.github.io/painless/), développé au LIP6, est un cadre reconnu qui permet de paralléliser des solveurs séquentiels de l'état de l'art (Kissat, CaDiCaL, etc.) et d'expérimenter librement des stratégies de partage de clauses apprises. Son extension distribuée, D-Painless, étend cette approche à des grappes de plusieurs centaines de cœurs. Récemment, l'introduction du runtime AMP a doté D-Painless d'une couche de communication asynchrone unifiée, tolérante aux pannes (MPI/ULFM), qui libère entièrement les stratégies de partage des détails de la programmation réseau. Une première campagne sur Grid'5000 (960 workers, 20 nœuds) a montré que cette architecture augmente sensiblement le nombre de formules résolues et réduit les temps de résolution, sans aucune régression de correction. Cette approche a été validée de façon continue par la SAT Competition, référence internationale du domaine. Les solveurs construits avec Painless y figurent chaque année parmi les meilleurs de la track parallèle : troisième en 2018, premier et deuxième en 2020 (P-MCOMSPS-STR), premier en 2021 (P-MCOMSPS), premier et deuxième en 2024 (Painless avec PRS, BVA et Kissat, premier à la fois sur les instances SAT et UNSAT), et deuxième en 2025 (PL-PRS-Kissat), à quelques points seulement de MallobSat. En 2025, l'équipe a également engagé une variante fondée sur GASPI plutôt que MPI, classée quatrième, préfigurant l'axe de portabilité du transport porté par ce projet. Le projet vise à franchir l'étape suivante : faire de D-Painless la plateforme de référence pour la recherche et l'usage du SAT distribué, capable de passer de quelques centaines à plusieurs milliers de cœurs, de s'adapter dynamiquement aux ressources disponibles, et de produire des résultats expérimentaux reproductibles de bout en bout.

Il s’agit de : – écrire une fonction de "dépliage" transformant un réseau d'automates synchronisés en un automate équivalent – étudier et améliorer la déclaration et l'utilisation de templates pour en particulier déclarer un ensemble de transitions synchronisées avec un quantificateur – concevoir la syntaxe pour la hiérarchie et les liens père-fils, avec une attention particulière sur les variables et horloges globales/locales – interfacer dans CosyVerif avec cette structure hiérarchique (à plusieurs niveaux) – traduire en réseau d'automates (1 niveau).