Skip to topic | Skip to bottom
Home
Minfo05
Minfo05.Lp1r1.15 - 14 Jan 2006 - 13:16 - EspenelCelinetopic end

Start of topic | Skip to actions

Satisfiabilité dans le calcul propositionnel

Enoncé

http://deptinfo.unice.fr/~ol/M1I/sat.pdf

C++

le 04/12

Pascal Benoit & Jean-Christophe Franchi :

Mise en place de la structure d'arbre en utilisant la façon abordée dans le sujet, trés facile à mettre en place. Les deux algos ont aussi été codés reste à vérifier l'efficacité de tout sur plusieurs tests et à faire un debuggage plus approfondi.

le 23/12

Nous nous sommes rendus compte que nous n'avons peut etre pas assez explicité notre travail, voici donc un descriptif un peu plus élaboré de la façon avec laquelle nous avons procédé pour développer notre partie :

Nous avons essayé de coller au maximum aux possibilités offertes par les langages objets:

Nous avons donc découper le travail a faire en plusieurs classes :

Deux fichiers pour la génération des tests (schur et additionneur) Deux fichiers pour la résolution avec les deux algos proposés ("davis & putnam" et "quine")

Ensuite nous avons fait une classe abstraite arbre qui sera la classe principale permettant d'effectuer toutes les opérations sur les arbres.

On a donc plusieurs arbres de défini (arbreOU arbreET ArbreIMPLIQUE?,...).

Les méthodes de la classe arbre sont celles que l'on a besoin pour les différents algos, exemple :

