Skip to content

Instantly share code, notes, and snippets.

@gonch
Last active December 31, 2015 09:39
Show Gist options
  • Save gonch/7968147 to your computer and use it in GitHub Desktop.
Save gonch/7968147 to your computer and use it in GitHub Desktop.
Simple 3-SAT Solver
#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