/******************************************************************************
  A template program for MAXSAT solver. Subroutines to read instance data and
  compute the objective value of a given solution are included.

  This program can also be used to compute the objective value of a solution
  given from a file. The format of a file is:
    for each variable j from 1 to n in this order, the value of the truth
    assignment (true = 1,  false = 0).
  For example, if n=4, and variables 1 and 4 are assigned true while variables
  2 and 3 are assigned false, then the data in the file should be as follows:
  1 0 0 1. (It is safer to put a space before the first value in such a file
  to avoid errors.)

  NOTE: Index of variables ranges from 0 to n-1 and
        index of clauses ranges from 0 to m-1 in the program,
	while in the data files of the instances,
        index of variables ranges from 1 to n and
	index of clauses ranges from 1 to m.

  If you would like to use various parameters, it might be useful to modify
  the definition of struct "Param" and mimic the way the default value of
  "timelim" is given and how its value is input from the command line.
******************************************************************************/

#include <stdio.h>
#include <stdlib.h>
#include <limits.h>
#include <math.h>
#include "cpu_time.c"

/***** default values of parameters ******************************************/
#define	TIMELIM	600	/* the time limit for the algorithm in seconds */
#define	GIVESOL	0	/* 1: input a solution; 0: do not give a solution */
#define	OUTBESTSOL 0	/* 1: output a solution; 0: do not output a solution */
#define	OUTINST 0	/* 1: output the instance; 0: do not output it */

typedef struct {
  int		timelim;	/* the time limit for the algorithm in secs. */
  int		givesol;	/* give a solution (1) or not (0) */
  int		outbestsol;	/* output the best solution (1) or not (0) */
  int		outinst;	/* output the instance (1) or not (0) */
  /* Never modify the above three lines.  */
  /* You can add more components below. */
} Param;			/* parameters */

typedef struct {
  int	n;		/* number of variables */
  int	m;		/* number of clauses */
  int	*w;		/* weight of each clause */
  int	*nlit;		/* number of literals for each clause */
  int	**lit;		/* literals for each clause */
  int	**clause[2];	/* clauses that include a literal */
  int	*nclause[2];	/* number of clauses that includes a literal */
} MSATdata;		/* data of the MAXSAT */

typedef struct {
  double	timebrid;	/* the time before reading the instance data */
  double	starttime;	/* the time the search started */
  double	endtime;	/* the time the search ended */
  int		*bestsol;	/* the best solution found so far */
  /* Never modify the above four lines. */
  /* You can add more components below. */
} Vdata;		/* various data often necessary during the search */

/*************************** functions ***************************************/
void copy_parameters(int argc, char *arcv[], Param *param);
void read_instance(MSATdata *msatdata);
void output_instance(MSATdata *msatdata);
void prepare_memory(Vdata *vdata, MSATdata *msatdata);
void free_memory(Vdata *vdata, MSATdata *msatdata);
void read_sol(Vdata *vdata, MSATdata *msatdata);
void recompute_obj(Vdata *vdata, MSATdata *msatdata, Param *param);
void *malloc_e(size_t size);

/***** check the feasibility and recompute the cost **************************/
/***** NEVER MODIFY THIS SUBROUTINE! *****************************************/
void recompute_obj(Vdata *vdata, MSATdata *msatdata, Param *param)
{
  int	i, j;		/* indices */
  int	truelit;	/* index */
  int	nclause_i;	/* index */
  int	sum;		/* sum of the weights of satisfied clauses */
  int	*nt;		/* number of literals with value 1 for each clause i */

  nt = (int *) malloc_e(msatdata->m * sizeof(int)); 
  for(i=0; i<msatdata->m; i++) nt[i] = 0;
  for(i=0; i<msatdata->n; i++) {
    truelit = 1-vdata->bestsol[i];
    nclause_i = msatdata->nclause[truelit][i];
    for(j=0; j<nclause_i; j++) nt[msatdata->clause[truelit][i][j]]++;
  }
  sum=0;
  for(i=0; i<msatdata->m; i++) if(nt[i]>0) sum += msatdata->w[i];
  free((void *) nt);

  /**** output ****/
  printf("recomputed objective value = %d\n", sum);
  printf("time for the search:       %7.2f seconds\n",
	 vdata->endtime - vdata->starttime);
  printf("time to read the instance: %7.2f seconds\n",
	 vdata->starttime - vdata->timebrid);
  if(param->outbestsol == 1) {
    printf("solution:");
    for(i=0; i<msatdata->n; i++) printf(" %d", vdata->bestsol[i]);
    printf("\n");
  }
}

/***** read a solution from STDIN ********************************************/
void read_sol(Vdata *vdata, MSATdata *msatdata)
{
  int	j;		/* index of variables */
  int	value_read;	/* the value read by fscanf */
  FILE	*fp=stdin;	/* set fp to the standard input */

  for(j=0; j<msatdata->n; j++){
    fscanf(fp, "%d", &value_read);
    vdata->bestsol[j] = value_read;
  }
}

