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);
}
/****************************************************************/
//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
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.
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.