Explications pour les solveurs SAT

Les solveurs SAT sont devenus des outils largement utilisés pour résoudre des problèmes de décision ou d’optimisation combinatoires, dans le monde académique comme dans le monde économique. L’une des raisons de leur succès est de parcourir efficacement l’espace de recherche, que l’on peut représenter sous la forme d’un arbre. Ce type d'arbre peut être utilisé pour justifier qu’un problème de décision n’admet pas de solution (il est incohérent). L’objectif de cette thèse est de réduire autant que possible cet arbre afin d'atteindre une taille assimilable par un utilisateur. Pour atteindre ce but, nous proposons de reconnaître des redondances dans l'arbre de recherche en identifiant des sous-formules qui sont incohérentes et prouvées plusieurs fois comme telles au cours de la recherche. Lorsque l'arbre de recherche développé pour ces sous formules est de taille exponentielle, on peut obtenir une compression importante qui est de plus facilement explicable à l'utilisateur, ce qui justifie d'utiliser des méthodes coûteuses pour les identifier. Au cours de la thèse, nous avons principalement étudié deux approches. Dans un premier temps, nous nous sommes intéressés à la détection de formules incohérentes classiques au cours de la recherche : nous avons proposé un algorithme pour détecter des problèmes de pigeons, qui sont des problèmes d’appariements simples à expliquer à l’utilisateur mais dont l’arbre de recherche est exponentiel. Cet algorithme repose à la fois sur une reconnaissance syntaxique d’une partie du problème et d’une reconnaissance sémantique des exclusions mutuelles. En pratique, on retrouve peu d’instances de ce problème lors de la résolution de benchmarks des compétitions SAT. Dans un second temps, nous avons étudié une approche de détection syntaxique de sous formules incohérentes lors de l’exploration de l’espace combinatoire par le solveur. Cette fois-ci, nous avons utilisé un système de cache de formules incohérentes en détectant que la formule courante contient un sous-ensemble isomorphe à une entrée du cache déjà prouvée incohérente. Nous utilisons une réduction en isomorphisme de sous-graphes pour reconnaître les entrées de ce cache. Cette approche a été implémentée dans deux architectures de solveur SAT : DPLL et CDCL.Les approches proposées ont une complexité très élevée. En effet, d’un côté l’approche de détection de problèmes de pigeons implique une combinatoire importante, et de l’autre la reconnaissance de sous-formules déjà prouvées incohérentes nécessite de régulièrement résoudre une séquence de problèmes NP-complets d’isomorphismes de sous-graphes. De ce fait, nous ne parvenons à appliquer nos approches que sur un nombre limité de benchmarks et nous n’obtenons de bons résultats que sur des familles de benchmarks très structurées. Par contre, sur ces instances, la compression est impressionnante et donne des arbres qui sont de tailles réellement assimilables par l’utilisateur.