Table des matières

Introduction

Les 4 séances de TP de logique visent à implémenter un programme testant la satisfiabilité d'une formule mise sous forme normale conjonctive (CNF), c'est-à-dire sous la forme d'un ensemble de clauses. Un exemple de tel solveur est MiniSat. Ce programme sera ensuite utilisé pour vérifier un circuit d'additionneur représenté à partir d'une spécification, tous deux représentés par des formules.

Ce programme va explorer l'espace de recherche (les combinaisons de valeurs possibles pour les variables) afin de déterminer la satisfiabilité de la formule testée.

<note>Le projet est prévu pour être réalisé dans un environnement Unix (Linux ou Mac OS X). La compilation se fera via l'utilitaire make. Aucun support ne sera fourni pour la réalisation du projet sous Windows ni pour la compilation dans un IDE comme CodeBlocks (même s'il est possible d'utiliser ce dernier pour éditer les fichiers source).</note>

Modalités de rendu

Le projet est à rendre en deux fois (parties 1&2, puis parties 3&4).

Le rendu consistera en une archive .zip ou .tar.gz1), nommée nom1-num1-nom2-num2-intermediaire.zip2) ou nom1-num1-nom2-num2-final.zip, contenant:

Rendu intermédiaire

L'archive du rendu intermédiaire est à déposer sur spiral au plus tard le dimanche 23 novembre 2014 à 23h594). Il fortement recommandé de tester l'accès à la zone de dépôt avant la date butoir5).

Lien spiral pour le rendu intermédiaire: http://spiralconnect.univ-lyon1.fr/webapp/activities/activities.jsp?containerId=3668845

Rendu final

Cette archive est à déposer sur spiral au plus tard le mardi 23 décembre 2014 à 23h596).

La zone de dépôt pour le rendu final: http://spiralconnect.univ-lyon1.fr/webapp/activities/activities.jsp?containerId=3662577

<note important>Le non respect de ces consignes entraînera une sanction dans la note du projet.</note>

Projet de départ

L'archive lif11-2014-enonce.zip contient un projet C++. Ce projet de départ fourni contient une arborescence de projet avec :

<note tip>Il est demandé de ne pas héberger vos sources sur un dépôt public. L'UCBL met à votre disposition une forge avec un hébergement de dépôts mercurial. Le projet fourni7) peut être poussé vers cette forge.

</note>

Organisation du projet

Le projet est divisé en quatre grandes étapes qui correspondent grossièrement aux 4 séances de TP prévues :

<note tip>C'est le résultat de ces deux première parties qu'il faut rendre dans le cadre du rendu intermédiaire.</note>

<note important> Le projet est à réaliser seul ou en binôme. Les différentes étapes permettent aux étudiants de situer leur avancement. Avancer régulièrement et progresser hors des séances de TP afin que ces dernières vous soient le plus profitables possibles. Vous pouvez vous aider les uns les autres, en gardant à l'esprit que ceci n'implique pas de devoir s'échanger les sources entre binômes. </note>

Première partie : prise en main

<note warning> Pour de l'aide sur les bases du C++ utiles à ce TP voir :

</note>

Tests unitaires avec UnitTest++

Le projet est fourni avec la bibliothèque UnitTest++ qui simplifie (grandement) l'expression et la gestion de tests unitaires. Un test peut être vu comme une fonction sans arguments dont on attend que le résultat s'évalue à true. Dans UnitTest++ un test est une macro de la forme TEST(nom_du_test) { code du test }. Dans le corps de cette fonction/macro certaines assertions CHECK(test) sont vérifiées. Il est possible de faire autant de CHECK que l'on veut dans un TEST, possiblement aucun. Le fichier main-test.cpp contient l'exemple initial suivant : 

// Un test simple qui réussit
TEST(test1) {
  CHECK(2 == 1+1);
}
 
// Un test simple qui échoue
TEST(test2) {
  CHECK(2 == 1+2);
}

Le Makefile fourni dans le projet de départ permet d'exécuter les tests définis dans main-test.cpp simplement via make test.

Exercices

Forme normale conjonctive

