Différences

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

Lien vers cette vue comparative

Les deux révisions précédentes Révision précédente
Prochaine révision
Révision précédente
enseignement:logique:projet:2014 [2014/10/21 18:26]
ecoquery [Contraintes explicites]
enseignement:logique:projet:2014 [2014/12/08 12:27] (Version actuelle)
ecoquery [Couper l'arbre de recherche]
Ligne 208: Ligne 208:
 };  }; 
 </code> </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 
 +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
 +
 +</code>
 +</note>
  
 === Exercices sur la représentation d'un emploi du temps === === 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)   * 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 ==== ==== 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). 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 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)//   - 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 === === 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.   * 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); 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. </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, 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 3et 5:<code c++>
 void cours_exactement_une_fois(ostream& out, const probleme& pb, const lit_edt& vars); 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_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.   - 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++> <code c++>
 struct probleme { struct probleme {
Ligne 280: Ligne 366:
 }; };
 </code> </code>
 +
 +<note tip>
 +**Exemple:**
 +
 +Si on reprend le problème exemple:
 +
 +<code txt 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
 +
 +</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 === === Exercices sur les contraintes explicites ===
Ligne 286: Ligne 413:
     * ''void peut_seulement_avoir_lieu_dans(ostream& out, const probleme& pb, const lit_edt& vars, int cours, set<int> salles)''     * ''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)''.     * ''void contraintes_salles_cours(ostream& out, const probleme& pb, const lit_edt& vars)''.
-  * Le codage des contraintes d'indisponibilité des enseignants est très 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:+  * 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 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)''     * ''void contrainte_indisponibilites(ostream& out, const probleme& pb, const lit_edt& vars)''
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//. 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: 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 un solution vide.+  * Initialiser une solution vide.
   * Pour chaque cours:   * Pour chaque cours:
     * Trouver la salle, l'enseignant et le créneau correspondant en interrogeant la valeur des littéraux dans le modèle.     * 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.     * Créer  remplir une structure affectation et l'ajouter à la solution.
  
-===== Troisième partie: solveur SAT =====+===== Troisième partie: solveur SAT simple =====
  
-venir+<note tip>Exemples de CNF pour les problemes: {{:enseignement:logique:projet: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''): 
 + 
 +  * 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 
 + 
 + 
 + 
 +=== 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 (''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> 
 + 
 +==== Exploration de l'espace de recherche ==== 
 + 
 +Écrire la fonction récursive  
 +<code c++> 
 +bool cherche(vector<val_t> & valeurs, var_t suiv, const cnf_t & cnf);  
 +</code> 
 +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: 
 +  - si ''suiv'' est supérieur à la taille de ''valeurs'', alors évaluer la CNF et renvoyer VRAI si elle est satisfaite. 
 +  - sinon: 
 +    - mettre la valeur de ''suiv'' à VRAI dans ''valeurs'' 
 +    - Appeler récursivement la fonction avec ''suiv+1'' 
 +      - si l'appel récursif renvoie ''true'' la CNF est satisfiable et on peut renvoyer ''true'' 
 +      - sinon mettre la valeur de ''suiv'' à FAUX dans ''valeurs'' 
 +    - Appeler à nouveau récursivement la fonction avec ''suiv+1'' 
 +      - si l'appel récursif renvoie ''true'' la CNF est satisfiable et on peut renvoyer ''true'' 
 +      - 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 à: 
 + 
 +  - lire la cnf en utilisant la fonction ''lit_dimacs'' définie dans ''dimacs.hpp'' 
 +  - initialiser un tableau de valeurs à INDETERMINEE pour chaque identifiant de variable; 
 +  - appeler la fonction cherche et afficher le résultat: 
 +    * soit la ligne suivante si la CNF est insatisfiable:<code>UNSAT</code> 
 +    * soit une ligne SAT suivie d'une ligne au format dimacs listant les littéraux vrai((//i.e.// pour chaque variable, son littéral positif si elle vaut vrai ou son littéral négatif si elle vaut faux)), par exemple<code>SAT 
 +1 -2 -3 4 0 
 +</code> 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> 
 +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>
  
 ===== Quatrième partie: optimisations ===== ===== Quatrième partie: optimisations =====
  
-venir+==== 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 === 
 + 
 +  * Écrire une fonction <code c++>vector<vector<cls_t> > indexe_clauses(const cnf_t& cnf)</code> qui renvoie une telle structure initialisée en fonction de la CNF passée en argument. 
 +  * Écrire une fonction <code c++>bool contient_insatisfaite(var_t variable, const vector<val_t>& valeurs,const vector<vector<cls_t> >& index_clauses)</code> 
 +    * ''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''
 + 
 +==== 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 L//1// ∨ ... ∨ L//k//. Si tous les littéraux de cette clause valent FAUX, sauf un certain L//j// qui vaut INDETERMINEE, alors cette clause ne pourra s'évaluer à VRAI que si L//j// 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 L//j//: si L//j// est un littéral positif, V doit prendre la valeur VRAI, si L//j// est un littéral négatif, elle doit prendre la valeur FAUX. 
 + 
 + 
 +On peut également remarquer que si L//j// se voit affecter la valeur VRAI, alors ¬L//j// 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. 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 === 
 + 
 +  - Créer une nouvelle fonction<code c++>vector<var_t> propage(lit_t lit, vector<val_t> & valeurs, cnf_t & cnf, vector<vector<cls_t> > & index)</code> 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((i.e. la clause s'évalue à FAUX)) ) 
 +        * 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 
 +  - 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 ===== 
 + 
 +  * Jean Gallier: //[[http://www.cis.upenn.edu/~jean/gbooks/logic.html|Logic for Computer Science:  
 +Foundations of Automatic Theorem Proving]]//
 + 
  
 ===== Historique ===== ===== Historique =====
  
 +  * **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-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   * **2014-10-12**: Première version, sans les parties 3 & 4