Contributions to SAT Solving

Contributions à la résolution des problèmes SAT Le problème de satisfaisabilité booléenne (SAT) est un défi fondamental en informatique aux implications profondes. Des solveurs SAT efficaces sont essentiels pour un large éventail d'applications, allant de la vérification formelle et de l'intelligence artificielle à la recherche opérationnelle et à la cybersécurité. Cependant, la complexité exponentielle de SAT pose des défis significatifs, en particulier pour les instances à grande échelle et hautement symétriques rencontrées dans les problèmes du monde réel. Cette thèse vise à améliorer l'efficacité et la performance des solveurs SAT en relevant les principaux défis liés à l'exploitation des symétries, à l'initialisation des variables et à la performance des solveurs. Les principales contributions de ce travail sont : Le développement d'une nouvelle approche hybride de bris de symétrie, ESBP_SEL, qui combine les prédicats de bris de symétrie effectifs (ESBP) avec l'apprentissage d'explications symétriques (SEL). En se concentrant sur les symétries locales, cette technique fournit une méthode plus nuancée et plus efficace sur le plan informatique pour élaguer l'espace de recherche, en particulier dans les instances SAT à grande échelle et hautement symétriques. L'introduction d'une approche basée sur un algorithme génétique, GASPI (Algorithme génétique pour l'initialisation de la polarité SAT), pour optimiser l'assignation initiale des polarités des variables. GASPI vise à fournir un point de départ plus intelligent pour le processus de résolution, guidant le solveur vers des régions prometteuses de l'espace de recherche. Une version améliorée, GASPI-ML, intègre des techniques d'apprentissage automatique pour prédire les paramètres optimaux de l'algorithme génétique en fonction des caractéristiques du problème. Les techniques proposées sont rigoureusement évaluées sur un large éventail de problèmes de référence et d'instances SAT du monde réel. Les résultats expérimentaux démontrent la supériorité d'ESBP_SEL par rapport aux méthodes ESBP et SEL autonomes, en particulier pour les instances insatisfiables présentant un degré élevé de symétrie. De plus, GASPI et GASPI-ML améliorent systématiquement les performances des solveurs SAT de pointe sur diverses instances de problèmes. En repoussant les limites de l'exploitation des symétries et de l'initialisation des solveurs, cette thèse ouvre de nouvelles voies pour résoudre efficacement les problèmes SAT complexes, avec des impacts potentiels dans de multiples domaines. Les idées et les techniques développées ici contribuent à la quête permanente d'expansion des horizons de la capacité de calcul dans la résolution SAT.