- >Recherche
- >Études doctorales et HDR
- >Soutenir sa thèse
- >Les soutenances
- >Suruthy SEKAR
Soutenance de thèse de Madame Suruthy SEKAR
Le 20 novembre 2025 de 14:00 à 17:00
14h00 | Faculté des Sciences | Bâtiment L | Amphi L003 | 2, boulevard Lavoisier | ANGERS
Sujet : Hybridation SAT/CP : Approches Hybrides pour la Résolution de Problèmes de Satisfaction et d’Optimisation de Contraintes
Directeur de thèse : Monsieur Éric MONFROY
RÉSUMÉ
Cette thèse se place dans le contexte de l’hybridation entre deux paradigmes de résolution de problèmes combinatoires : le problème de satisfiabilité booléenne (SAT) et la Programmation par Contraintes (CP, de l’anglais Constraint Programming). Ces deux approches, qui définissent deux façons de résoudre des problèmes similaires, présentent des avantages et des inconvénients spécifiques. L’objectif de cette recherche est d’explorer des techniques d’hybridation qui intègrent le meilleur atout de SAT, l’analyse de conflit, dans un environnement CP, afin de tirer parti de son expressivité. Cette forme d’hybridation nécessite l’utilisation d’explications paresseuses. Ces explications peuvent être génériques, mais profitent grandement à être spécifiques à la contrainte utilisée. Cela introduit la première contribution de cette thèse, où nous développons et expérimentons l’élaboration d’explications pour la contrainte globale Somme. La deuxième contribution marque un tournant ; déplaçant l’attention des problèmes de satisfaction vers les problèmes d’optimisation. Cette contribution s’intéresse plus particulièrement aux cores insatisfiables et leur rôle dans les stratégies de recherche linéaire. Nous proposons une nouvelle technique guidée par les cores insatisfiables, permettant d’éviter de nombreux appels au solveur. Cette approche repose sur l’idée que le core d’un problème insatisfiable est généralement plus simple à résoudre que le problème lui-même. Enfin, la troisième, et plus importante contribution de cette thèse porte sur les clauses hybrides issues des conflits, dans un contexte d’optimisation SAT/CP. Traditionnellement, les clauses générées lors d’un appel insatisfiable sont jetées, leur validité ne pouvant être vérifiée aisément. Nous développons ici une méthode permettant d’isoler l’influence de la contrainte associée à la fonction objectif et ainsi étendre la validité des clauses au-delà des approches actuelles.
