Emmanuel COQUERY

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>

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

Le rendu consistera en une archive .zip ou .tar.gz¹⁾, nommée nom1-num1-nom2-num2-intermediaire.zip²⁾ ou nom1-num1-nom2-num2-final.zip, contenant:

• Le contenu de le projet de départ modifié par vos soins
• Un fichier etudiants.txt contenant les nom(s), prénom(s) et numéro(s) du/des étudiants ayant réalisé le projet (maximum 2 étudiants).
• Un fichier au format .pdf d'au maximum 5 pages A4 en police 11 pts³⁾, contenant:
  • une introduction (max. 0,5 page);
  • une description des difficultés rencontrées, des solutions apportées et une argumentation autour des choix techniques effectués;
  • une conclusion dans laquelle on pourra indiquer d'un point de vue plus personnel les apports et les manques du projet (max. 1 page).

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

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

Cette archive est à déposer sur spiral au plus tard le mardi 23 décembre 2014 à 23h59⁶⁾.

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>

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

• un fichier /Lisez-moi.txt qui décrit le contenu de l'archive; Attention ce fichier est celui de l'an dernier, ne pas en tenir compte
• un fichier /Syntaxe-EdT.txt qui décrit la syntaxe des fichiers d'entrée pour les problèmes d'emploi du temps. Remarque: le code de lecture de ces fichiers est founi.
• un dossier /unittest-cpp qui est une bibliothèque pour simplifier l'écriture des tests. Vous n'avez pas à vous intéresser à son contenu;
• un dossier /src qui contient les sources fournies :
  • /src/Makefile permet de construire le projet avec make, mais aussi de lancer les tests, de nettoyer le projet etc.
  • /src/main-edt.cpp, main-sat.cpp et /src/main-test.cpp sont les points d'entrée des trois programmes exécutables du projet: edt qui lit des contraintes d'emploi du temps et génère une formule, ou qui lit un modèle de cette formule et génère un emploi du temps; sat qui lit une formule, évalue sa satisfiabilité et affiche un modèle si la formule est satisfiable; et run-test.
  • /src/formule.hpp et /src/formule.cpp donnent la structure de CNF. Quelques fonctions de base sont à implémenter dans formule.cpp.
  • /src/edt.hpp et /src/edt.cpp définissent la structure d'un problème et de solution à un problème d'emploi du temps. Il sera demandé d'écrire les fonctions permettant de générer une CNF à partir d'un problème d'emploi du temps et inversement de construire une solution (i.e. un emploi du temps) à partir d'un modèle de cette CNF.
  • /src/sat.hpp et /src/sat.cpp sont encore quasiment vides et destinés à recevoir vos fonctions.
  • /src/dimacs.hpp et /src/dimacs.cpp contiennent les fonctions pour écrire les CNF au format DIMACS. Ce format servira d'intermédiaire entre les programmes edt et sat. A noter que c'est le format natif pour le programme minisat, qui pourra être utilisé à la place du programme sat du projet dans la 2eme partie et à des fins de comparaison ou de test dans les parties 3&4.
  • une collection d'autres fichiers dont certains seront générés automatiquement. Il n'est pas utile de les lire. Leur principal objectif est de définir une fonction lit_formule qui crée l'arbre de syntaxe abstraite à partir d'une formule sous fourme de chaîne (typiquement, saisie au clavier ou lue dans un fichier).

<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 fourni⁷⁾ peut être poussé vers cette forge.

• Pour créer un projet: http://forge.univ-lyon1.fr/projects/new
• Pour être ajouté à un projet, un étudiant doit s'être connecté au moins une fois sur http://forge.univ-lyon1.fr. Le manager du projet pourra alors l'ajouter via Configuration → Membres.
• L'url mercurial⁸⁾ de votre projet est accessible depuis Configuration → Dépôt
• Voir l'aide sur la forge pour un scénario d'utilisation pour des TPs/projets
• Voir les cours de LIF7
• Quelques slides pour la gestion de projet (regarder la partie forge)

</note>

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

• Première partie : prise en main et modélisation. Les premières fonctions à écrire permettent de s'imprégner de l'application, de la représentation des formules qui sera utilisée.
• Deuxième partie : traduction. Les algorithmes de test SAT travaillant sur des clauses, il faut tout d'abord convertir le problème d'emploi du temps en formule en forme normale conjonctive (CNF). Il faudra également être capable de reconvertir un modèle de la CNF en emploi du temps.

<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>

• Troisième partie : test de satisfiabilité . L'objectif est ici tester la satisfiabilité d'une formule CNF et de produire, le cas échéant, un modèle de cette formule. Une version naïve du test de satisfiabilité est à réaliser dans cette partie.
• Quatrième partie : optimisations. Il s'agit d'améliorer les performances du solveur en ajoutant des stratégies et des index permettant de couper l'arbre de recherche.

