Outils de la page

Piste:

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/11/24 13:04]
ecoquery [Troisième partie: solveur SAT simple] 		enseignement:logique:projet:2014 [2014/12/08 12:27] (Version actuelle)
ecoquery [Couper l'arbre de recherche]
Ligne 554: Ligne 554:
 <note important> <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. 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> </note>
  
Ligne 564: Ligne 604:
 === Exercice === === 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. Remarque: cette remise à zéro fait partie du "retour arrière" lors de l'exploration de l'arbre de recherche.
Ligne 628: Ligne 668:
 ===== 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-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-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.
CC Attribution-Noncommercial-Share Alike 3.0 Unported Sauf mention contraire, le contenu de ce wiki est placé sous les termes de la licence suivante : CC Attribution-Noncommercial-Share Alike 3.0 Unported
enseignement/logique/projet/2014.1416830676.txt.gz · Dernière modification: 2014/11/24 13:04 de ecoquery Haut de page