Un solveur hybride pour la résolution pratique de SAT

International audienceLa programmation par contraintes est un paradigme de résolution très puissant, permettant de modéliser de nombreux problèmes dans différents domaines tels que les interfaces personne-machine, l'intelligence artificielle ou encore la recherche opérationnelle. Parmi ces langages de représentation, le langage des formules propositionnelles mises sous forme normale conjonctive (ou langage SAT) permet de modéliser et de résoudre de nombreux problèmes. Depuis l'avènement des solveurs CDCL (pour " Conflict Driven, Clause Learning "), le formalisme SAT est utilisé avec succès pour la résolution de problèmes applicatifs (vérification formelle bornée, gestion de dépendance, etc.). Ces méthodes sont effectivement très performantes sur les problèmes industriels, mais ne sont par exemple pas adaptées à la résolution de problèmes aléatoires, où les méthodes de recherche locales (RL) sont les plus efficaces. Une comparaison de ces deux paradigmes de recherche (CDCL et RL) montre que les avantages et les inconvénients de l'un correspondent respectivement aux inconvénients et aux avantages de l'autre, faisant de ces deux méthodes de potentiels partenaires complémentaires. Partant de ce constat, nous avons hybridé ces deux types d'approche afin d'en combiner les avantages. Nous étudierons et montrerons expérimentalement que notre approche est performante, en comparaison avec d'autre solveurs de l'état de l'art