Le Problème de Satisfiabilité Booléenne (SAT) demeure une pierre angulaire de l'informatique, avec des applications couvrant la vérification formelle, l'intelligence artificielle, la recherche opérationnelle et la cybersécurité. Malgré des avancées significatives dans les techniques de résolution SAT, la nature exponentielle de l'espace de recherche continue de poser des défis, particulièrement pour les instances à grande échelle rencontrées dans les applications réelles. Cette thèse présente deux approches pour améliorer l'efficacité des solveurs SAT.
La première contribution introduit ESBP_SEL, une nouvelle approche hybride qui combine les Prédicats de Rupture de Symétrie Efficaces (ESBP) avec l'Apprentissage d'Explications Symétriques (SEL) à travers le concept de symétries locales. Les résultats expérimentaux démontrent qu'ESBP_SEL surpasse significativement les méthodes existantes sur les instances hautement symétriques, particulièrement celles qui sont insatisfiables.
La seconde contribution aborde le problème d'initialisation dans les solveurs SAT CDCL à travers une série d'approches basées sur les algorithmes génétiques. L'approche de base, GASPI (Algorithme Génétique pour l'Initialisation de la Polarité SAT), utilise le calcul évolutionnaire pour identifier les affectations initiales de variables prometteuses. Celle-ci est encore améliorée dans GASPI-ML, qui utilise des techniques d'apprentissage automatique pour prédire les paramètres optimaux de l'algorithme génétique basés sur les caractéristiques de la formule ; et dans GASPI+, un algorithme génétique auto-adaptatif.
Ces techniques montrent une amélioration par rapport aux méthodes d'initialisation traditionnelles, particulièrement sur les instances satisfiables.
En repoussant les limites de l'exploitation de la symétrie et de l'initialisation des solveurs, cette thèse ouvre de nouvelles voies pour aborder efficacement les problèmes SAT complexes, avec des impacts potentiels dans de multiples domaines. Les perspectives et techniques développées ici contribuent à la quête continue d'expansion des horizons de la capacité computationnelle dans la résolution SAT.