/***** prepare memory space **************************************************/
/***** Feel free to modify this subroutine. **********************************/
void prepare_memory(Vdata *vdata, MSATdata *msatdata)
{
  int j;

  vdata->bestsol = (int *)  malloc_e(msatdata->n * sizeof(int));
  /* the next line is just to avoid confusion */
  for(j=0; j<msatdata->n; j++){vdata->bestsol[j] = 0;}
}

/***** free memory space *****************************************************/
/***** Feel free to modify this subroutine. **********************************/
void free_memory(Vdata *vdata, MSATdata *msatdata)
{
  int i;

  free((void *) vdata->bestsol);
  free((void *) msatdata->w);
  free((void *) msatdata->nlit);
  for(i=0; i<msatdata->m; i++) free((void *) msatdata->lit[i]);
  free((void *) msatdata->lit);
  free((void *) msatdata->nclause[0]);
  for(i=0; i<msatdata->n; i++) free((void *) msatdata->clause[0][i]);
  free((void *) msatdata->clause[0]);

}

/***** read the instance data ************************************************/
/***** NEVER MODIFY THIS SUBROUTINE! *****************************************/
void read_instance(MSATdata *msatdata)
{
  int	i, j;		/* indices */
  int	temp;		/* temporary value used for convenience */
  int	value_read;	/* the value read by fscanf */
  int	**frontier[2];	/*  */
  FILE	*fp=stdin;	/* set fp to the standard input */

  /* read the number of agents and jobs */
  fscanf(fp, "%d", &value_read);	/* number of variables */
  msatdata->n = value_read;
  fscanf(fp,"%d",&value_read);		/* number of clauses */
  msatdata->m = value_read;

  /* initialize memory */
  msatdata->w    = (int *)  malloc_e(msatdata->m * sizeof(int));
  msatdata->nlit = (int *)  malloc_e(msatdata->m * sizeof(int));
  msatdata->lit  = (int **) malloc_e(msatdata->m * sizeof(int *));

  for(i=0; i<msatdata->m; i++){
    fscanf(fp, "%d", &value_read);      /* read #variables in clause i */
    msatdata->nlit[i] = value_read;
    fscanf(fp, "%d", &value_read);      /* read the weight of clause i */
    msatdata->w[i] = value_read;
    msatdata->lit[i] = (int *) malloc_e(msatdata->nlit[i] * sizeof(int));
    for(j=0; j<msatdata->nlit[i]; j++){ /* read the literals of clause i */
      fscanf(fp, "%d", &value_read);
      msatdata->lit[i][j] = value_read;
    }
  }

  /**** count the number of pos/neg clauses for each variable ****/
  msatdata->nclause[0] = (int *) malloc_e(2 * msatdata->n * sizeof(int));
  msatdata->nclause[1] = msatdata->nclause[0] + msatdata->n;
  for(i=0; i<msatdata->n; i++) {
    msatdata->nclause[0][i] = msatdata->nclause[1][i] = 0;
  }
  for(i=0; i<msatdata->m; i++) {
    for(j=0; j<msatdata->nlit[i]; j++) {
      temp = msatdata->lit[i][j];
      if(temp<0) msatdata->nclause[1][-temp-1]++;
      else       msatdata->nclause[0][temp-1]++;
    }
  }

  /**** make the list of clauses for each literal ****/
  msatdata->clause[0] = (int **) malloc_e(2 * msatdata->n * sizeof(int *));
  msatdata->clause[1] = msatdata->clause[0] + msatdata->n;
  for(i=0; i<msatdata->n; i++){
    msatdata->clause[0][i] =
      (int *) malloc_e((msatdata->nclause[0][i] + msatdata->nclause[1][i])
		       * sizeof(int));
    msatdata->clause[1][i] = msatdata->clause[0][i] + msatdata->nclause[0][i];
  }
  frontier[0] = (int **) malloc_e(2 * msatdata->n * sizeof(int *));
  frontier[1] = frontier[0] + msatdata->n;
  for(i=0; i<msatdata->n; i++) {
    frontier[0][i] = msatdata->clause[0][i];
    frontier[1][i] = msatdata->clause[1][i];
  }
  for(i=0; i<msatdata->m; i++) {
    for(j=0; j<msatdata->nlit[i]; j++) {
      temp = msatdata->lit[i][j];
      if(temp<0) *frontier[1][-temp-1]++ = i;
      else       *frontier[0][temp-1]++  = i;
    }
  }
  free((void *) frontier[0]);
}

