Algorithme de davis putnam

5/5 (2 avis)

Vue 9 588 fois - Téléchargée 561 fois

Description

Permet de trouver un modèle d'une formule propositionnelle

Source / Exemple :


/*
   Algorithme de Davis-Putnam
      
   Programme fait par semaj_james
   mail: florentjustin@hotmail.com   
   09/12/2005 */

#include <stdio.h>
#include <stdlib.h>  /* Autorise l'utilisation de malloc
			et de free. */
#include<string.h>  //strlen(), strcpy()
#include<math.h>    //abs()

#define taille 80  //longeur du tableau pour la saisie

static struct
   {
   char tp[taille];
   int n;
   }pile;

typedef struct seg{
  int val;   //valeur
  int nl;    //numero de la ligne
}TABL ;  

typedef char *Tnom; //tableau pour stocker le nom des variables

/************************************************************/
// Matrice Rectangulaire Dynamique (mrd)
// allocation dynamique d'une matrice de taille (nbl, nbc)

#define composante int
typedef composante *mat_dyn;   //tableau d'entier

mat_dyn alloc_mrd(int nbl,int nbc)
 {return((mat_dyn)malloc((nbl)*nbc*sizeof(composante)));}

/* macro permettant d'acceder a l'element en ligne l et 
colonne c par m[l*nbc+c] */
#define adr_mrd(l,c,nbc) ((l)*(nbc)+(c))  

typedef struct noeud
      {   
      mat_dyn matrice;
      char arc;    //literral
      char signe;  //signe de l'arc
      int ligne;   //nombre de ligne de la matrice
      struct noeud *fils;
      struct noeud *frere;
      } *PNOEUD, NOEUD;

void gestion_regles(PNOEUD ancetre, int colonne, Tnom tvar, TABL *tabL);

/****************************************************************/
//initialisation de la matricre

void ini_matrice(mat_dyn *matrice,int ligne,int colonne)
{
int i,j;

  • matrice=alloc_mrd(ligne,colonne);
if(*matrice==NULL) { printf("pas assez de memoire disponible\n"); exit(1); } for(i=0;i<ligne;i++) for(j=0;j<colonne;j++) (*matrice)[adr_mrd(i,j,colonne)]=0; } /***************************************************************/ //affichage de la matrice void affiche_mrd(mat_dyn tab,int nblig, int nbcol) { int l,c; printf("\n"); for(l=0;l<nblig;l++) { printf("|"); for(c=0;c<nbcol;c++) printf("%2d ",tab[adr_mrd(l,c,nbcol)]); printf(" |\n"); } } /****************************************************************/ //insertion d'un sommet dans l'arbre PNOEUD ajout_arbre(mat_dyn t, int ligne, char lettre,char signe, PNOEUD fils, PNOEUD frere) { PNOEUD p; p = (PNOEUD)malloc(sizeof(NOEUD)); if(p==NULL) { printf("pas assez de memoire disponible\n"); exit(1); } p->matrice=t; p->ligne=ligne; p->arc=lettre; p->signe=signe; p->fils=fils; p->frere=frere; return p; } /***************************************************************/ void saisie(char formule[],int *var) { char saisie[6]; puts(" **********************************"); puts(" * *"); puts(" * ALGORITHME DE DAVIS - PUTNAM *"); puts(" * *"); puts(" **********************************\n"); puts("Notations: \n\n + pour OU\n . pour ET\n - pour NON\n"); puts("Saisissez une conjonction de clauses: (Maximum 20 variables propositionelles)"); fgets(formule,taille,stdin); printf("\nSaisissez le nombre de variables: "); fgets(saisie,sizeof(saisie),stdin); sscanf(saisie,"%d",var); } /****************************************************************/ //calcule le nombre de clauses (nombre de ligne de la matrice) int nbrligne(char formule[],int longueur) { int i,ligne=1; //il y a au minimum 1 ligne for(i=0;i<longueur;i++) { if (formule[i]=='.') ligne++; } return ligne; } /***************************************************************/ void ini_tabvar(Tnom *tvar, int var) { int i;
  • tvar=(Tnom)malloc((var+1)*sizeof(char));
if(*tvar==NULL) { printf("pas assez de memoire disponible\n"); exit(1); } for(i=0;i<var;i++) (*tvar)[i]='0'; (*tvar)[i]='\0'; } /***************************************************************/ //affiche le nom des variables void affiche_var(Tnom tvar) { int i; printf("\n| "); for(i=0;tvar[i]!='\0';i++) { printf("%c",tvar[i]); printf(" "); } printf("|\n"); } /***************************************************************/ /*remplissage de la matrice 0 pour vide 1 pour valeur positive -1 pour valeur negative */ void decoup(mat_dyn *matrice,int *ligne, int var,int longueur,char formule[], Tnom *tvar) { int i,j,lmat=0,valeur=1; for(i=0;i<longueur;i++) { switch(formule[i]) { case '+': break; case '(': break; case ')': break; case '.': lmat++; break; case '-': valeur=-1; break; default : for(j=0;(*tvar)[j]!='\0';j++) { if((*tvar)[j]==formule[i]) { switch((*matrice)[adr_mrd(lmat,j,var)]) { case 0: (*matrice)[adr_mrd(lmat,j,var)]=valeur; break; default: if( (*matrice)[adr_mrd(lmat,j,var)]==valeur) break; //application regle 1
  • ligne=*ligne-1; //on a une ligne de moins
for(j=0;j<var;j++) // on reinitialise la ligne (*matrice)[adr_mrd(lmat,j,var)]=0; while((formule[i]!='.') && (formule[i]!='\0')) i++; // on cherche la clause suivante break; } j=var-1; //on sort de la boucle for } else if((*tvar)[j]=='0') { (*matrice)[adr_mrd(lmat,j,var)]=valeur; (*tvar)[j]=formule[i]; j=var-1; //on sort de la boucle for } } valeur=1; break; } } } /****************************************************************/ int compare_qsort(const void *p1, const void *p2) //compare 2 adresses (qsort()) { const TABL *s1=p1, *s2=p2; if(s1->val < s2->val) return -1; if(s1->val == s2->val) return 0; else return 1; } /****************************************************************/ //comptage des elements sur une ligne void cpt_ligne(mat_dyn *t,TABL *tab2, int ligne, int colonne) { int i,j; for(i=0;i<ligne;i++) { tab2[i].val=0; //initialisation des valeurs tab2[i].nl=i; for(j=0;j<colonne;j++) tab2[i].val=tab2[i].val+abs((*t)[adr_mrd(i,j,colonne)]); } } /****************************************************************/ //reorganisation de la matrice apres triage void reorg(mat_dyn *t,TABL *tab2,int ligne,int colonne) { int k,j,l; mat_dyn tampon; ini_matrice(&tampon,ligne,colonne); for(k=0;k<ligne;k++) { l=tab2[k].nl; for(j=0;j<colonne;j++) tampon[adr_mrd(k,j,colonne)]=(*t)[adr_mrd(l,j,colonne)]; } free(*t);
  • t=tampon;
} /****************************************************************/ //comparaison de 2 lignes int compare(mat_dyn t,TABL *cpt_l,int ligne1, int ligne2, int colonne) { int i,cpt=0; for(i=0;i<colonne;i++) { if(t[adr_mrd(ligne1,i,colonne)] !=0) { if(t[adr_mrd(ligne1,i,colonne)] == t[adr_mrd(ligne2,i,colonne)]) { cpt++; if(cpt==cpt_l[ligne1].val) //la ligne 2 contient toutes les return 1; //clause de la ligne 1 } } } return 0; } /****************************************************************/ //suppression d'une clause int supp_ligne(mat_dyn *t,TABL *tabL, int *ligne, int nl, int colonne) { int i,j; if(*ligne==1) { for(i=0;i<colonne;i++) (*t)[adr_mrd(0,i,colonne)]=0; tabL[0].val=0; return 0; //matrice vide } else if((*ligne)-1==nl) //si derniere ligne
  • ligne=(*ligne)-1;
