Etude des Mécanismes de Transformation de Modèles CSP/SAT

A Study on the CSP/SAT Model Transformation Mechanisms La plupart des problèmes combinatoires peuvent être formulés comme des CSP (Constraint Satisfaction Problems). Un CSP est défini par des variables et des contraintes entre ces variables. Résoudre un CSP consiste à trouver une affectation des variables qui satisfasse les contraintes. L’une des principales forces des CSP est la déclarativité : les variables peuvent être de plusieurs types ainsi que les contraintes. D’un autre côté, le problème de satisfiabilité en logique propositionnelle (SAT) est réduit, en terme de déclarativité, à des variables booléennes et des formules propositionnelles. Cependant, les solveurs SAT sont maintenant capables de manipuler d’énormes instances.Il semble donc intéressant de 1) coder les CSP en SAT afin de bénéficier de l’expressivité et de la déclarativité des CSP et de la puissance des solveurs SAT, et 2) introduire plus de sémantique du problème initial dans SAT.Cette thèse analyse les encodages CSP vers SAT afin de mieux comprendre les facteurs clés qui déterminent leurs caractéristiques ainsi que leur impact sur la résolution. Une première étude analyse l’impact des variables venant du modèle CSP sur l’heuristique de branchement des solveurs SAT. Une étude sur la manière de transférer de l’information sémantique du modèle CSP au modèle SAT est aussi réalisée. Un travail est aussi réalisé sur l’intégration dans le modèle SAT d’un propagateur CSP pour l’addition. Pour finir, nous proposons l’encodage Abacus, un nouvel encodage SAT qui établit un bon compromis entre la taille des instances générées et l’efficacité de la résolution.