Projet accompagnant le cours de model checking. ----------------------------------------------- Objectif: --------- Écrire une bibliothèque efficace de diagrammes de décision booléens (BDD), accompagnée de quelques exemples. Sauf quelques contraintes listée plus loin vous êtes libre d'implémenter la bibliothèque comme vous voulez. Les objectifs sont d'être (1) correct, (2) complet vis-à-vis des opérations classiques sur les BDD, et (3) rapide. En particulier, si vous pouvez décider de ne pas implémenter les BDD de façon classique (voir les références plus bas), tant que vous êtes capable d'offrir les même fonctionnalités avec un coût équivalent ou moindre. Vous vous justifierez pendant la soutenance. Références: ----------- Pour commencer, lisez le support de cours limpide d'Henrik Reif Andersen: http://www.configit.com/fileadmin/Configit/Documents/bdd-eap.pdf Lisez-le jusqu'au bout : il décrit les exemples que je vous demande en démoi, et vous suggère même un plan pour commencer votre bibliothèque. Dans ce sujet j'appelle BDD n'importe quel objet qui peut se manipuler comme un BDD. Le fait que ce soit véritablement stocké sous la forme d'un diagramme de décision, qu'il soit ordonné, réduit, ou par exemple que les liens vers "0"/"false" ne soient pas représentés, que vous utilisiez des ZDD, sont autant de détails d'implémentation sur lesquels vous pouvez faire des choix. Pour approfondir, ce brouillon de Knuth est dense à souhait : http://www-cs-faculty.stanford.edu/~knuth/fasc1b.ps.gz N'hésitez pas à chercher d'autres articles sur le sujet (ça ne manque pas !). Modalités: ---------- 1) Le projet est à faire par groupes de 3 au plus. Qu'une personne de chaque groupe m'envoie un mail à avec la consitution du groupe, avant le 17 mai. 2) Le projet est à rendre au plus tard le 1er juillet (mais c'est la fin de la semaine des exams, donc arrangez vous pour finir avant!). Envoyez moi une tarball (<2Mo) par mail a . 3) Nous ferons des soutenances dans les premières semaines de juillet. Contraintes: ------------ - Je compilerai votre projet sur un Linux 64bits avec 4 cœurs et 8Go de RAM tournant sous Debian "unstable". Vous pouvez utiliser n'importe quel langage et bibliothèque (sauf bien sûr une bibliothèque qui implémente les BDD!) tant que le paquet existe sous Debian. Je n'ai pas clairement pas envie de devoir compiler 15 bibliothèques inconnues pour réussir à jouer avec votre projet. - La tarball ne doit pas contenir de binaires, et doit contenir un README indiquant 1) les noms des auteurs du projet 2) comment compiler le projet en ligne de commande (je préférerais "./configure; make" mais si vous utilisez autre chose dites moi quoi taper) 3) comment lancer les démos - Les opérations suivantes sur les BDD doivent être absolument supportées : (vous pouvez adapter les noms tant qu'on les reconnaît) - la construction d'un BDD représentant x ou !x, pour une variable x donnée. - la combinaisons de BDDs avec des opérateurs booléens classiques (au moins: and, or, not, xor, equiv, implies) - la quantification existentielle - la possibilité de substituer des variables dans un BDD (typiquement remplacer x' par x) - l'affichage un BDD - le calcul du nombre de satisfactions possibles d'un BDD, et l'affichage d'au moins une Libre à vous d'implémenter d'autres opérations qui vous semblent utiles. Par exemple enchaîner une opération binaire puis une quantification existentielle est assez fréquent, et il est classique de proposer une fonction qui fait les deux opérations en un seul parcours en profondeur. Démonstrations à implémenter: ----------------------------- 1) Le problème des 8 reines (mentionné dans le document d'Andersen) avec des options permettant, en ligne de commande: - de préciser le nombre de reines - de demander d'afficher au choix - le nombre de solutions, - une solution, - toutes les solutions 2) Le problème du cavalier (knight tour), avec une option en ligne de commande pour préciser la taille de l'échiquier. (Cf. exercice 7.1) Bonus ----- - si l'implémentation tire parti du multi-cœur - si l'implémentation est la plus rapide à résoudre l'un des problèmes à implémenter comme démo (et sans tricher -- p.ex. afficher le résultat attendu sans le calculer le compte pas.) - si l'implémentation possède un ramasse miettes pour libérer les BDD inutilisés - si le problème des huits reines à une option pour que trois reines ne soient jamais alignées: Si Ri, Rk, Rj sont les vecteurs représentant les coordonées de trois reines, les trois reines sont alignés si Ri-Rk et Rk-Rj sont colinéaires. Wikipedia illustre cette variante sur la page en français : http://fr.wikipedia.org/wiki/Probl%C3%A8me_des_huit_dames Sur les 12 solutions du problème classiques, seules 2 respectent cette contrainte supplémentaire. - des techniques de réordonnancement automatique des BDD (i.e., choisir l'ordre des variables pour réduire les BDD). Soutenance ---------- - N'importe qui dans le groupe doit avoir relu le code écrit par ses associés, et savoir m'expliquer comment marche la bibliothèque. - Je n'impose pas que tout le monde ait implémenté une partie de la bibliothèque. Relire le code des copains pour écrire des tests qui le cassent est un travail tout aussi productif. Mais je ne donnerai pas la même note à tous le monde si j'ai l'impression que certains ont laissé les autres faire sans s'impliquer.