else { (*ligne)=(*ligne)-1; for(j=nl;j<(*ligne);j++) { for(i=0;i<colonne;i++) //on remonte chaque ligne => la matrice reste triee (*t)[adr_mrd(j,i,colonne)]=(*t)[adr_mrd(j+1,i,colonne)]; tabL[j].val=tabL[j+1].val; } } return 1; } /****************************************************************/ //application regle 2 void regle2(mat_dyn *t, TABL *cpt_l,int *ligne,int colonne) { int ligne1,ligne2; cpt_ligne(t,cpt_l,*ligne,colonne); qsort(cpt_l,*ligne,sizeof(struct seg),compare_qsort); //Trie le tableaux par ordre croissant reorg(t,cpt_l,*ligne,colonne); for(ligne1=0;ligne1<(*ligne)-1;ligne1++) for(ligne2=ligne1+1;ligne2<*ligne;ligne2++) { if(compare(*t,cpt_l,ligne1,ligne2,colonne)) { supp_ligne(t,cpt_l,ligne,ligne2,colonne); ligne2--; //on re-teste la nouvelle ligne } } } /****************************************************************/ /* s'applique aux regles 3, 4, 5 Enleve de la matrice: - toutes les clauses qui contiennent le litteral a - (-a) dans toutes les autres clauses */ int enl_a(mat_dyn *t, int valeur, int col_a, TABL *tabL,int *ligne,int colonne) { int i; for(i=0;i<(*ligne);i++) { if( (*t)[adr_mrd(i,col_a,colonne)] == valeur) { if(supp_ligne(t,tabL,ligne,i,colonne)==0) return 2; //matrice vide i--; //permet de retester la (nouvelle) ligne } else if( (*t)[adr_mrd(i,col_a,colonne)] == -valeur) { (*t)[adr_mrd(i,col_a,colonne)]=0; tabL[i].val=tabL[i].val -1 ; if(tabL[i].val == 0) // clause incoherente { (*ligne)= 1; return 3; } } } return valeur; } /****************************************************************/ // note la lettre et le signe // retourne un pointeur pointant sur l'avant derniere structure PNOEUD // afin de faire dans gestion_regles(...): ancetre->fils PNOEUD caractere(PNOEUD ancetre,mat_dyn t,int ligne,int valeur_retour,int valeur,char carac, int frere) { PNOEUD nveau,nveau_fin; char lettre,signe; mat_dyn Mdefin; int colonne=1; switch(valeur) { case 1: lettre=carac; signe='+'; break; case -1:lettre=carac; signe='-'; break; } nveau= ajout_arbre(t,ligne,lettre,signe, NULL, NULL); if(frere) ancetre->frere=nveau; else ancetre->fils=nveau; if(valeur_retour>1) { switch(valeur_retour) { case 2: lettre=' '; //matrice vide signe=' '; break; case 3:lettre='-'; //matrice incoherente signe='|'; break; } ini_matrice(&Mdefin,ligne,colonne); nveau_fin= ajout_arbre(Mdefin,ligne,lettre,signe, NULL, NULL); nveau->fils=nveau_fin; return nveau; } return ancetre; } /****************************************************************/ //application regle 3 int regle3(mat_dyn *t,Tnom tvar,TABL *tabL,int *ligne,int colonne, PNOEUD *ancetre) { int j=0,valeur,val_retour; if(tabL[0].val==1) //matrice triee donc si != 1 la ligne et les suivantes // contiennent forcement + de 2 elements { while((*t)[adr_mrd(0,j,colonne)] == 0) //on cherche la colonne du litteral j++; valeur= (*t)[adr_mrd(0,j,colonne)]; val_retour=enl_a(t,valeur,j,tabL,ligne,colonne); (*ancetre)=caractere(*ancetre,*t,*ligne,val_retour,valeur,tvar[j],0); return 3; //le litteral a ete trouve, on quitte } return 0; //il n'y a pas de litteral dans la matrice } /****************************************************************/ // application regle 4 int regle4(mat_dyn *t,Tnom tvar,TABL *tabL,int *ligne,int colonne, PNOEUD *ancetre) { int i,j=0,valeur=-3,val_retour; while(j<colonne && valeur==-3) { for(i=0;i<(*ligne);i++) { if((*t)[adr_mrd(i,j,colonne)] !=0 ) { if(valeur==-3) valeur=(*t)[adr_mrd(i,j,colonne)]; //on initialise valeur else if( valeur != (*t)[adr_mrd(i,j,colonne)]) { i=(*ligne); //si a et -a existe on passe a la colonne suivante valeur=-3; } } } if(valeur==-3) j++; } if(valeur>=-1) //application regle 4 { val_retour=enl_a(t,valeur,j,tabL,ligne,colonne); (*ancetre)=caractere(*ancetre,*t,*ligne,val_retour,valeur,tvar[j],0); return 4; } return 0; } /****************************************************************/ // application regle 5 void regle5(mat_dyn *t,Tnom tvar,TABL *tabL,int *ligne,int colonne, PNOEUD ancetre) { int i=0,j=0,trouve=0,ligne2,val_retour; PNOEUD nveau1; TABL *tabL2; mat_dyn t2; ligne2=(*ligne); ini_matrice(&t2,*ligne,colonne); memcpy(t2,*t,ligne2*colonne*sizeof(composante)); //on fait une copie de la matrice t tabL2=(TABL *)malloc(ligne2*sizeof(TABL)); memcpy(tabL2,tabL,ligne2*sizeof(TABL)); while(j<colonne && trouve==0) //on cherche la colonne pour { //appliquer cette rï¿?le while(i<(*ligne) && (*t)[adr_mrd(i,j,colonne)] ==0 ) i++; if(i==(*ligne)) { i=0; j++; } else trouve=(*t)[adr_mrd(i,j,colonne)]; //permet de sortir de la boucle } if(trouve) { // gestion de a val_retour=enl_a(t,1,j,tabL,ligne,colonne); nveau1=caractere(ancetre,*t,*ligne,val_retour,1,tvar[j],0); if(ancetre==nveau1) gestion_regles(ancetre->fils,colonne,tvar,tabL); // si ancetre != nveau1 => soit une matrice incoherente soit vide // cas deja traite donc on poursuit avec -a // gestion de -a val_retour=enl_a(&t2,-1,j,tabL2,&ligne2,colonne); nveau1=caractere(ancetre,t2,ligne2,val_retour,-1,tvar[j],1); if(ancetre==nveau1) gestion_regles(ancetre->frere,colonne,tvar,tabL2); // si ancetre != nveau1 => soit une matrice incoherente soit vide // cas deja traite donc on poursuit } free(tabL2); } /****************************************************************/ //gestion des regles void gestion_regles(PNOEUD ancetre, int colonne, Tnom tvar, TABL *tabL) { int ligne; mat_dyn Mmatrice,Mancetre; if( ancetre->arc!=' ' && ancetre->arc!='-') { Mancetre=ancetre->matrice; ligne=ancetre->ligne; ini_matrice(&Mmatrice,ligne,colonne); // copie du contenu de la matrice tampon dans la matrice t if(memcpy(Mmatrice,Mancetre,ligne*colonne*sizeof(composante))==NULL) printf("pointeur null"); cpt_ligne(&Mmatrice,tabL, ligne, colonne); if(regle3(&Mmatrice,tvar,tabL,&ligne,colonne,&ancetre)) gestion_regles(ancetre->fils,colonne,tvar,tabL); else if(regle4(&Mmatrice,tvar,tabL,&ligne,colonne,&ancetre)) gestion_regles(ancetre->fils,colonne,tvar,tabL); else regle5(&Mmatrice,tvar,tabL,&ligne,colonne,ancetre); } } /*****************************************************************/ void affiche_model(PNOEUD arbre) { PNOEUD p; pile.tp[pile.n++]=arbre->signe; pile.tp[pile.n++]=arbre->arc; if(arbre->arc=='#' && arbre->fils==NULL && arbre->frere ==NULL) printf("il n'y a pas de modele \n"); if(arbre->arc==' ' ) printf("%s -> modele valide\n",pile.tp+2); if(arbre->arc=='-') printf("%s -> modele incoherent\n",pile.tp+2); else { p=arbre->fils; if(p!=NULL) affiche_model(p); p=arbre->frere; if(p!=NULL) affiche_model(p); } pile.n=pile.n-2; } /****************************************************************/ // liberation de la memoire void lib_memoire(PNOEUD arbre) { if(arbre !=NULL) { if(arbre->fils != NULL) lib_memoire(arbre->fils); if(arbre->frere != NULL) lib_memoire(arbre->frere); free(arbre->matrice); free(arbre); } } /****************************************************************/ int main(void) { char formule[taille]; int var; //nombre de variables dans formule int ligne; //nombre de clauses dans formule int longueur; //nombre de caractere dans la formule mat_dyn Mdepart; Tnom tvar; TABL *tab_ligne; PNOEUD premier; saisie(formule,&var); longueur=strlen(formule); ligne=nbrligne(formule,longueur); //creation de la matrice [nombre clauses] [nombre variable] ini_matrice(&Mdepart,ligne,var); //creation du tableau de variable ini_tabvar(&tvar,var); decoup(&Mdepart,&ligne, var,longueur,formule, &tvar); printf("\nFormule: "); affiche_var(tvar); affiche_mrd(Mdepart,ligne,var); //regle 2 tab_ligne=(TABL *)malloc(ligne*sizeof(TABL)); regle2(&Mdepart,tab_ligne,&ligne,var); //regle 3,4,5 premier=ajout_arbre(Mdepart,ligne,'#','#', NULL, NULL); gestion_regles(premier,var,tvar,tab_ligne); printf("\nModele(s) trouve(s):\n\n"); affiche_model(premier); lib_memoire(premier); free(tab_ligne); //system("pause"); // permet d'empecher la fenetre DOS de se fermer immediatement return EXIT_SUCCESS; }

Conclusion :


Le zip contient:
- un pdf nommé regles qui decrit les règles de l'algorithme de Davis Putnam
- un autre pdf décrivant le code source
- un fichier .c contenant le programme
- un makefile pour les linuxiens

Dans le programme il y a dans le main la fonction system(pause) qui sert uniquement à empecher que la fenetre DOS ne se ferme automatiquement. A enlever pour les linuxiens sinon pour les utilisateurs de Windows cela fera une pause.

Codes Sources

A voir également

Ajouter un commentaire Commentaires
deck_bsd
Messages postés
1243
Date d'inscription
jeudi 31 mars 2005
Statut
Membre
Dernière intervention
3 août 2016
2
25 janv. 2006 à 14:30
Katsankat : "Pour rendre le code plus portable, system("pause") peut être remplacé par getchar() qui est défini dans stdio.h" c'est getch(); c'est mieu ;)
katsankat
Messages postés
571
Date d'inscription
vendredi 30 décembre 2005
Statut
Membre
Dernière intervention
12 juillet 2012
3
23 janv. 2006 à 14:10
Salut, c'est très bon.
Pour rendre le code plus portable, system("pause") peut être remplacé par getchar() qui est défini dans stdio.h; ou alors avec
#ifdef WIN32
system("PAUSE")
#endif

Vous n'êtes pas encore membre ?

inscrivez-vous, c'est gratuit et ça prend moins d'une minute !

Les membres obtiennent plus de réponses que les utilisateurs anonymes.

Le fait d'être membre vous permet d'avoir un suivi détaillé de vos demandes et codes sources.

Le fait d'être membre vous permet d'avoir des options supplémentaires.