Simple 3-SAT Solver

3SAT.c

#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);
}