MASTER DAPM - D22. Examen de TP.

Mercredi 2 Mars 2016 - 09:00 → 13:00 (durée 3H00)  DOCUMENTS INTERDITS

Vous avez 1/4 d'heure pour vous installer et lire en détail le contenu de ce paragraphe avant de commencer les exercices ! Lisez attentivement les énoncés et suivez scrupuleusement les instructions en respectant à la lettre les commandes, les noms des fichiers proposés, majuscules/minuscules comprises.

Suggestion : copiez les à la souris afin d'éviter, entre autres, de confondre la quote ' et l'antiquote `. Les réponses aux questions éventuelles doivent être incorporées aux fichiers sources C sous forme de commentaires en début de programme.

NB. Si vous n'avez pas réussi à suivre les instructions ci-dessus et que je dois intervenir pour faire ce travail à votre place, je retirerai 5 points à votre note.

OBJECTIF DE L'EXAMEN : Écrire un programme de résolution du problème 3-SAT basé sur le principe du retour en arrière (backtracking).

Avant de commencer, récupérez le fichier sat.lex et le fichier makefile. En l'état ce programme lit un fichier texte contenant les clauses du problème 3-SAT et les range dans un tableau. Vous devrez utiliser les variables prédéfinies suivantes, dont certaines seront déjà initialisées par le programme sat :

  1. la variable nbclauses qui contient le nombre de clauses reconnues par flex;
  2. le tableau Clauses qui contient les nbclauses clauses sous forme de triplets d'entiers de type tclause;
  3. le tableau Verite qui contient à l'entrée i la valeur de vérité de la variable ui;
  4. le tableau EstLibre qui indique si la variable ui est libre ou non.
  5. la variable nbvars qui contient le nombre de variables booléennes utilisées;

Chaque ligne du fichier texte contient une clause sous la forme d'un triplet (a,b,c) où a, b et c sont des entiers relatifs dont la valeur absolue indique le numéro de la variable. Si l'entier est négatif, il désigne la négation de la variable. Par exemple (-2,3,5) code la clause C = {u2, u3, u5}. Si vous utilisez n variables booléennes pour décrire vos clauses, ces variables doivent impérativement être numérotées de 1 à n. Par convention, une clause ne peut contenir que des littéraux associés à des variables différentes.

Une variable clause de type tclause est un enregistrement contenant 3 valeurs entières positives x, y et z codant les indices des variables qui constituent les trois littéraux de la clause. Le codage est le suivant :

  1. Si le littéral est positif et associé à la variable i, alors la valeur est 2i;
  2. Si le littéral est négatif et associé à la variable i, alors la valeur est 2i + 1.

Autrement dit, le bit de poids faible indique s'il s'agit d'un littéral négatif ou non. Ainsi, pour la clause C = {u2, u3, u5} associée au triplet (-2,3,5) du fichier analysé, le codage est x = 5, y = 6 et z = 10. Pour le reste, le rôle des variables, types, structures et fonctions du code C fourni dans le programme C sont commentées et explicites. Vous n'aurez pas à modifier ces fonctions, simplement à rajouter celles qui seront nécessaires à la résolution du problème.

Écrivez une fonction CompterVar() qui renvoie le nombre de variables utilisées dans les clauses analysées. Initialisez alors la variable nbvars.
Écrivez une fonction InitTables() qui initialise deux tables de nb + 1 valeurs booléennes :
  1. une table de vérité Verite à 0;
  2. une table EstLibre à 1.

Attention ! pour plus de commodité, les deux tables sont indexées par le numéro de la variable, la cellule 0 est donc inutilisée puisque la numérotation commence à 1. Il faut donc bien allouer 1 cellule de plus que le nombre de variables.
Écrivez une fonction EvalClause(clause) qui renvoie 0 ou 1 selon que clause est satisfaite ou non pour la table de vérité Verite.
Résolvez le problème de satisfaisabilité de ces clauses à l'aide d'une fonction récursive Sat() dont vous fixerez les paramètres et qui utilisera le principe du backtracking. Commentez votre/vos fonction(s) et expliquez clairement ce que fait votre programme !
Votre fonction modifiera les valeurs dans la table de vérité Verite pour satisfaire une-à-une les nbclauses clauses. La base récurrente de votre fonction de backtracking sera atteinte quand toutes les clauses auront été satisfaites. Dans ce cas vous afficherez la table de vérité. Dans le cas contraire l'ensemble des clauses n'est pas satisfaisable.

Indications : Pour satisfaire une clause, il faudra nécessairement satisfaire l'un des trois littéraux de la clause puis passer à la clause suivante avec un appel récursif. Si la valeur d'une variable booléenne a été fixée dans la table de vérité Verite pour satisfaire un littéral de la clause, cette variable ne sera plus libre pour satisfaire les clauses suivantes, vous devrez donc utiliser la table de booléens EstLibre pour indiquer quelles variables sont encore libres ou non.

Le principe est globalement le même que pour le programme des huit reines. Pour chaque ligne de l'échiquier on cherchait la première colonne libre pour placer une reine avant de passer à la ligne suivante, ici pour chaque clause, on essaie de satisfaire l'un des trois littéraux avant de passer à la clause suivante.
L'instance test.sat est-elle satisfaisable ? Si oui, fournissez une table de vérité.
Quelle est la complexité de votre algorithme ?