Les structures codant les clauses et les formules conjonctives (que l'on abrégera désormais CNF pour Conjunctive Normal Form) sont définies par des typedef utilisant différents conteneurs de la STL. Une cnf_t est un tableau dynamique (vector) qui contient des clauses cls_t représentées par des ensembles de littéraux (set), les littéraux lit_t étant codés par des entiers. 

typedef unsigned int  var_t;
typedef int           lit_t;
typedef set<lit_t>    cls_t;
typedef vector<cls_t> cnf_t;

Exercices sur les clauses

Exercices sur CNF

Représentation des variables et des littéraux

Pour des raisons d'efficacité, il faut éviter de représenter les variables propositionnelles par des chaînes (classe string en C++) et leur préférer des entiers (var_t dans le projet).

Pour l'efficacité, on représentera également les littéraux (c'est-à-dire des variables avec ou sans négation) par des entiers :

Il faut ainsi prêter garder à ne pas mélanger la proposition dont la string est p avec sa représentation numérotée, par exemple 2, et les littéraux associés dont les formules sont p et ~p valant respectivement 4 et 5. Pour cela, il est vivement recommander d'utiliser systématiquement par la suite les fonctions var2lit et neg demandées en exercices.

Exercices sur les littéraux

<note important> Cette première partie donne les bases sur lesquelles s’appuyer dans la suite du projet. Ces bases doivent être solides. Bien garder les tests unitaires rédigés au fur et à mesure de l'avancement : ils permettent de s'assurer de la correction du code, de la non-régression lors des modifications et sont attendus dans le rendu final du projet comme la preuve que le programme a été convenablement testé. </note>

Deuxième partie : traduction

Représentation d'un emplois du temps

On considère une version simplifiée du problème d'emploi du temps suivant: on cherche à placer dans une semaine des cours dans des créneaux horaire en leur attribuant des salles et des enseignants. On dispose des disponibilités des enseignants, on sait quel cours peut être enseigné par quel enseignant. On suppose que les cours ont une durée d'une heure. On rappelle que deux cours ne peuvent pas avoir lieu dans la même salle en même temps et qu'un enseignant ne peut pas faire deux cours simultanément.

Notation: Dans la suite, les cours seront numérotés et notés Crs_1 … Crs_n, les enseignants Ens_1 … Ens_m, les créneaux Cx_1 … Cx_p et les salles Sl_1 … Sl_q .

La structure probleme définie dans edt.hpp donne accès aux nombres d'enseignants, de salles, de créneaux et de cours: 

struct probleme {
  int nb_enseignants;
  int nb_cours;
  int nb_creneaux;
  int nb_salles;
 
  ...
 
};

Pour traduire un problème d'emploi du temps en formule, on va s'appuyer sur les (tableaux de) variables booléennes suivantes:

Afin de pouvoir utiliser les bonnes variables lorsqu'on génèrera la CNF, on stocke celles-ci (en fait leur littéral positif) dans la structure suivante: 

// Structure stockant les littéraux qui représentent un emploi du temps.
struct lit_edt {
  // le littéral Cr_En[i][j] est vrai si l'enseignant Ens_j enseigne
  // le cours Crs_i.
  vector< vector<lit_t> > Cr_En; 
  // le littéral Cr_Sal[i][j] est vrai si le cours Crs_i a lieu
  // dans la salle Sl_j.
  vector< vector< lit_t> > Cr_Sal;
  // le littéral Cr_Cx[i][j] est vrai si le cours Crs_i a lieu
  // au créneau Cx_j.
  vector< vector<lit_t> > Cr_Cx;
};

<note tip> Exemple: cet exemple sera repris tout au long de la partie 2.

On considère un problème d'emploi du temps avec 3 cours (Crs_0, Crs_1 et Crs_2), 2 enseignants (Ens_0 et Ens_1), 2 salles (Sl_0 et Sl_1) et 2 créneaux (Cx_0 et Cx_1).

Cela correspond au fichier problème suivant (ne tenir compte que des 4 premières lignes jusque dans la sous-partie sur les contraintes explicites).

pb-simple5b.txt
enseignants: 2
salles: 2
creneaux: 2
cours: 3 
0 enseigne: 0,1,2
1 enseigne: 0,1
salle pour 0: 0
salle pour 1: 0
salle pour 2: 0,1
0 indisponible: 1

