Abstract

Le problème de satisfiabilité booléenne (SAT) est un défi central en informatique, avec des applications en vérification formelle, intelligence artificielle, recherche opérationnelle et cybersécurité. Sa complexité exponentielle reste un frein majeur, en particulier pour les instances de grande taille. Le travail présenté explore deux leviers pour améliorer l'efficacité des solveurs SAT. Le premier est une approche hybride de cassage de symétrie combinant prédicats effectifs et apprentissage d'explications symétriques, permettant un élagage plus fin de l'espace de recherche en ciblant les symétries locales. Le second utilise un algorithme génétique — enrichi par apprentissage automatique — pour optimiser l'initialisation des polarités des variables et orienter le solveur vers des régions prometteuses dès le départ. Ces approches ont été testées sur un ensemble d'instances de référence et de problèmes réels, et les résultats obtenus se sont révélés prometteurs. Cette présentation détaillera ces contributions et leurs perspectives pour la résolution de problèmes SAT.