/***** output the instance for debugging *************************************/
void output_instance(MSATdata *msatdata)
{
  int i, j, nlit_i;

  printf("%d variables,  %d clauses\n", msatdata->n, msatdata->m);
  printf("clause #lit weight literals\n");
  for(i=0; i<msatdata->m; i++) {
    nlit_i = msatdata->nlit[i];
    printf("%4d  [  %2d, %3d]:", i+1, nlit_i, msatdata->w[i]);
    for(j=0; j<nlit_i; j++) printf(" %3d", msatdata->lit[i][j]);
    printf("\n");
  }
  printf("val npos/nneg  clauses");
  for(i=0; i<msatdata->n; i++) {
    printf("\n%3d npos=%3d:", i+1, msatdata->nclause[0][i]);
    for(j=0; j<msatdata->nclause[0][i]; j++)
      printf(" %3d", msatdata->clause[0][i][j]+1);
    printf("\n    nneg=%3d:", msatdata->nclause[1][i]);
    for(j=0; j<msatdata->nclause[1][i]; j++)
      printf(" %3d", msatdata->clause[1][i][j]+1);
  }
  printf("\n");
}

/***** copy and read the parameters ******************************************/
/***** Feel free to modify this subroutine. **********************************/
void copy_parameters(int argc, char *argv[], Param *param)
{
  int i;

  /**** copy the parameters ****/
  param->timelim    = TIMELIM;
  param->givesol    = GIVESOL;
  param->outbestsol = OUTBESTSOL;
  param->outinst    = OUTINST;
  /**** read the parameters ****/
  if(argc>0 && (argc % 2)==0){
    printf("USAGE: ./template [param_name, param_value] [name, value]...\n");
    exit(EXIT_FAILURE);}
  else{
    for(i=1; i<argc; i+=2){
      if(strcmp(argv[i],"timelim")==0)    param->timelim    = atoi(argv[i+1]);
      if(strcmp(argv[i],"givesol")==0)    param->givesol    = atoi(argv[i+1]);
      if(strcmp(argv[i],"outbestsol")==0) param->outbestsol = atoi(argv[i+1]);
      if(strcmp(argv[i],"outinst")==0)    param->outinst    = atoi(argv[i+1]);
    }
  }
}

/***** malloc with error check ***********************************************/
void *malloc_e( size_t size ) {
  void *s;
  if ( (s=malloc(size)) == NULL ) {
    fprintf( stderr, "malloc : Not enough memory.\n" );
    exit( EXIT_FAILURE );
  }
  return s;
}

/***** main ******************************************************************/
int main(int argc, char *argv[])
{
  Param		param;		/* parameters */
  MSATdata	msatdata;	/* MAXSAT instance data */
  Vdata		vdata;		/* various data often needed during search */

  vdata.timebrid = cpu_time();
  copy_parameters(argc, argv, &param);
  read_instance(&msatdata);
  if(param.outinst==1) output_instance(&msatdata);
  prepare_memory(&vdata, &msatdata);
  if(param.givesol==1){read_sol(&vdata, &msatdata);}
  vdata.starttime = cpu_time();

  /*
    Write your algorithm here. Of course you can add your subroutines
    outside main(). At this point, the instance data is stored in "msatdata".
      msatdata.n		the number of variables n
      msatdata.m		the number of clauses m
      msatdata.w[i]		the weight of clause i (i=0,1,...,m-1)
      msatdata.nlit[i]		the number of literals in clause i
      				(i=0,1,...,m-1)
      msatdata.lit[i]		the list of literals in clause i, where
				msatdata.lit[i][k] is the k-th literal in
				the list
      				(k=0,1,...,msatdata.nlit[i]-1, i=0,1,...,m-1)
      msatdata.nclause[0][j]	the number of clauses that include the positive
      				literal of variable x_j	(j=0,1,...,n-1)
      msatdata.nclause[1][j]	the number of clauses that include the negative
				literal of variable x_j	(j=0,1,...,n-1)
      msatdata.clause[0][j]	the list of clauses that includes the positive
				literal of variable x_j, where
				msatdata.clause[0][j][k] is the k-th clause in
				the list (k=0,1,...,msatdata.nclause[0][i]-1,
				j=0,1,...,n-1)
      msatdata.clause[1][j]	the list of clauses that includes the positive
				literal of variable x_j, where
				msatdata.clause[1][j][k] is the k-th clause in
				the list (k=0,1,...,msatdata.nclause[1][i]-1,
				j=0,1,...,n-1)
    Note that  you should write, e.g., "msatdata->w[i]" in your subroutines.
    Store your best solution in vdata.bestsol, then "recompute_obj" will
    compute its objective value. The format of vdata.bestsol is: For each
    variable j from 0 to n-1 in this order, the truth assignment of the
    variable. For example, if n=4, and variables 1 and 4 are assigned true
    while variables 2 and 3 are assigned false, then vdata.bestsol should be
    as follows:  
	vdata.bestsol[0] = 1
	vdata.bestsol[1] = 0
	vdata.bestsol[2] = 0
	vdata.bestsol[3] = 1.
    Note that you should write "vdata->bestsol[j]" in your subroutines.
  */

  vdata.endtime = cpu_time();
  recompute_obj(&vdata, &msatdata, &param);
  free_memory(&vdata, &msatdata);

  return EXIT_SUCCESS;
}