<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>

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

• l'introduction au C++
• le code d'exemple.

</note>

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.

• Prendre connaissance et comprendre le contenu du fichier Lisez-moi.txt. Prendre particulièrement attention à ce qu'il est DEMANDE DE NE PAS FAIRE .
• Lancer la compilation et l'exécution des tests via make test. Comprendre l'affichage produit. Ne pas s'inquiéter des warnings (relativement inoffensifs) produits lors de la compilation du code qui vous est fourni.

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;

• La classe vector permet un accès en temps constant via ses indices avec c[i] comme les tableaux C et offre l'avantage d'être dynamique. On peut par exemple ajouter autant d'éléments que l'on veut avec c.push_back(). Le nombre d'élément d'un vector est donnée avec c.size().
• La classe set offre l'avantage de garantir l'unicité et un ordre total sur les éléments qu'il contient. En revanche, il est obligatoire d'utiliser les itérateurs pour parcourir son contenu, voir cet exemple.

• Avec un itérateur de type cls_t::const_iterator, implémenter la méthode ostream& operator<<(ostream& out, const cls_t& cl) qui permettra d'afficher des élément sur un ostream comme cout et cerr. Voir l'exemple de l'affichage des éléments d’un conteneur.
• Écrire un TEST⁹⁾ qui crée une clause cl1 contenant les littéraux 1, 4, 7 et 6¹⁰⁾ et une autre clause cl2 de votre choix puis les affiche.
• Écrire un TEST avec les vérifications suivantes :
  • CHECK(cl1 != cl2);
  • CHECK(cl2 != cl1);
  • CHECK(cl1 == cl1);
  • CHECK(cl2 == cl2);
• Vérifier que les quatre tests s'évaluent à true.

• Avec un itérateur ou avec size(), implémenter la méthode ostream& operator<<(ostream& out, const cnf_t& c). Cette méthode utilisera l'opérateur précédemment défini pour cls_t.
• Ajouter un TEST pour l'affichage d'une CNF c contenant les clauses cl1 et cl2.
• Écrire une fonction bool est_dans(const cls_t& cl, const cnf_t& c) permettant de tester l'appartenance d'une clause à une CNF.
• Écrire un TEST pour vérifier notamment que est_dans(cl1, c) et que est_dans(cl2, c).

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 :

• Les littéraux positifs sont représentés par les entiers naturels pairs. On injecte ainsi la variable p qui vaut 2 dans l'ensemble des littéraux positifs en multipliant par 2, le littéral p vaut ainsi 4 : c'est le 3ème entier pair associé à la 3ème variable.
• Les littéraux négatifs sont représentés par les entiers naturels impairs. Le littéral ~p vaut ainsi 5 : c'est le 3ème entier impair associé à la 3ème variable.

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.

• Écrire la fonction lit_t var2lit(var_t v, bool p = true) qui injecte une variable v dans l'ensemble des littéraux. Le booléen p indique si le littéral est positif ou négatif. La déclaration bool p = true permet d'affecter une valeur par défaut à ce paramètre ce qui permet de considérer alors var2lit comme une fonction à un seul argument.
• Écrire la fonction lit_t neg(lit_t l) qui prend un littéral et retourne sa négation. La fonction renvoie donc l+1 ou l-1 selon le cas.
• Écrire la fonction var_t lit2var(lit_t l) qui prend un littéral en argument et retourne sa variable.
• Écrire la fonction bool positif(lit_t l) qui renvoie true si le littéral passé en argument est un littéral positif.
• Tester ces fonctions avec UnitTest++.

<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>

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:

• Cr_En_i_j: vrai si l'enseignant Ens_j enseigne le cours Crs_i.
• Cr_Sal_i_j: vrai si le cours Crs_i a lieu dans la salle Sl_j.
• Cr_Cx_i_j: vrai si le cours Crs_i a lieu durant le créneau Cx_i.

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>

• Coder la fonction void init_lits(const probleme& pb, lit_edt& vars) permettant d'initialiser cette structure en fonction du problème (i.e. en fonction du nombre de salles, d'enseignants, etc)

<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

Le littéral 4 (qui correspond à la variable 2) prend la valeur vrai¹¹⁾ 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

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

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

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:

• 13=neg(12)=neg(Cr_Sl[0][0]),
• 21=neg(20)=neg(Cr_Sl[2][0]),
• 27=neg(26)=neg(Cr_Cx[0][1])
• et 35=neg(34)=neg(Cr_Cx[2][1])

</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>

<note tip> Pour écrire les clauses dans un flux de sortie¹²⁾, 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>