</note>

Exercices sur la représentation d'un emploi du temps

<note tip>Exemple:

On doit donc obtenir les 3 matrices suivantes.

Remarque: on ne stocke pas les variables mais les littéraux positifs qui leur correspondent d'où les saut de 2 en 2 sur les valeurs. Les variables portent les numéros 0 à 17, les littéraux les numéros de 0 à 35.

Matrice Cr_En

Crs\Ens 01
002
146
2810

Le littéral 4 (qui correspond à la variable 2) prend la valeur vrai11) si et seulement si le cours Crs_1 est enseigné par l'enseignant Ens_0. On peut dire que ce littéral code le fait “le cours Crs_1 est enseigné par l'enseignant Ens_0”.

Matrice Cr_Sal

Crs\Sal01
01214
11618
22022

Le littéral 18 prend la valeur vrai si et seulement si le cours Crs_1 a lieu dans la salle Sl_1.

Matrice Cr_Cx

Crs\Cx01
02426
12830
23234

On peut dire que le littéral 34 code le fait “le cours Crs_2 a lieu au créneau Cx_1” </note>

Contraintes implicites

Pour que l'emploi du temps soit correct, il doit respecter implicitement les contraintes suivantes:

  1. cours_salle_creneau: Il est impossible que deux cours différents aient lieu au même moment dans la même salle.
  2. enseignant_creneau: Un enseignant fait au maximum un cours dans un créneau horaire donné.
  3. cours_une_fois: Un cours a lieu exactement une fois.
  4. cours_une_salle: un cours a lieu dans exactement une salle.
  5. cours_enseignant: Un cours est donné par exactement un enseignant.

Chacune des contraintes ci-dessus peut-être codée par une ou plusieurs clauses portant sur les bons littéraux de la structure lit_edt.

Par exemple le fait que les cours Crs_1 et Crs_2 n'aient pas lieu en même temps dans la salle 3 au créneau 4 peut se coder par la clause suivante: (¬Cr_Sal_1_3 ⋁ ¬Cr_Cx_1_4 ⋁ ¬Cr_Sal_2_3 ⋁ ¬Cr_Cx_2_4): Soit le cours 1 n'a pas lieu dans la salle 3, soit pas pendant le créneau 4, soit le cours 2 n'a pas lieu dans la salle 3, soit pas pendant le créneau 4 (il est aussi possible qu'aucun de ces 2 cours n'ait lieu dans la salle 3 au créneau 4).

<note tip> Exemple:

En reprenant l'exemple “fil rouge” précédent, la clause qui code le fait que les cours Crs_0 et Crs_2 n'ont pas lieu en même temps dans la salle Sl_0 pendant le créneau Cx_1 est:

{13, 21, 27, 35}

avec:

</note>

Pour représenter le fait qu'un enseignant ne peut avoir deux cours en même temps, on pourra procéder de manière similaire à la contrainte n°1 en replaçant les salles par les enseignants.

Pour coder le fait qu'un cours a lieu exactement une fois, on procède en 2 étapes:

  1. On code le fait qu'il doit avoir lieu au plus une fois, c'est à dire qu'il ne peut pas avoir lieu à deux créneaux différents. Par exemple le cours Crs_1 ne peut pas avoir lieu aux créneaux Cx_2 et Cx_3: ( ¬Cr_Cx_1_2 ⋁ ¬Cr_Cx_1_3)
  2. On code le fait qu'il doit avoir lieu au moins une fois, c'est à dire pendant au moins un créneau. Par exemple le cours Crs_1 doit avoir lieu au créneau Cx_1 ou au créneau Cx_2 ou … ou au créneau Cx_p: (Cr_Cx_1_1 ⋁ Cx_Cx_1_2 ⋁ … ⋁ Cr_Cx_1_p)

<note tip>Exemple:

La clause disant que le cours Crs_1 ne peut pas avoir lieu aux créneaux Cx_0 et Cx_1 est {29, 31}

La clause disant que le cours Crs_1 doit avoir lieu dans au moins un créneau est {28, 30} </note>

