===== Introduction ===== 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 [[http://minisat.se/|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. 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). ==== Modalités de rendu ==== Le projet est à rendre en deux fois (parties 1&2, puis parties 3&4). Le rendu consistera en une archive .zip ou .tar.gz((pas de rar ou autre format exotique)), nommée ''//nom1//-//num1//-//nom2//-//num2//-intermediaire.zip''((//i.e.// les noms et numéros des étudiants du binômes doivent constituer le nom du fichier)) 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((pas de fichier en police 14 ou 16 pts pour faire du remplissage, cela se voit au premier coup d'oeil)), 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). === Rendu intermédiaire === L'archive du rendu intermédiaire est à déposer sur spiral au plus tard le dimanche **23 novembre 2014 à 23h59**((la zone de dépôt sera automatiquement fermée à ce moment)). Il **fortement** recommandé de tester l'accès à la zone de dépôt avant la date butoir((l'excuse "je n'avais pas accès au dépôt" ne sera pas acceptée)). Lien spiral pour le //**rendu intermédiaire**//: http://spiralconnect.univ-lyon1.fr/webapp/activities/activities.jsp?containerId=3668845 === Rendu final === Cette archive est à déposer sur spiral au plus tard le mardi **23 décembre 2014 à 23h59**((la zone de dépôt sera automatiquement fermée à ce moment)). La zone de dépôt pour le //**rendu final**//: http://spiralconnect.univ-lyon1.fr/webapp/activities/activities.jsp?containerId=3662577 Le non respect de ces consignes entraînera une sanction dans la note du projet. ==== Projet de départ ==== L'archive {{:enseignement:logique:projet: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 [[http://logic.pdmi.ras.ru/~basolver/dimacs.html|DIMACS]]. Ce format servira d'intermédiaire entre les programmes ''edt'' et ''sat''. A noter que c'est le format natif pour le programme [[http://minisat.se|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). Il est demandé de ne pas héberger vos sources sur un dépôt public. L'UCBL met à votre disposition une [[http://forge.univ-lyon1.fr|forge]] avec un hébergement de dépôts [[http://mercurial.selenic.com/|mercurial]]. Le projet fourni((qui peut être récupéré via ''hg pull https://forge.univ-lyon1.fr/hg/inf3034l-2014-base'')) 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((pour le push/pull/clone)) de votre projet est accessible depuis Configuration -> Dépôt * Voir [[:enseignement:aide:forge|l'aide sur la forge]] pour un scénario d'utilisation pour des TPs/projets * Voir les cours de [[http://liris.cnrs.fr/~ameyer/public_html/www/doku.php?id=lif7|LIF7]] * Quelques {{:enseignement:maven-forge-ic.pdf|slides}} pour la gestion de projet (regarder la partie forge) ==== Organisation du projet ==== 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. C'est le résultat de ces deux première parties qu'il faut rendre dans le cadre du rendu intermédiaire. * //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. 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. ===== Première partie : prise en main ===== Pour de l'aide sur les bases du C++ utiles à ce TP voir : * [[http://liris.cnrs.fr/romuald.thion/files/Enseignement/LIFC++/Intro_Cpp.html|l'introduction au C++]] * [[http://liris.cnrs.fr/romuald.thion/files/Enseignement/LIFC++/Code_LIF10_Example/Simple.cpp|le code d'exemple]]. ==== Tests unitaires avec UnitTest++ ==== Le projet est fourni avec la bibliothèque ''[[http://unittest-cpp.sourceforge.net/|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''. === Exercices === * 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. ==== Forme normale conjonctive ==== Les structures codant les clauses et les formules conjonctives (que l'on abrégera désormais CNF pour [[http://fr.wikipedia.org/wiki/Forme_normale_conjonctive|Conjunctive Normal Form]]) sont définies par des ''typedef'' utilisant différents [[http://www.cplusplus.com/reference/stl/|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 cls_t; typedef vector cnf_t; * La classe ''[[http://www.cplusplus.com/reference/stl/vector/|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 ''[[http://www.cplusplus.com/reference/stl/set/|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 [[http://www.cplusplus.com/reference/stl/set/begin/|cet exemple]]. === Exercices sur les clauses === * 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 [[http://liris.cnrs.fr/romuald.thion/files/Enseignement/LIFC++/Intro_Cpp.html|l'affichage des éléments d’un conteneur]]. * Écrire un ''TEST''((Ce test ne contient pas de ''CHECK'', on fera une simple vérification visuelle.)) qui crée une clause ''cl1'' contenant les littéraux //1//, //4//, //7// et //6//((Vous pouvez pour cela utiliser la notation des [[http://www.cplusplus.com/reference/std/initializer_list/|initializer_list]] avec par exemple ''cl1 = { 7, 6, 1, 4, 1};''.)) 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''. === Exercices sur CNF === * 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)''. ==== Représentation des variables et des littéraux ==== Pour des raisons d'efficacité, il faut éviter de représenter les variables propositionnelles par des chaînes (classe ''[[http://www.cplusplus.com/reference/string/|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. === Exercices sur les littéraux === * É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++''. 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é. ===== Deuxième partie : traduction ===== ==== Représentation d'un emplois du temps ==== 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 > 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 > Cr_Cx; }; **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]]). 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 === 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) **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" ==== Contraintes implicites ==== Pour que l'emploi du temps soit correct, il doit respecter implicitement les contraintes suivantes: - ''cours_salle_creneau'': Il est impossible que deux cours différents aient lieu au même moment dans la même salle. - ''enseignant_creneau'': Un enseignant fait au maximum un cours dans un créneau horaire donné. - ''cours_une_fois'': Un cours a lieu exactement une fois. - ''cours_une_salle'': un cours a lieu dans exactement une salle. - ''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). **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]) 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: - 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)// - 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)// **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}'' === Exercices sur les contraintes implicites === 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''. 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'' * 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. ==== Contraintes explicites ==== 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''): - 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. - Un cours ne peut avoir lieu que dans certaines salles. - 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 > enseigne; // pb.salles[i]={j1,j2,...} correspond // à la contrainte "salles pour i: j1, j2, ..." vector< set > salles; // pb.indisponibilites[i]={j1,j2,...} correspond à la // contrainte "i indisponible: j1, j2, ..." vector< set > indisponibilites; }; **Exemple:** Si on reprend le problème exemple: 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'' ^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. === Exercices sur les contraintes explicites === * 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 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 <> en implémentant les fonctions * ''void peut_seulement_avoir_lieu_dans(ostream& out, const probleme& pb, const lit_edt& vars, int cours, set 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 creneaux_indisponibles)'' * ''void contrainte_indisponibilites(ostream& out, const probleme& pb, const lit_edt& vars)'' ==== Traduction du problème ==== 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''. ==== Traduction d'un modèle en emploi du temps ==== 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''). Ecrire la fonction ''solution construit_solution(set& 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//. **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'' ^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 } La fonction ''construit_solution'' procédera comme suit: * (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: * 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. ===== Troisième partie: solveur SAT simple ===== Exemples de CNF pour les problemes: {{:enseignement:logique:projet:pb-simple-cnf.zip|}}. ==== 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, 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, 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, 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. 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 ==== Exploration de l'espace de recherche ==== Écrire la fonction récursive bool cherche(vector & 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: - 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''. Dans la définition de la fonction ''cherche'', on suppose que la longueur du tableau ''vector & 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()''. 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:UNSAT * 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 exempleSAT 1 -2 -3 4 0 On utilisera la fontion ''ecrit_clause_dimacs'' pour écrire la 2eme ligne. 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 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. Code partiel pour la fonction ''main'': #include "formule.hpp" #include "parser.hpp" #include "sat.hpp" #include "dimacs.hpp" #include #include #include 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 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 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(); } ===== Quatrième partie: optimisations ===== ==== 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 vector > 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& valeurs,const vector >& 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''. ==== 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. 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. === Exercices === - Créer une nouvelle fonctionvector propage(lit_t lit, vector & valeurs, cnf_t & cnf, vector > & 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'' 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 ===== * **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