• Implémenter la fonction void cours_salle_creneau(ostream& out, const lit_edt& vars, int cours1, int cours2, int salle, int creneau) qui génère la clause qui exprime que deux cours ne peuvent avoir lieu en même temps au même endroit. L'utiliser pour coder la fonction void cours_salle_creneau(ostream& out, const probleme& pb, const lit_edt& vars) qui génère ces clauses pour toutes les combinaisons possibles de cours, salles et créneaux.
• Implémenter la fonction void cours_enseignant_creneau(ostream& out, const lit_edt& vars, int cours1, int cours2, int enseignant, int creneau) qui génère la clause qui exprime que deux cours ne peuvent avoir le même enseignant pendant le même créneau. L'utiliser pour coder la fonction void cours_enseignant_creneau(ostream& out, const probleme& pb, const lit_edt& vars) qui génère ces clauses pour toutes les combinaisons possibles de cours, enseignants et créneaux.
• Coder les fonctions suivantes:

  void cours_au_plus_une_fois(ostream& out, const probleme& pb, const lit_edt& vars, int cours);
  void cours_au_plus_une_salle(ostream& out, const probleme& pb, const lit_edt& vars, int cours);
  void cours_au_plus_un_enseignant(ostream& out, const probleme& pb, const lit_edt& vars, int cours);

  qui codent le fait qu'un cours a lieu au plus une fois, a lieu dans au plus une salle et est enseigné par au plus un enseignant.

• Coder les fonctions suivantes:

  void cours_au_moins_une_fois(ostream& out, const probleme& pb, const lit_edt& vars, int cours);
  void cours_au_moins_une_salle(ostream& out, const probleme& pb, const lit_edt& vars, int cours);
  void cours_au_moins_un_enseignant(ostream& out, const probleme& pb, const lit_edt& vars, int cours);

  qui codent le fait qu'un cours a lieu au moins une fois, a lieu dans au moins une salle et est enseigné par au moins un enseignant.

• Utiliser les fonctions (cours_au_moins_XXX et cours_au_plus_XXX) ci-dessus pour écrire les fonctions suivantes qui codent les contraintes 3, 4 et 5:

  void cours_exactement_une_fois(ostream& out, const probleme& pb, const lit_edt& vars);
  void cours_exactement_une_salle(ostream& out, const probleme& pb, const lit_edt& vars);
  void cours_exactement_un_enseignant(ostream& out, const probleme& pb, const lit_edt& vars);

  Remarque: contrairement aux fonctions précédentes qui portaient sur un seul cours, ces fonctions doivent imposer les contraintes 3, 4 et 5 sur tous les cours.

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

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

salles

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

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

• En remarquant que coder la contrainte Ens_i enseigne Cr_j1, Crs_j2, etc revient à interdire à Ens_i d'enseigner les autres cours, en déduire les clauses (unitaires, c'est à dire réduites à une seule variable) à écrire pour coder cette contraintes. Implémenter la fonction void peut_enseigner_seulement(ostream& out, const probleme& pb, const lit_edt& vars, int enseignant, set<int> cours), puis la fonction void contrainte_enseigne(ostream& out, const probleme& pb, const lit_edt& vars) qui appellera la précédente pour tous les enseignants.
• Procéder de manière similaire pour les contraintes du type «les salles pour Cr_i sont Sl_j1, Sl_j2, etc» en implémentant les fonctions
  • void peut_seulement_avoir_lieu_dans(ostream& out, const probleme& pb, const lit_edt& vars, int cours, set<int> salles)
  • void contraintes_salles_cours(ostream& out, const probleme& pb, const lit_edt& vars).
• Le codage des contraintes d'indisponibilité des enseignants est proche, mais la contrainte liste les créneaux interdits au lieu des créneaux permis. De plus, il n'y a pas de variable codant directement le fait qu'un enseignant est (in)disponible à un certain créneau. Si un enseignant Ens_i n'est pas disponible au créneau Crx_j, il faut dire pour chaque cours Cr_k que si l'enseignant Ens_i enseigne le cours Cr_k, alors ce cours n'a pas lieu au créneau Crx_j. Coder les fonctions:
  • void indisponibilites_enseignant(ostream& out, const probleme& pb, const lit_edt& vars, int enseignant, set<int> creneaux_indisponibles)
  • void contrainte_indisponibilites(ostream& out, const probleme& pb, const lit_edt& vars)

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:

• création des littéraux qui représentent l'emploi du temps;
• pose des contraintes implicites;
• pose des contraintes explicites.

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

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

Matrice Cr_Sal

Matrice Cr_Cx

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

