Master 2013 2014
Stages de la spécialité SAR
Analyse d’énoncés GAL avec un SAT solver


Site :Trac-Analyse d’énoncés GAL avec un SAT solver
Lieu :Jussieu, UPMC - LIP6, 25/26 2eme étage
Encadrant : Yann Thierry-Mieg, Souheib Baarir

Description

L’objectif du stage est de réaliser une transformation d’un énoncé d’accessibilité GAL en une formule booléenne. Cette dernière sera exprimée sous une forme normale conjonctive (une conjonction de disjonctions de variables booléennes). La résolution d’une telle formule est réalisée par un SAT-solveur (Minisat, glucose,…). Une technologie qui devient très puissante et permettant de résoudre des problèmes à forte combinatoire. La réalisation de la transformation permettra, donc, de se comparer aux performances de l’outil existant, utilisant des technologies basées sur les diagrammes de décision (BDD).

Cf. Détails dans le pdf joint.