Last active
December 31, 2015 09:39
-
-
Save gonch/7968147 to your computer and use it in GitHub Desktop.
Simple 3-SAT Solver
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#include <stdio.h> | |
#include <assert.h> | |
FILE *ent; | |
int i,j,c,numclauses,n; | |
int satisfactible; | |
int r; | |
int clauses[1065][3]; | |
void escribir_modelo(int modelo[]) | |
{ | |
for(i=1;i<=n;i++) | |
{ | |
if (modelo[i]==-1)modelo[i]=0; | |
printf("m[%d]= %d \n",i,modelo[i]); | |
} | |
printf("\n"); | |
} | |
void escribir_pesos(int pesos[i]) | |
{ | |
for(i=1;i<=n;i++) | |
{ | |
printf("p[%d]= %d ",i,pesos[i]); | |
} | |
printf("\n"); | |
} | |
int next(int modelo[]) | |
{ | |
int pesos[n+1]; | |
for(i=0;i<=n;i++) | |
{ | |
pesos[i]=0; | |
} | |
for(i=0;i<numclauses;i++) | |
{ | |
int c1=clauses[i][0]; | |
int c2=clauses[i][1]; | |
int c3=clauses[i][2]; | |
if((c1>0 && modelo[c1]==1) || (c1<0 && modelo[-c1]==0))continue; | |
if((c2>0 && modelo[c2]==1) || (c2<0 && modelo[-c2]==0))continue; | |
if((c3>0 && modelo[c3]==1) || (c3<0 && modelo[-c3]==0))continue; | |
int falsas=0; | |
if ((c1>0 && modelo[c1]==0) || (c1<0 && modelo[abs(c1)]==1)) falsas++; | |
if ((c2>0 && modelo[c2]==0) || (c2<0 && modelo[abs(c2)]==1)) falsas++; | |
if ((c3>0 && modelo[c3]==0) || (c3<0 && modelo[abs(c3)]==1)) falsas++; | |
if (falsas==3) return 0; | |
else if (falsas==2) | |
{ | |
if(modelo[abs(c1)]==-1) return abs(c1); | |
if(modelo[abs(c2)]==-1) return abs(c2); | |
if(modelo[abs(c3)]==-1) return abs(c3); | |
} | |
else if (falsas==1) | |
{ | |
if(modelo[abs(c1)]==-1) pesos[abs(c1)]+=5; | |
if(modelo[abs(c2)]==-1) pesos[abs(c2)]+=5; | |
if(modelo[abs(c3)]==-1) pesos[abs(c3)]+=5; | |
} | |
else if (falsas==0) | |
{ | |
if(modelo[abs(c1)]==-1) pesos[abs(c1)]++; | |
if(modelo[abs(c2)]==-1) pesos[abs(c2)]++; | |
if(modelo[abs(c3)]==-1) pesos[abs(c3)]++; | |
} | |
} | |
int max=0; | |
int pmax=0; | |
for(i=1;i<=n;i++) | |
{ | |
if(pesos[i]>max) | |
{ | |
max=pesos[i]; | |
pmax=i; | |
} | |
} | |
if(pmax==0) return -1; | |
return pmax; | |
} | |
void dpll(int modelo[]) | |
{ | |
if(satisfactible==0) | |
{ | |
int x=next(modelo); | |
if(x==0) return; | |
if(x==-1) | |
{ | |
satisfactible=1; | |
printf("SATISFACTIBLE:\n"); | |
escribir_modelo(modelo); | |
return; | |
} | |
else | |
{ | |
modelo[x]=1; | |
dpll(modelo); | |
modelo[x]=0; | |
dpll(modelo); | |
modelo[x]=-1; | |
} | |
} | |
} | |
int main( int argc, char *argv[] ) | |
{ | |
ent = fopen(argv[1], "r"); | |
c = getc(ent); | |
while( c == 'c' ) { while (c != '\n') c=getc(ent); c=getc(ent); } | |
fscanf(ent," cnf %d %d",&n, &numclauses); | |
printf("\nNumvars: %d Numclausulas: %d\n",n,numclauses); | |
int modelo[n+1]; | |
for(i=1;i<=n;i++) modelo[i]=-1; | |
for(i=0;i<numclauses;i++) | |
{ | |
for(j=0;j<3;j++) | |
{ | |
fscanf(ent,"%d\n",&clauses[i][j]); | |
} | |
fscanf(ent,"%d\n",&c); | |
} | |
printf("clausulas leidas: \n"); | |
for(i=0;i<numclauses;i++) | |
{ | |
for(j=0;j<3;j++) | |
{ | |
printf("%d ",clauses[i][j]); | |
} | |
printf("\n"); | |
} | |
satisfactible=0; | |
dpll(modelo); | |
if (satisfactible==0) printf("UNSAT\n"); | |
return(1); | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment