Différences

Ci-dessous, les différences entre deux révisions de la page.

--- enseignement:logique:projet:2014 [2014/10/23 11:12]
ecoquery [Quatrième partie: optimisations]
+++ enseignement:logique:projet:2014 [2014/12/08 12:27] (Version actuelle)
ecoquery [Couper l'arbre de recherche]
@@ Ligne 208: / Ligne 208: @@
 };
 </code>
+<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 [[#contraintes_explicites|sous-partie sur les contraintes explicites]]).
+<code txt pb-simple5b.txt>
+enseignants: 2
+salles: 2
+creneaux: 2
+cours: 3
+enseigne: 0,1,2
+enseigne: 0,1
+salle pour 0: 0
+salle pour 1: 0
+salle pour 2: 0,1
+indisponible: 1
+</code>
+</note>
 === Exercices sur la représentation d'un emploi du temps ===
   * 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''
+^Crs\Ens ^0^1^
+^0|0|2|
+^1|4|6|
+^2|8|10|
+Le littéral 4 (qui correspond à la variable 2) prend la valeur vrai((attention, c'est le seolveur SAT qui lui donnera une valeur lorsqu'on lui demandera de tester la CNF à générer)) 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\Sal^0^1^
+^0|12|14|
+^1|16|18|
+^2|20|22|
+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\Cx^0^1^
+^0|24|26|
+^1|28|30|
+^2|32|34|
+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 ====
@@ Ligne 224: / Ligne 276: @@
 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.
@@ Ligne 231: / Ligne 297: @@
   - 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 sortie((''ostream'')), on pourra utiliser la fonction ''ecrit_clause_dimacs(ostream& output, const cls_t& clause)'' fournie dans ''dimacs.hpp''.</note>
+<note tip>
+Pour écrire les clauses dans un flux de sortie((''ostream'')), on pourra utiliser la fonction ''ecrit_clause_dimacs(ostream& output, const cls_t& clause)'' fournie dans ''dimacs.hpp''.
+</note>
+<note important>
+Le [[http://www.satcompetition.org/2009/format-benchmarks2009.html|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.
@@ Ligne 248: / Ligne 334: @@
 void cours_au_moins_un_enseignant(ostream& out, const probleme& pb, const lit_edt& vars, int cours);
 </code> 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 2, 3 et 4:<code c++>
+  * 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:<code c++>
 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);
@@ Ligne 262: / Ligne 348: @@
   - 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:
+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:
 <code c++>
 struct probleme {
@@ Ligne 280: / Ligne 366: @@
 };
 </code>
+<note tip>
+**Exemple:**
+Si on reprend le problème exemple:
+<code txt pb-simple5b.txt>
+enseignants: 2
+salles: 2
+creneaux: 2
+cours: 3
+enseigne: 0,1,2
+enseigne: 0,1
+salle pour 0: 0
+salle pour 1: 0
+salle pour 2: 0,1
+indisponible: 1
+</code>
+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 ===
@@ Ligne 315: / Ligne 442: @@
 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:
+<code>
+{1,2,5,6,8,11,12,15,16,19,21,22,25,26,28,31,32,35}
+</code>
+On rappelle les matrices correspondant au problème:
+Matrice ''Cr_En''
+^Crs\Ens ^0^1^
+^0|0|2|
+^1|4|6|
+^2|8|10|
+Matrice ''Cr_Sal''
+^Crs\Sal^0^1^
+^0|12|14|
+^1|16|18|
+^2|20|22|
+Matrice ''Cr_Cx''
+^Crs\Cx^0^1^
+^0|24|26|
+^1|28|30|
+^2|32|34|
+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:
-  * Recréation des littéraux à partir du problème.
+  * (Re)création des matrices de littéraux à partir du problème((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.)).
   * Initialiser une solution vide.
   * Pour chaque cours:
@@ Ligne 325: / Ligne 488: @@
 ===== Troisième partie: solveur SAT simple =====
+<note tip>Exemples de CNF pour les problemes: {{:enseignement:logique:projet:pb-simple-cnf.zip|}}.
+</note>
 ==== Calcul de la valeur courante d'une CNF ====
@@ Ligne 338: / Ligne 504: @@
 === Exercices ===
-  * É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 et un littéral donne la valeur de ce littéral.
+  * É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 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_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.
@@ Ligne 388: / Ligne 554: @@
 <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'':
+<code c++ 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();
+}
+</code>
 </note>
@@ Ligne 398: / Ligne 604: @@
 === 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 id_var à INDETERMINEE avant de renvoyer false, sous peine de fausser la suite de l'exploration de l'arbre de recherche.
+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.
@@ Ligne 462: / Ligne 668: @@
 ===== Historique =====
-  * **2014-10-23**: Corrections variées dans la partie 2, ajout d'exemples dans les sources {{:enseignement:logique:projet:lif11-2014-enonce.zip|}} et sur la forge https://forge.univ-lyon1.fr/hg/inf3034l-2014-base
+  * **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 {{:enseignement:logique:projet:pb-simple-cnf.zip|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 [[#deuxieme_partietraduction|partie 2]].
+  * **2014-10-23**: Corrections variées dans la [[#deuxieme_partietraduction|partie 2]], ajout d'exemples dans les sources {{:enseignement:logique:projet: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 {{:enseignement:logique:projet:lif11-2014-enonce.zip|}}
   * **2014-10-12**: Première version, sans les parties 3 & 4

Emmanuel COQUERY

Outils de la page

Différences