/*******************************************************************/
/*  A-SAT - Satisfiability of a CNF formula (backtracking method)  */
/*                                                                 */
/*  This program was developped by Pascal Andre on June 1992,      */
/*  in collaboration with Olivier Dubois, Jacques Carlier and      */
/*  Yacine Boufkhad.                                               */
/*                                                                 */
/*  Updated on October 1993 : the program has as argument an input */
/*  filename containing a CNF formula on DIMACS format.            */
/*******************************************************************/

#include <stdio.h>
#include <math.h>

#define then

int N; /* valeur du nombre de variables */
int P; /* valeur du nombre de clauses */
int R; /* valeur maximum de la longueur d'une clause */
int G; /* valeur du germe aleatoire */

int  **SATx; /* matrice PxLR des variables par clause */
char **SATv; /* matrice PxLR des formes des variables par clause */
int  **SAKc; /* matrice NxLK des clauses par variable */
char **SAKv; /* matrice NxLK des formes des clauses par variable */

int *LR;  /* vecteur P des longueurs des clauses (-1,0,..,R) */
int *LK;  /* vecteur N des frequences des variables (0,..,K) */
char *V;  /* vecteur N des instanciations des variables (0,1,2) */

int  PU; /* valeur du nombre de clauses unitaires */
int *CU; /* vecteur P des clauses unitaires */

char SAT; /* valeur de l'existence d'une solution */
int  BCH; /* valeur du nombre de branches parcourues */
int  PP;  /* valeur courante du nombre de clauses */
int  PRF; /* valeur de la profondeur de l'arbre de resolution */

char okSAT; /* valeur courante de la satisfiabilite du systeme */

struct arbre { int x,PP,PRF,*LR; char v,*V; };
struct arbre *LSAT; /* pointeur de l'arbre de resolution */
struct arbre *L;    /* pointeur du noeud de l'arbre de resolution */

double *KR; /* vecteur R des coef de la fct de bch */

FILE *f;

/**************************************************************/
 main(argc,argv) int argc; char *argv[];
/**************************************************************/
{

if (argc<2)
 fprintf(stderr,"Error : filename must be provided as argument !\n");
else {

 okSAT=2;

 lire_SAT(argv[1]);

 if (okSAT<=2) {

  L=LSAT; SAT=0; BCH=0; PP=P; PRF=0;

  if (okSAT) do {
   if (okSAT!=2) selectionner_SAT();
   if (okSAT==2) reduire_SAT();
   if (okSAT==2) brancher_SAT();
   if (okSAT==1) SAT=1;
  } while ((L!=LSAT) && !SAT);

  if (SAT)
   then printf("%s  %d variables  %d clauses    SATISFIABLE  %d branches  A-SAT\n",argv[1],N,P,BCH);
   else printf("%s  %d variables  %d clauses  UNSATISFIABLE  %d branches  A-SAT\n",argv[1],N,P,BCH);

 }

}

}

/**************************************************************/
 lire_SAT(fic) char *fic;
