Séminaire

Le problème SAT (une formule propositionnelle donnée sous forme normale conjonctive admet-elle une valuation qui la rende vraie ?) est un problème fondamental en théorie de la complexité. Il est aujourd’hui utilisé dans de nombreux domaines comme la bio-informatique, la cryptanalyse, la planification, 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 de SAT grâce à la puissance des démonstrateurs SAT, la preuve de la satisfiabilité ou de l’insatisfiabilité de plusieurs problèmes reste un défi intéressant. En effet, de nombreux problèmes industriels restent hors de portée de tous les démonstrateurs SAT 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épendances fonctionnelles entre variables) détectées 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 dépendances fonctionnelles 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 démonstrateurs SAT modernes, à savoir la stratégie d’élimination des contraintes (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. Dans ce cadre, nous revisitons quelques stratégies efficaces 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 au cours de la résolution. 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 variables affectées en haut de l’arbre de recherche.