Exercices sur les contraintes implicites

<note tip> Pour écrire les clauses dans un flux de sortie12), on pourra utiliser la fonction ecrit_clause_dimacs(ostream& output, const cls_t& clause) fournie dans dimacs.hpp. </note>

<note important> Le format dimacs utilise un codage des littéraux différent de celui utilisé en interne pour le projet.

:!: Vous n'avez pas à gérer directement ce format, les fonctions de lecture et d'écriture sont fournies dans dimacs.hpp/dimacs.cpp :!:

Dans ce codage un littéral est codé directement comme son numéro de variable, multiplié par -1 pour les les littéraux négatifs. Deplus, les variables sont numérotées à partir de 1, il y a donc un décalage de 1 entre les numéros de variable en interne et ceux utilisé en dimacs. Chaque ligne correspond à une clause et se termine par 0.

Par exemple la clause {0,5,12,15} sera représentée par la ligne suivante en dimacs:

1 -3 7 -8 0 </note>

Contraintes explicites

On va maintenant s'intéresser à coder les contraintes explicitement exprimées dans les fichiers de problèmes. Il y a 3 types de contraintes explicites (la syntaxe est décrite dans le fichier /Syntaxe-EdT.txt):

  1. Un enseignant peut enseigner certains cours. Si cette contrainte ne spécifie pas que c'est possible, un enseignant Ens_i ne peut pas enseigner un cours Crs_j.
  2. Un cours ne peut avoir lieu que dans certaines salles.
  3. Un enseignant n'est pas disponible a certains créneaux.

Une fois le fichier lu par la fonction lit_probleme, ces contraintes sont représentées dans la structure probleme partiellement présentée plus haut: 

struct probleme {
  int nb_enseignants;
  int nb_cours;
  int nb_creneaux;
  int nb_salles;
  // pb.enseigne[i]={j1,j2,...}
  // correspond à la contrainte "i enseigne: j1, j2, ..."
  vector< set<int> > enseigne; 
  // pb.salles[i]={j1,j2,...} correspond 
  // à la contrainte "salles pour i: j1, j2, ..."
  vector< set<int> > salles;
  // pb.indisponibilites[i]={j1,j2,...} correspond à la 
  // contrainte "i indisponible: j1, j2, ..."
  vector< set<int> > indisponibilites;
};

<note tip> Exemple:

Si on reprend le problème exemple:

pb-simple5b.txt
enseignants: 2
salles: 2
creneaux: 2
cours: 3 
0 enseigne: 0,1,2
1 enseigne: 0,1
salle pour 0: 0
salle pour 1: 0
salle pour 2: 0,1
0 indisponible: 1

on aura:

enseigne

Ens\Crs
0{0,1,2}
1{0,1}

L'enseignant Ens_0 peut enseigner tous les cours, alors que l'enseignant ne peut enseigner que les deux premiers.

salles

Crs\Salle
0{0}
1{0}
2{0,1}

Les cours Crs_0 et Crs_1 peuvent avoir lieu uniquement dans la salle Sl_0, alors que le cours Crs_2 peut avoir lieu partout.

indisponibilites

Ens\Cx
0{1}
1{}

L'enseignant Ens_0 est indisponible au créneau Cx_1, alors que l'enseignant Ens_1 est tout le temps disponible. </note>

Exercices sur les contraintes explicites

Traduction du problème

Coder la fonction ecrit_cnf_probleme(ostream& out, probleme& pb), qui utilise les autres fonctions de la deuxième partie pour traduire le problème en CNF:

Cette fonction est appelée par la fonction main du fichier main-edt.cpp.

Traduction d'un modèle en emploi du temps

Le programme edt doit également être capable de traduire un modèle de la CNF en solution au problème d'emploi du temps. La valeur des littéraux représentant l'emploi du temps permet de savoir pour chaque cours l'enseignant, la salle et le créneau qui lui ont été attribués. A partir de là il est possible de remplir pour chaque cours la structure affectation suivante: 

struct affectation {
  int enseignant; // numero de l'enseignant faisant cours
  int cours; // numero du cours
  int salle; // le numero de la salle
  int creneau; // le creneau concerné
};