/**************************************************************/
{int i,j,x,r,*CL; char v,c;

 f=fopen(fic,"r");

if (f==NULL) {
 fprintf(stderr,"Error : \"%s\" does not exist !\n",fic);
 okSAT=3;
} else {

 fscanf(f,"%c",&c);
 while (c=='c') { while (c!='\n') fscanf(f,"%c",&c); fscanf(f,"%c",&c); }

if (c=='p') {

 while (c!='f') fscanf(f,"%c",&c);
 fscanf(f,"%d %d",&N,&P); G=0;

 SATx=(int **)malloc(P*sizeof(long));
 SATv=(char **)malloc(P*sizeof(long));
 LSAT=(struct arbre *)malloc(N*sizeof(struct arbre));
 for (i=0;i<N;i++) {
  LSAT[i].V=(char *)malloc(N*sizeof(char));
  LSAT[i].LR=(int *)malloc(P*sizeof(int));
 }

 LR=LSAT->LR; R=0;
 CL=(int *)malloc((N+1)*sizeof(int));
 CU=(int *)malloc(P*sizeof(int)); PU=0;
 for (i=0;i<P;i++) {
  r=0; fscanf(f,"%d",&CL[r]);
  while (CL[r]) { r++; fscanf(f,"%d",&CL[r]); }
  if (r>R) R=r;
  SATx[i]=(int *)malloc(r*sizeof(int));
  SATv[i]=(char *)malloc(r*sizeof(char));
  for (j=0;j<r;j++) {
   x=CL[j]; SATx[i][j]=abs(x)-1;
   if (x>0) SATv[i][j]=1; else SATv[i][j]=0;
  }
  if (r==1) { CU[PU]=i; PU++; }
  if (r==0) okSAT=0;
  LR[i]=r;
 }

 fclose(f);

 LK=(int *)malloc(N*sizeof(int));
 for (i=0;i<N;i++) LK[i]=0;
 for (i=0;i<P;i++)
  for (j=0;j<LR[i];j++) LK[SATx[i][j]]++; 
 SAKc=(int **)malloc(N*sizeof(long));
 SAKv=(char **)malloc(N*sizeof(long));
 for (i=0;i<N;i++) {
  SAKc[i]=(int *)malloc(LK[i]*sizeof(int));
  SAKv[i]=(char *)malloc(LK[i]*sizeof(char));
  LK[i]=0;
 }
 for (i=0;i<P;i++)
  for (j=0;j<LR[i];j++) {
   x=SATx[i][j]; v=SATv[i][j];
   SAKc[x][LK[x]]=i; SAKv[x][LK[x]]=v;
   LK[x]++;
  }

 V=LSAT->V;
 for (i=0;i<N;i++) V[i]=2;

 KR=(double *)malloc((R+1)*sizeof(double));
 KR[0]=0.0; KR[1]=(exp2((double)R)-1)*(exp2((double)R)-1);
 for (i=2;i<=R;i++)
  KR[i]=KR[1]/(exp2((double)i)-1)/(exp2((double)i)-1);

} else {
 fprintf(stderr,"Error : \"%s\" does not contain a CNF formula on DIMACS format !\n",fic);
 okSAT=3;
}

}

}

/**************************************************************/
 propager(x,v) int x; char v;
/**************************************************************/
{int j,c;

 PU=0;

 for (j=0;j<LK[x];j++) {
  c=SAKc[x][j];
  if (LR[c]>0) {
   if (SAKv[x][j]^v) LR[c]-=1; else { LR[c]=-1; PP--; }
   if (LR[c]==1) { CU[PU]=c; PU++; }
  }
 }

 V[x]=v; PRF++; BCH++;
}

/**************************************************************/
 brancher_SAT()
/**************************************************************/
{int i,j,x,r; double e,e1,e0;

 e=-1.0;
 for (i=0;i<N;i++) if (V[i]==2) {
  e1=0.0;
  for (j=0;j<LK[i];j++) { r=LR[SAKc[i][j]]; if (r>0) e1+=KR[r]; }
  if (e1>e) { x=i; e=e1; } 
 }

/*printf("e=%0.3f x=%d PRF=%d BCH=%d\n",e,x,PRF,BCH);*/

 e1=0.0; e0=0.0;
 for (j=0;j<LK[x];j++) {
  r=LR[SAKc[x][j]];
  if (r>0) if (SAKv[x][j]) e1+=KR[r]; else e0+=KR[r];
 }

 if (e1>e0) {
  accrocher(x,0);
  propager(x,1);
 } else {
  accrocher(x,1);
  propager(x,0);
 }

}

/**************************************************************/
 reduire_SAT()
/**************************************************************/
{int i,j,x,iu,c;
 char v;

 for (i=0;i<PU;i++) if (LR[CU[i]]==1) {
  iu=CU[i];
  for (j=0;V[SATx[iu][j]]!=2;j++);
  x=SATx[iu][j]; v=SATv[iu][j];
  for (j=0;j<LK[x];j++) {
   c=SAKc[x][j];
   if (LR[c]>0) {
    if (SAKv[x][j]^v) LR[c]-=1; else { LR[c]=-1; PP--; }
    if (LR[c]==0) { okSAT=0; goto fin; }
    if (LR[c]==1) { CU[PU]=c; PU++; }
   }
  }
  V[x]=v;
 }

 if (PP==0) okSAT=1;

 fin:;
}

/**************************************************************/
 selectionner_SAT()
/**************************************************************/
{int i;

 okSAT=2;

 for (i=0;i<N;i++) V[i]=L->V[i];
 for (i=0;i<P;i++) LR[i]=L->LR[i];

 PRF=L->PRF; PP=L->PP; propager(L->x,L->v); L--;
}

/**************************************************************/
 accrocher(x,v) int x; char v;
/**************************************************************/
{int i;

 L++; L->x=x; L->v=v; L->PP=PP; L->PRF=PRF;

 for (i=0;i<N;i++) L->V[i]=V[i];
 for (i=0;i<P;i++) L->LR[i]=LR[i];
}