Le fichier ArbreEt? dont on se sert pour "quine" et pour "davis et putnam" contient les méthodes utilent aux deux traitements, a contrario la classe ArbreIMPLIQUE? ne contient que les méthodes nécessaires pour l'algo de "quine" étant donné que pour "davis et putnam" on n'a besoin que de conjonction de disjonction. Ces arbres possèdent par contre des méthodes afin de passer à une forme compatible avec le traitement de "davis et putnam" (exemple : un Arbre a=>b va rendre (a | b) en se servant de la methode fnc (mise sous forme clausale) qu'il contient.

le 30/12

Rien de partculier à signaler

ICON

Anthony Thuaux, Dimitre Kostov:

le 23/12

Diverses recherches ont été réalisées pour le moment, mais nous avouons rencontrer encore quelques problèmes non pas sur le sujet lui-même mais plus sur son implémentation étant donné notre connaissance limitée dans ce langage. Cela dit, nous essaierons dans les semaines à venir d'évoluer plus efficacement.

le 30/12

  • analyse les lignes grace aux fonction d'ICON
  • recuperation des littéraux dans la formule On met les littéraux dans une table
  • tri par ordre lexicographique
  • tri pas ordre alphabétique
  • modification de leur valeurs dans la ligne

Maintenant on peut associer des valeurs au variables. Dans la ligne grace à find on va checher le littéral égal au premier litteral de ligne et on le remplace dans toute la ligne par la valeur 0.(mais on perd le littéral...On ne pourra plus le modifier... On fait ça récurcivement sur tout les littéraux.

le ../01

Kostov Dimitre et Espenel Céline:

Avant de ne rendre le sujet, nous avons fini l'implémentation de l'algoritmhe de Quine et nous avons commencés l'algorithme de Putnam.

OCAML

le 06/12

David Bonfils & Céline Espenel : Etude des algos et discution sur la conception de programmation (filtres, types sommes, ...) imposé par l'énoncé.

le 15/12

David Bonfils & Céline Espenel : nous avons vu la structure d'une formule et d'un variable grace au type somme.

De plus nous avons penser qu'un parseur serait la bienvenue. Mais comment faire un parseur dans un langage purement fonctionnel? Nous avons étudier et nous étudierons encore ce point cette semaine.

le 23/12

Nous avons pensé à deux possibilités pour le parcours de l'arbre et la liste de ses variables. La première solution consiste à établir un parcours complet de l'arbre et de stocker toutes ses variables dans une liste avec la possibilité de ne pas stocker les variables déjà insérées dans cette liste. La seconde solution consiste à établir un parcours de l'arbre en ne rendant uniquement la prochaine occurrence de variable. Nous avons opté pour la seconde solution, car nous pensons qu'elle peut s'avèrer plus efficace dans la majorité des cas, hormis dans certains cas particulier.

En ce qui concerne l'état d'avancement du projet, nous avons implémentés la fonction principale, le moteur principal de l'application en d'autres termes. Il s'agit de la fonction qui evalue et simplifie une formule. De plus, nous avons implémenté l'algorithme de "Quine" qui nous renvoie un couple (bool, liste) :

  • premier élément correspond à la satisfaisabilité de la formule
  • second élément correspond à la liste des affectations des valeurs successives dons le cas où la formule est satisfaisable et une liste vide sinon.

Concernant la partie analyse lexicale et syntaxique, nous avons pensé un temps utiliser une bibliothèque d'OCaml mais après réflexion nous pensions préférable d'utiliser les outils (bien connus) que sont flex et yacc pour OCaml (OCamllex & OCamlyacc). Cependant, après en avoir établit une version, il s'avère que la tâche risque de prendre un peu de temps, notamment dû aux problèmes liés à la grammaire (26 shift/reduce et plus grave encore 11 reduce/reduce) Ainsi, pour le moment nous avons laissé ces travaux d'analyse en suspend. D'autre part, toujours concernant l'analyse d'une formule, nous avons pensé utilisé une notation préfixée afin de nous faciliter l'analyse et surtout dans le but de pouvoir réaliser nos tests.

Pour la suite des évènements, reste à implémenter l'algorithme de "Davis & Putnam"et de réaliser nos tests.

Pour la partie question : Existe-t-il une fonction "time" qui mesure le temps d'exécution d'un programme afin de réaliser nos benchmark ?

le 30/12

A venir ...

Rapports des entrevues pour la confection du rapport wink

le 10 janvier 2006 : Céline propose une première ébauche de plan et propose de voire le groupe le 11 janvier à 18h de vennir chez elle pour réviser le paradigme et passer un peu de temps à consolider ce plan fait à toute vitesse.

le 11 janvier 2006 :Kostov Dimitre et Espenel Céline

Nous avons principalement parler d'ICON. Icon est un extrèmement pratique pour la manipulation des chaînes de caractère. Ainsi faire le parseur en ce langage n'a pas nécéssité de bibliothèque suplémentaire comme dans OCAML où l'on s'est servi de Lex et de Yacc de OCAML. De plus les procédures sont assez génériques. On peut renvoyer un arbre comme un élément seul ou encore une constante. La notion d'échec permet une souplesse au point de vue de la programmation. Ainsi lorque l'on ne peut renvoyer de résultat correcte on renvoie un échec. La procédure qui reçoit cet échec n'a plus qu'à l'ignorer.

L'écriture de ce langage permet d'éviter les imbrications de if then else qui deviennent souvent illisibles. Par exemple, ici f := open(args[1]) | stop("lecture impossible du fichier:"||args[1])

Si l'on peut ouvrir args[1] alors on ne fera pas la commande stop si on ne peut l'ouvrir alors on lance stop. On voit bien dans cette ligne la facilité de traiter les erreures grace à la ntion de l'échec et grace à "|" qui permet de lancer la commande suivante si la première est mise en échec.

Mais si on peut reprocher une choe à Icon c'est la gestion des erreurs... En effet, comme la liaison entre les variables et leur valeur ne se fait qu'à l'exécution. Donc si l'on se trompe de nom dans l'apelle d'une procédure ou de variable alors la compilation se passe sans aucune erreur affichée... Seule l'éxécution révèlera la faute.

* formules.txt: quelques formules pour tester

Pour se servir de l'algo de Davis et Putnam lancer la commande ~>cel2 -d [formule] sinon ~>cel2 [formule]

le 14 janvier 2006 Espenel Céline

j'ai avancé le plan et comme prévu initialement j'ai fait le squellette du rapport en Latex.Ne pas oublier que chaque partie doit être dans un fichier à part que l'on importe dans le document maitre. Amusez vous bien! * ParadigmeRapport.rar: Rapport du projet

Plan détaillé du rapport

Pour cette partie, PERSONNE ne doit déborder sur les parties des autres! On peut aidé à la conception d'autres parties mais je ne veux pas qu'une seule personne ne fasse presque tout le rapport! Dans ce cas autant s'abstenir d'y participer ou encore d'aller à la fac!

Céline vous propose:

Notre travail devra contenir:

description du sujet, cahier des charges, spécifications, etc.

une petite introduction présentant le sujet.... Rien de bien méchant

description des choix d’implémentation et des problèmes rencontrés dans chaque langage

on a le choix entre le faire par langages ou par problèmes. Le meilleur choix étant par problèmes.

description plus détaillée des aspects spécifiques rencontrés dans chacun des trois langages

C++ à faire par Jean-Christophe et Pascal
Icon à faire par Dimitre Anthony et Céline
OCAML fait par David

bilan comparatif, à la fois pour les trois langages étudiés, et de manière plus générale, en tenant compte des langages connus

ce sera la plus grande partie de ce rapport. En tout cas à mon avis... Il faudra que l'on fasse tant bien que mal cette partie ensembles.

en annexe, les trois programmes, suffisamment commentés.

Documentation

Documentation sur la partie programmation de ce projet

http://caml.inria.fr/pub/docs/manual-ocaml/manual003.html Manuel officiel de OCAML! Même s'il est en anglais, il est clair et presque facile à lire. On y trouve rapidement ce qu'on y cherche.

http://www.pps.jussieu.fr/Livres/ora/DA-OCAML/ Cours sur OCAML en français. Il est pour les débutant. J'aime bien sa partie sur les arbres.

http://cristal.inria.fr/~remy/poly/ocaml/ocaml.pdf Cours sur OCAML en français

http://www.irisa.fr/lande/pichardie/TPLog/TP1/ un tp long un peu comme notre projet...

Documentation pour les différnts paradigmes observés et observables dans ce projet

-- EspenelCeline - 03 Dec 2005

Set ALLOWTOPICCHANGE = BenoitP, BonfilsDavid, EspenelCeline, FranchiJ, KostovDimitre, ThuauxAnthony


to top

I Attachment sort Action Size Date Who Comment
ParadigmeCaml.txt manage 2.0 K 17 Dec 2005 - 09:53 EspenelCeline petit travail sur les types somme
formules.txt manage 0.1 K 12 Jan 2006 - 10:40 EspenelCeline quelques formules pour tester
cel2.icn manage 15.2 K 12 Jan 2006 - 10:40 EspenelCeline version définitive d'Icon
ParadigmeRapport.rar manage 221.9 K 14 Jan 2006 - 13:15 EspenelCeline Rapport du projet

You are here: Minfo05 > ProjetParadigmes > Lp1

to top

Copyright © 1999-2017 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding WIKIDeptinfo? Send feedback