• pour l'enseignant: 0 (Ens_0) et 2 (Ens_1). Comme 2 est dans le modèle et pas 0, c'est l'enseignant Ens_1 qui fait le cours Crs_0.
• pour la salle: 12 (Sl_0) et 14 (Sl_1). Comme 12 est dans le modèle et pas 14, la salle pour le cours Crs_0 est Sl_0.
• pour le créneau: 24 (Cx_0) et 26 (Cx_1). Comme 26 est dans le modèle et pas 24, le cours Crs_0 a lieu au créneau Cx_1.

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:

• (Re)création des matrices de littéraux à partir du problème¹³⁾.
• Initialiser une solution vide.
• Pour chaque cours:
  • Trouver la salle, l'enseignant et le créneau correspondant en interrogeant la valeur des littéraux dans le modèle.
  • Créer remplir une structure affectation et l'ajouter à la solution.

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

</note>

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):

• VRAI si la variable est affectée à vrai
• FAUX si la variable est affectée à faux
• INDETERMINEE si la variable n'est pas affectée

• Écrire la fonction val_t valeur_lit(vector<val_t>, lit_t) qui, étant donnés le tableau des valeurs des variables suivant leur numéro (valeurs) et un littéral (l), donne la valeur de ce littéral.
• Écrire la fonction val_t valeur_clause(vector<val_t>, cls_t) qui, étant donnés le tableau des valeurs des variables suivant leur numéro (valeurs) et une clause (clause), utilise la fonction précédente pour déterminer la valeur de la clause.
  Remarque: si la clause contient un littéral qui vaut VRAI, alors elle sa valeur est VRAI. Si tous les littéraux de la clause valent FAUX, alors la clause vaut FAUX. Sinon sa valeur est INDETERMINEE.
• Écrire la fonction val_t valeur_cnf(vector<val_t>, cnf_t) qui utilise la fonction précédente pour déterminer la valeur de la CNF.
  Remarque: si la CNF contient une clause qui vaut FAUX, alors elle vaut FAUX. Si toutes ses clauses valent VRAI, alors elle vaut VRAI. Sinon sa valeur est INDETERMINEE.

<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>

É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:

• valeur contient les valeurs des variables
• suiv est une variable non affectée. On considère que toutes les variables dont le numéro est inférieur au numéro de suiv ont une valeur dans valeurs.

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:

• il n'y a pas besoin de faire de push_back ou de resize, l'allocation et l'initialisation est à la charge de la fonction qui appelle cherche ;
• on peut déterminer que toute les variables ont été affectées en comparant suiv et valeurs.size().

</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 vrai¹⁴⁾, 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>

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.

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.

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.

• Écrire une fonction

  vector<vector<cls_t> > indexe_clauses(const cnf_t& cnf)

  qui renvoie une telle structure initialisée en fonction de la CNF passée en argument.

• Écrire une fonction

  bool contient_insatisfaite(var_t variable, const vector<val_t>& valeurs,const vector<vector<cls_t> >& index_clauses)

  • index_clauses est la structure d'indexation des clauses
  • variable est le numéro d'une variable. On appelle l le littéral correspondant à variable et prenant la valeur FAUX
  • valeurs est le tableau des valeurs affectées aux variables
  • la fonction renvoie true si une des clauses contenant l s'évalue à FAUX dans l'interprétation courante (i.e. valeurs).
• Remplacer les appels à valeur_cnf dans cherche par une utilisation de la fonction contient_insatisfaite.

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:

• La CNF peut s'évaluer à FAUX auquel cas on sait que les valeurs choisies pour les variables n°1 à n ne permettront pas de montrer que la CNF est satisfiable;
• Une ou plusieurs autres clauses peuvent devenir unitaires, ceci entrainant l'affectation d'autres variables et ainsi de suite jusqu'à ce que la CNF s'évalue à FAUX ou qu'aucune clause ne soit rendue unitaire.

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.

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 contradiction¹⁵⁾ )
       • 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.

• Jean Gallier: Logic for Computer Science: Foundations of Automatic Theorem Proving.

• 2014-11-27: Ajout de code pour la fonction main dans main.cpp (à la fin de la partie 3). Le dépôt a été également mis à jour sur la forge, pas le zip sur cette page.
• 2014-11-24: Ajout de CNF générées correspondant aux problèmes pb-simpleX. Il se peut que vos CNF soient différentes en cas de différence dans l'ordre de numérotation des matrices de littéraux.
• 2014-11-04: Ajout d'un exemple fil rouge dans la partie 2.
• 2014-10-23: Corrections variées dans la partie 2, ajout d'exemples dans les sources lif11-2014-enonce.zip et sur la forge https://forge.univ-lyon1.fr/hg/inf3034l-2014-base, rédaction des partie 3 et 4.
• 2014-10-13: Bugfix pour la compilation de l'exécutable edt + bugfix dans le parseur dimacs, nouvelle version de lif11-2014-enonce.zip
• 2014-10-12: Première version, sans les parties 3 & 4