/******************************************************************/
/*                           gensatexp.c                          */
/******************************************************************/
/*         Generation d'une donnee 3-SAT difficile "in.dat"       */
/******************************************************************/

#include <stdio.h>

int N; /* valeur du nombre de variables */
int P; /* valeur du nombre de clauses   */
int R; /* valeur de la longueur des clauses */
int D; /* facteur proportionnel a la taille de la donnee */

int *REP,*SATx,*SATv;
int *s,*t;

FILE *f;


/******************************************************************/
 gen_SAT(j1,j2,j3,s1,s2,s3) int j1,j2,j3,s1,s2,s3;
/******************************************************************/
{
 *s= j1; s++; *s= j2; s++; *s= j3; s++;
 *s= j1; s++; *s= j2; s++; *s= j3; s++;
 *s= j1; s++; *s= j2; s++; *s= j3; s++;
 *s= j1; s++; *s= j2; s++; *s= j3; s++;

 *t= s1; t++; *t= s2; t++; *t= s3; t++;
 *t=-s1; t++; *t=-s2; t++; *t= s3; t++;
 *t= s1; t++; *t=-s2; t++; *t=-s3; t++;
 *t=-s1; t++; *t= s2; t++; *t=-s3; t++;
}
 
/******************************************************************/
 main(argc,argv) int argc; char *argv[];
/******************************************************************/
{ int i,j,k;

 if (argc>1) sscanf(argv[1],"%d",&D);
 else { fprintf(stderr,"degree (d) = "); scanf("%d",&D); }

 N=3*D; P=8*D; R=3;
 fprintf(stderr,"variables (n) = %d\n",N);
 fprintf(stderr,"clauses (p) = %d\n",P);
 fprintf(stderr,"length of clauses (r) = %d\n",R);

 REP=(int *) malloc((N+1)*sizeof(int));
 SATx=(int *) malloc(P*R*sizeof(int));
 SATv=(int *) malloc(P*R*sizeof(int));

 s=SATx; t=SATv;
 for (i=1;i<=D;i++) gen_SAT(2*i-1,2*i,2*i+1,1,1,1);
 for (i=1;i<D;i++) gen_SAT(2*D+i+1,2*(D-i)+2,2*D+i,1,1,1);
 gen_SAT(1,2,3*D,1,1,-1);

 for (i=1;i<D;i++) REP[2*i+1]=i; k=D-1;
 for (i=1;i<D;i++) REP[2*D+i+1]=k+i; k=k+D-1;
 REP[1]=k+1; k=k+1;
 for (i=1;i<=D;i++) REP[2*i]=k+i; k=k+D;
 REP[2*D+1]=k+1; 

 f=fopen("in.dat","w");
 if (f==NULL) 
  printf("Erreur : ouverture du fichier \"%s\"\n","in.dat");
 fprintf(f,"d = %d\nn = %d\np = %d\nr = %d\n",D,N,P,R);
 for (s=SATx,t=SATv,i=0;i<P;i++) {
  for (j=0;j<R;j++,s++,t++) fprintf(f,"%3d ",*t*REP[*s]);
  fprintf(f,"\n");
 }
 fclose(f);

 printf("\n");
 /* printf("%d\n",D); */

}