Le mercredi 13 mai 2015 à 14:00 en salle 201, Jerry Lonlac viendra présenter ses travaux de recherche sur le problème SAT.
Le problème SAT est un problème fondamental en théorie de la complexité. Il est aujourd'hui utilisé dans de nombreux domaines comme la cryptanalyse, la planification, la bio-informatique, la vérification de matériels et de logiciels. En dépit d'énormes progrès observés ces dernières années dans la résolution pratique du problème SAT grâce à la puissance des solveurs SAT, la preuve de la satisfiabilité ou de l'insatisfiabilité de plusieurs problèmes reste un défit intéressant. En effet, de nombreux problèmes industriels restent hors de portés de tous les solveurs contemporains. Ainsi, il existe encore une forte demande d'algorithmes efficaces pouvant permettre de résoudre ces problèmes difficiles.
Dans la première partie de cet exposé, nous présentons une méthode de résolution basée sur une technique de substitution dynamique de fonctions booléennes détectés lors d'une phase de pré-traitement. Cette approche permet de mimer de façon élégante la résolution étendue un des plus puissants systèmes de preuve par résolution. Les fonctions booléennes exploitées correspondent à celles introduites lors de la phase d'encodage CNF grâce à l'application du principe de Tseitin.
Dans la deuxième partie, nous nous intéressons à un autre composant des solveurs SAT modernes, à savoir la stratégie d'élimination des clauses apprises déduites par résolution à chaque conflit. En effet, Le nombre des ces clauses croît de manière exponentielle rendant nécessaire d'éliminer régulièrement certaines, jugées non pertinentes, afin de maintenir une propagation unitaire efficace. Dans ce cadre, nous revisitons les différentes stratégies de gestion des clauses apprises. Nous proposons également de nouvelles stratégies originales combinant de manière astucieuse la longueur des clauses et la randomisation afin d'éliminer les clauses non pertinentes. Ces différentes stratégies sont conçues en considérant qu'une clause est pertinente pour la suite de la recherche si elle est courte et implique des littéraux affectés en haut de l'arbre de recherche