Une solution au problème devient alors une liste d'affectations (codée via un vector<affectation>). Ecrire la fonction solution construit_solution(set<lit_t>& modele, probleme& pb) qui sera utilisée dans la fonction main de edt.hpp pour traduire un modèle en solution.

Le modèle est représenté par l'ensemble des littéraux dont la valeur est vrai. Les littéraux dont la valeur n'est pas dans l'ensemble valent donc faux.

<note tip> Exemple:

Supposons que le modèle trouvé par le solveur SAT soit le suivant: 

{1,2,5,6,8,11,12,15,16,19,21,22,25,26,28,31,32,35}

On rappelle les matrices correspondant au problème:

Matrice Cr_En

Crs\Ens 01
002
146
2810

Matrice Cr_Sal

Crs\Sal01
01214
11618
22022

Matrice Cr_Cx

Crs\Cx01
02426
12830
23234

Intéressons nous au cours Crs_0: les littéraux qui nous intéressent sont:

A partir de ces informations, on peut créer la bonne affectation pour le cours Crs_0:
{ enseignant → 1, cours → 0, salle→0, creneau→1 } </note>

La fonction construit_solution procédera comme suit:

Troisième partie: solveur SAT simple

<note tip>Exemples de CNF pour les problemes: pb-simple-cnf.zip.

</note>

Calcul de la valeur courante d'une CNF

Au cours de l'exploration de l'espace de recherche, on peut représenter les interprétations des variables propositionnelles par un tableau qui à chaque numéro de variable fait correspondre une valeur (de type val_t):

Exercices

<note tip> Par exemple, pour évaluer la valeur de vérité de la formule f = (a ∨ b) ⇒ c, on a besoin de connaître les valeurs des variables a, b et c. Considérons la correspondance m = { a ↦ 0; b ↦ 1; c ↦ 2; d ↦ 3} et l’interprétation où a & c sont VRAI, b FAUX et d INDETERMINEE. Cette interprétation est représentée par le vecteur [VRAI | FAUX | VRAI | INDETERMINEE]. On a dans cet exemple valeur_lit(v, ¬c) = FAUX, valeur_lit(v, ¬b) = VRAI et valeur_lit(v, ¬d) = INDETERMINEE

</note>

Exploration de l'espace de recherche

Écrire la fonction récursive 

bool cherche(vector<val_t> & valeurs, var_t suiv, const cnf_t & cnf);

qui renvoie true si cnf est satisfiable, sachant que:

La fonction procèdera comme suit:

  1. si suiv est supérieur à la taille de valeurs, alors évaluer la CNF et renvoyer VRAI si elle est satisfaite.
  2. sinon:
    1. mettre la valeur de suiv à VRAI dans valeurs
    2. Appeler récursivement la fonction avec suiv+1
      1. si l'appel récursif renvoie true la CNF est satisfiable et on peut renvoyer true
      2. sinon mettre la valeur de suiv à FAUX dans valeurs
    3. Appeler à nouveau récursivement la fonction avec suiv+1
      1. si l'appel récursif renvoie true la CNF est satisfiable et on peut renvoyer true
      2. sinon la CNF n'est pas satisfiable pour l'affectation courante: remettre la valeur de suiv à INDETERMINEE, puis renvoyer false.

<note warning>Dans la définition de la fonction cherche, on suppose que la longueur du tableau vector<val_t> & valeurs passé en paramètre est égale au nombre de variables (différentes) de la cnf. Ainsi:

</note>

Modifier la fonction main de façon à:

  1. lire la cnf en utilisant la fonction lit_dimacs définie dans dimacs.hpp
  2. initialiser un tableau de valeurs à INDETERMINEE pour chaque identifiant de variable;
  3. appeler la fonction cherche et afficher le résultat:
    • soit la ligne suivante si la CNF est insatisfiable:
      UNSAT
    • soit une ligne SAT suivie d'une ligne au format dimacs listant les littéraux vrai14), par exemple
      SAT
1 -2 -3 4 0

      On utilisera la fontion ecrit_clause_dimacs pour écrire la 2eme ligne.

