Ceci est une ancienne révision du document !
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 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.
<note>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).</note>
Le projet est à rendre en deux fois (parties 1&2, puis parties 3&4).
Le rendu consistera en une archive .zip ou .tar.gz1), nommée nom1-num1-nom2-num2-intermediaire.zip
2) ou nom1-num1-nom2-num2-final.zip
, contenant:
etudiants.txt
contenant les nom(s), prénom(s) et numéro(s) du/des étudiants ayant réalisé le projet (maximum 2 étudiants).L'archive du rendu intermédiaire est à déposer sur spiral au plus tard le dimanche 23 novembre 2014 à 23h594). Il fortement recommandé de tester l'accès à la zone de dépôt avant la date butoir5).
Lien spiral pour le rendu intermédiaire: http://spiralconnect.univ-lyon1.fr/webapp/activities/activities.jsp?containerId=3668845
Cette archive est à déposer sur spiral au plus tard le mardi 23 décembre 2014 à 23h596).
La zone de dépôt pour le rendu final: http://spiralconnect.univ-lyon1.fr/webapp/activities/activities.jsp?containerId=3662577
<note important>Le non respect de ces consignes entraînera une sanction dans la note du projet.</note>
L'archive lif11-2014-enonce.zip contient un projet C++. Ce projet de départ fourni contient une arborescence de projet avec :
/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 /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. /unittest-cpp
qui est une bibliothèque pour simplifier l'écriture des tests. Vous n'avez pas à vous intéresser à son contenu;/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 DIMACS. Ce format servira d'intermédiaire entre les programmes edt
et sat
. A noter que c'est le format natif pour le programme 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.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).<note tip>Il est demandé de ne pas héberger vos sources sur un dépôt public. L'UCBL met à votre disposition une forge avec un hébergement de dépôts mercurial. Le projet fourni7) peut être poussé vers cette forge.
</note>
Le projet est divisé en quatre grandes étapes qui correspondent grossièrement aux 4 séances de TP prévues :
<note tip>C'est le résultat de ces deux première parties qu'il faut rendre dans le cadre du rendu intermédiaire.</note>
<note important> 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. </note>
<note warning> Pour de l'aide sur les bases du C++ utiles à ce TP voir :
</note>
Le projet est fourni avec la bibliothèque 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
.
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.
Les structures codant les clauses et les formules conjonctives (que l'on abrégera désormais CNF pour Conjunctive Normal Form) sont définies par des typedef
utilisant différents 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<lit_t> cls_t; typedef vector<cls_t> cnf_t;
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()
.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 cet exemple.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 l'affichage des éléments d’un conteneur.TEST
avec les vérifications suivantes :CHECK(cl1 != cl2);
CHECK(cl2 != cl1);
CHECK(cl1 == cl1);
CHECK(cl2 == cl2);
true
.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
.TEST
pour l'affichage d'une CNF c
contenant les clauses cl1
et cl2
.bool est_dans(const cls_t& cl, const cnf_t& c)
permettant de tester l'appartenance d'une clause à une CNF.TEST
pour vérifier notamment que est_dans(cl1, c)
et que est_dans(cl2, c)
.
Pour des raisons d'efficacité, il faut éviter de représenter les variables propositionnelles par des chaînes (classe 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 :
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.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.
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.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.var_t lit2var(lit_t l)
qui prend un littéral en argument et retourne sa variable.bool positif(lit_t l)
qui renvoie true
si le littéral passé en argument est un littéral positif.UnitTest++
.<note important> 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é. </note>
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:
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<lit_t> > 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<lit_t> > Cr_Cx; };
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)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).
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:
<note tip>Pour écrire les clauses dans un flux de sortie11), on pourra utiliser la fonction ecrit_clause_dimacs(ostream& output, const cls_t& clause)
fournie dans dimacs.hpp
.</note>
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.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.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.
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.
cours_au_moins_XXX
et cours_au_plus_XXX
) ci-dessus pour écrire les fonctions suivantes qui codent les contraintes 2, 3 et 4: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.
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
):
Une fois le fichier lu par la fonctionlit_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<int> > enseigne; // pb.salles[i]={j1,j2,...} correspond // à la contrainte "salles pour i: j1, j2, ..." vector< set<int> > salles; // pb.indisponibilites[i]={j1,j2,...} correspond à la // contrainte "i indisponible: j1, j2, ..." vector< set<int> > indisponibilites; };
void peut_enseigner_seulement(ostream& out, const probleme& pb, const lit_edt& vars, int enseignant, set<int> 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.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 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)
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:
Cette fonction est appelée par la fonction main du fichier main-edt.cpp
.
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<affectation>
). Ecrire la fonction solution construit_solution(set<lit_t>& 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.
La fonction construit_solution
procédera comme suit:
A venir
A venir
edt
+ bugfix dans le parseur dimacs, nouvelle version de lif11-2014-enonce.ziphg pull https://forge.univ-lyon1.fr/hg/inf3034l-2014-base
CHECK
, on fera une simple vérification visuelle.cl1 = { 7, 6, 1, 4, 1};
.ostream