Différences

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

--- enseignement:logique:projet:2014 [2014/11/03 18:13]
ecoquery
+++ enseignement:logique:projet:2014 [2014/12/08 12:27] (Version actuelle)
ecoquery [Couper l'arbre de recherche]
@@ Ligne 224: / Ligne 224: @@
 salle pour 0: 0
 salle pour 1: 0
-salle pour 2: 0..1
+salle pour 2: 0,1
 indisponible: 1
 </code>
 </note>
@@ Ligne 306: / Ligne 306: @@
 === 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 334: / 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 352: / 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 387: / 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 397: / 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 410: / 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 460: / 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 470: / 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 534: / 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, rédaction des partie 3 et 4.
+  * **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