<note>Par convention (utilisée dans resout-edt.sh), le premier argument du programme est le fichier contenant la cnf et le deuxième est le fichier dans lequel on doit écrire le résultat</note>

<note important> A la fin de cette partie, le projet dispose de toutes les fonctionnalités pour vérifier la satisfiabilité (et donc aussi la validité) d'une formule. L'efficacité algorithmique de la méthode dépend des stratégies de recherche implémentée dans cherche et de simplification que l'on peut apporter lors du calcul de valeurs de la CNF, pour éviter d'effectuer trop de calculs. C'est l'objet de la quatrième partie du projet. </note>

<note tip>Code partiel pour la fonction main:

main.cpp
#include "formule.hpp"
#include "parser.hpp"
#include "sat.hpp"
#include "dimacs.hpp"
#include <iostream>
#include <fstream>
#include <cstdlib>
 
using namespace std;
 
int main(int argc, char** argv) {
  if (argc < 3) {
    cerr << "Usage: ./sat cnf.dimacs modele.dimacs" << endl;
    return EXIT_FAILURE;
  }
  ifstream fichier_cnf(argv[1]);
  dimacs dimacs_data;
  lit_dimacs(fichier_cnf, dimacs_data);
  vector<val_t> valeurs; // tableau dont les indices sont des (numéros
                         // de) variables et le contenu est la valeur
                         // affectée à la variable.
  // A FAIRE: initialiser correctement valeurs;
  ofstream fichier_modele(argv[2]);
  // attention effet de bord: valeurs est modifié par cherche
  if (cherche(valeurs, 0, dimacs_data.cnf)) {
    set<lit_t> modele;
    // remplir modele en fonction des valeurs données à chaque variable
    fichier_modele << "SAT" << endl;
    ecrit_clause_dimacs(fichier_modele, modele);
  } else {
    fichier_modele << "UNSAT" << endl;
  }
  fichier_modele.close();
}

</note>

Quatrième partie: optimisations

Couper l'arbre de recherche

L'exploration de l'espace de recherche implémentée précédement ne teste la satisfaction de la CNF que lorsque la valeur de toutes les variables est connue. Un moyen d'améliorer l'efficacité du solveur consiste à tester systématiquement la valeur de la CNF à chaque affectation de variable de façon à éviter d'explorer un morceau de l'arbre de recherche dont on sait qu'il mènera toujours à des évaluation de la CNF valant FAUX.

Exercice

Modifier la fonction cherche pour tester la satisfaction à chaque affectation de variable de façon à détecter au plus tôt les combinaisons de valeurs partielles insatisfiables. Si la CNF vaut FAUX, alors on peut renvoyer directement false sans faire l'appel récursif. Attention, il faut bien penser à remettre valeurs[suiv] à INDETERMINEE avant de renvoyer false, sous peine de fausser la suite de l'exploration de l'arbre de recherche.

Remarque: cette remise à zéro fait partie du “retour arrière” lors de l'exploration de l'arbre de recherche.

Indexation des clauses

Pour améliorer l'efficacité des tests de satisfiabilité, l'étape suivante consiste à indexer les clauses par les littéraux qui les contiennent. Plus précisément, il s'agit de construire une structure qui associe à chaque littéral la liste des clauses dans lequel il apparaît. Il suffit de tester uniquement cette liste lors de l'affectation d'un littéral à faux pour vérifier si l'affectation rend la CNF insatisfaite.

La structure d'indexation proposée consiste en un tableau contenant des listes de clauses. Les indice du tableau correspondent aux numéros des littéraux.

Exercices

Propagation unitaire

L'objectif de cette optimisation est, étant données certaines valeurs choisies pour les variables n°1 à n, d'affecter les variables dont la valeur est INDETERMINEE et qui doivent nécessairement prendre une certaine valeur pour que la CNF aie une chance de s'évaluer à VRAI.

Pour cela, on s'appuie sur la remarque suivante. Soit une clause L1 ∨ … ∨ Lk. Si tous les littéraux de cette clause valent FAUX, sauf un certain Lj qui vaut INDETERMINEE, alors cette clause ne pourra s'évaluer à VRAI que si Lj prend la valeur VRAI. On dira que cette clause est devenue unitaire. Il est ainsi inutile de tester les valeurs pour la variable V de Lj: si Lj est un littéral positif, V doit prendre la valeur VRAI, si Lj est un littéral négatif, elle doit prendre la valeur FAUX.

On peut également remarquer que si Lj se voit affecter la valeur VRAI, alors ¬Lj a pour valeur FAUX. Cela peut avoir deux conséquences:

On peut définir une fonction propage qui va se charger d'effectuer la propagation unitaire. A la manière de contient_insatisfaite, elle va s'appuyer sur l'index des clauses pour trouver rapidement les clauses à traiter. En effet, à l'exception des clauses qui sont unitaire dès le début, une clause ne peut être rendue unitaire que si un de ses littéraux est affecté à FAUX. On peut donc, lors de l'affectation d'une valeur à une variable, savoir, grâce à l'index, quelles sont les clauses à tester pour savoir si elles sont unitaires.

Lors du retour arrière, il est important de défaire le travail effectué par la propagation unitaire. Comme celle-ci peut toucher des variables dont les numéros ne se suivent pas forcément, il faudra stocker la liste des variables à remettre à zéro au cas où le choix de valeur ayant déclenché la propagation unitaire ne permet pas de montrer que la CNF est satisfiable.

Exercices

  1. Créer une nouvelle fonction
    vector<var_t> propage(lit_t lit, vector<val_t> & valeurs, cnf_t & cnf, vector<vector<cls_t> > & index)

    Cette fonction renvoie la liste des variables affectées. Par convention, si cette liste est vide on supposera que la propagation a mené à une contradiction. La fonction aura le comportement suivant:

    • Initialiser le vector résultat à un vector vide
    • Initialiser un vector<lit_t> contenant au départ lit. Cette structure contiendra la liste courante des littéraux que l'on veut affecter à VRAI.
    • Tant qu'il reste des littéraux à traiter:
      • Retirer un littéral L des littéraux à traiter
        • Vérifier si le littéral a déjà une valeur. Si c'est le cas, ne rien faire.
      • Ajouter la variable V correspondant à L dans le vector résultat
      • Affecter la bonne valeur à V
      • Utiliser l'index pour accéder aux clauses à vérifier (pour propagation unitaire ou contradiction15) )
        • Pour chaque clause unitaire trouvée, ajouté le littéral qui n'a pas de valeur dans les littéraux à traiter
        • Si une clause s'évalue à FAUX alors la CNF aussi et la propagation unitaire s'arrête. On remet alors à INDETERMINEE la valeur des variables du vector résultat, puis on renvoie un vector vide.
    • Renvoyer le résultat
  2. Modifier la fonction cherche de façon à utiliser propage au lieu de contient_insatisfaite
    • En particulier, bien penser à remettre la valeur des variables affectée par propage à INDETERMINEE lors des retours arrière.

Références

Historique

1)
pas de rar ou autre format exotique
2)
i.e. les noms et numéros des étudiants du binômes doivent constituer le nom du fichier
3)
pas de fichier en police 14 ou 16 pts pour faire du remplissage, cela se voit au premier coup d'oeil
4) , 6)
la zone de dépôt sera automatiquement fermée à ce moment
5)
l'excuse “je n'avais pas accès au dépôt” ne sera pas acceptée
7)
qui peut être récupéré via hg pull https://forge.univ-lyon1.fr/hg/inf3034l-2014-base
8)
pour le push/pull/clone
9)
Ce test ne contient pas de CHECK, on fera une simple vérification visuelle.
10)
Vous pouvez pour cela utiliser la notation des initializer_list avec par exemple cl1 = { 7, 6, 1, 4, 1};.
11)
attention, c'est le seolveur SAT qui lui donnera une valeur lorsqu'on lui demandera de tester la CNF à générer
12)
ostream
13)
comme il s'agit un appel séparé à l'exécutable edt, les matrices de littéraux ne sont plus disponibles, il faut donc les recréer.
14)
i.e. pour chaque variable, son littéral positif si elle vaut vrai ou son littéral négatif si elle vaut faux
15)
i.e. la clause s'évalue à FAUX