walksat.c

sp组合优化算法的一个改进算法

    default:
      printf("%s", heuristic_names[heuristic]);
      break;
    }
  if (numerator>0){
    printf(", noise %d / %d", numerator, denominator);
  }
  printf("\n");
}

void print_statistics_header(void)
{
    printf("numatom = %i, numclause = %i, numliterals = %i\n",numatom,numclause,numliterals);
    printf("wff read in\n\n");
    printf("    lowest     final       avg     noise     noise     total                 avg        mean        mean\n");
    printf("    #unsat    #unsat     noise   std dev     ratio     flips              length       flips       flips\n");
    printf("      this      this      this      this      this      this   success   success       until         std\n");
    printf("       try       try       try       try       try       try      rate     tries      assign         dev\n\n");

    fflush(stdout);

}

void initialize_statistics(void)
{
    x = 0; r = 0;
    if (hamming_flag) {
	read_hamming_file(hamming_target_file);
	open_hamming_data(hamming_data_file);
    }
    tail_start_flip = tail * numatom;
    printf("tail starts after flip = %i\n", tail_start_flip);
    numnullflip = 0;


}

void update_statistics_start_try(void)
{
    int i;

    lowbad = numfalse;

    sample_size = 0;
    sumfalse = 0.0;
    sumfalse_squared = 0.0;

    for (i=0; i<HISTMAX; i++)
	tailhist[i] = 0;
    if (tail_start_flip == 0){
	tailhist[numfalse < HISTMAX ? numfalse : HISTMAX - 1] ++;
    }
	      
    if (printfalse) save_false_clauses(lowbad);
    if (printlow) save_low_assign();
}

void print_statistics_start_flip(void)
{
    if (printtrace && (numflip % printtrace == 0)){
	printf(" %9i %9i                     %9li\n", lowbad,numfalse,numflip);
	if (trace_assign)
	    print_current_assign();
	fflush(stdout);
    }
}


void update_and_print_statistics_end_try(void)
{
    int i;
    int j;

    totalflip += numflip;
    x += numflip;
    r ++;

    if (sample_size > 0){
	avgfalse = sumfalse/sample_size;
	second_moment_avgfalse = sumfalse_squared / sample_size;
	variance_avgfalse = second_moment_avgfalse - (avgfalse * avgfalse);
	if (sample_size > 1) { variance_avgfalse = (variance_avgfalse * sample_size)/(sample_size - 1); }
	std_dev_avgfalse = sqrt(variance_avgfalse);

	ratio_avgfalse = avgfalse / std_dev_avgfalse;

	sum_avgfalse += avgfalse;
	sum_std_dev_avgfalse += std_dev_avgfalse;
	number_sampled_runs += 1;

	if (numfalse == 0){
	    suc_number_sampled_runs += 1;
	    suc_sum_avgfalse += avgfalse;
	    suc_sum_std_dev_avgfalse += std_dev_avgfalse;
	}
	else {
	    nonsuc_number_sampled_runs += 1;
	    nonsuc_sum_avgfalse += avgfalse;
	    nonsuc_sum_std_dev_avgfalse += std_dev_avgfalse;
	}
    }
    else{
	avgfalse = 0;
	variance_avgfalse = 0;
	std_dev_avgfalse = 0;
	ratio_avgfalse = 0;
    }

    if(numfalse == 0){

	save_solution();
	numsuccesstry++;

	totalsuccessflip += numflip;
	integer_sum_x += x;
	sum_x = (double) integer_sum_x;
	sum_x_squared += ((double)x)*((double)x);
	mean_x = sum_x / numsuccesstry;
	if (numsuccesstry > 1){
	    second_moment_x = sum_x_squared / numsuccesstry;
	    variance_x = second_moment_x - (mean_x * mean_x);
	    /* Adjustment for small small sample size */
	    variance_x = (variance_x * numsuccesstry)/(numsuccesstry - 1);
	    std_dev_x = sqrt(variance_x);
	    std_error_mean_x = std_dev_x / sqrt((double)numsuccesstry);
	}
	sum_r += r;
	mean_r = ((double)sum_r)/numsuccesstry;
	sum_r_squared += ((double)r)*((double)r);

	x = 0;
	r = 0;
    }

    printf(" %9i %9i %9.2f %9.2f %9.2f %9li %9li",
	   lowbad,numfalse,avgfalse, std_dev_avgfalse,ratio_avgfalse,numflip, (numsuccesstry*100)/numtry);
    if (numsuccesstry > 0){
	printf(" %9i", totalsuccessflip/numsuccesstry);
	printf(" %11.2f", mean_x);
	if (numsuccesstry > 1){
	    printf(" %11.2f", std_dev_x);
	}
    }
    printf("\n");

    if (printhist){
	printf("histogram: ");
	for (j=HISTMAX-1; tailhist[j] == 0; j--);
	for (i=0; i<=j; i++){
	    printf(" %i(%i)", tailhist[i], i);
	    if ((i+1) % 10 == 0) printf("\n           ");
	}
	if (j==HISTMAX-1) printf(" +++");
	printf("\n");
    }

    if (numfalse>0 && printfalse)
	print_false_clauses(lowbad);
    if (printlow && (!printonlysol || numfalse >= target))
	print_low_assign(lowbad);

    if(numfalse == 0 && countunsat() != 0){
	fprintf(stderr, "Program error, verification of solution fails!\n");
	exit(-1);
    }

    fflush(stdout);
}

void update_statistics_end_flip(void)
{
    if (numfalse < lowbad){
	lowbad = numfalse;
	if (printfalse) save_false_clauses(lowbad);
	if (printlow) save_low_assign();
    }
    if (numflip >= tail_start_flip){
	tailhist[(numfalse < HISTMAX) ? numfalse : (HISTMAX - 1)] ++;
	if ((numflip % samplefreq) == 0){
	  sumfalse += numfalse;
	  sumfalse_squared += numfalse * numfalse;
	  sample_size ++;
	}
    }
}

void print_statistics_final(void)
{
    seconds_per_flip = expertime / totalflip;
    printf("\ntotal elapsed seconds = %f\n", expertime);
    printf("average flips per second = %d\n", (long)(totalflip/expertime));
    if (heuristic == TABU)
	printf("proportion null flips = %f\n", ((double)numnullflip)/totalflip);
    printf("number solutions found = %d\n", numsuccesstry);
    printf("final success rate = %f\n", ((double)numsuccesstry * 100.0)/numtry);
    printf("average length successful tries = %li\n", numsuccesstry ? (totalsuccessflip/numsuccesstry) : 0);
    if (numsuccesstry > 0)
	{
	    printf("mean flips until assign = %f\n", mean_x);
	    if (numsuccesstry>1){
		printf("  variance = %f\n", variance_x);
		printf("  standard deviation = %f\n", std_dev_x);
		printf("  standard error of mean = %f\n", std_error_mean_x);
	    }
	    printf("mean seconds until assign = %f\n", mean_x * seconds_per_flip);
	    if (numsuccesstry>1){
		printf("  variance = %f\n", variance_x * seconds_per_flip * seconds_per_flip);
		printf("  standard deviation = %f\n", std_dev_x * seconds_per_flip);
		printf("  standard error of mean = %f\n", std_error_mean_x * seconds_per_flip);
	    }
	    printf("mean restarts until assign = %f\n", mean_r);
	    if (numsuccesstry>1){
		variance_r = (sum_r_squared / numsuccesstry) - (mean_r * mean_r);
		if (numsuccesstry > 1) variance_r = (variance_r * numsuccesstry)/(numsuccesstry - 1);	   
		std_dev_r = sqrt(variance_r);
		std_error_mean_r = std_dev_r / sqrt((double)numsuccesstry);
		printf("  variance = %f\n", variance_r);
		printf("  standard deviation = %f\n", std_dev_r);
		printf("  standard error of mean = %f\n", std_error_mean_r);
	    }
	}

    if (number_sampled_runs){
      mean_avgfalse = sum_avgfalse / number_sampled_runs;
      mean_std_dev_avgfalse = sum_std_dev_avgfalse / number_sampled_runs;
      ratio_mean_avgfalse = mean_avgfalse / mean_std_dev_avgfalse;

      if (suc_number_sampled_runs){
	  suc_mean_avgfalse = suc_sum_avgfalse / suc_number_sampled_runs;
	  suc_mean_std_dev_avgfalse = suc_sum_std_dev_avgfalse / suc_number_sampled_runs;
	  suc_ratio_mean_avgfalse = suc_mean_avgfalse / suc_mean_std_dev_avgfalse;
      }
      else {
	  suc_mean_avgfalse = 0;
	  suc_mean_std_dev_avgfalse = 0;
	  suc_ratio_mean_avgfalse = 0;
      }

      if (nonsuc_number_sampled_runs){
	  nonsuc_mean_avgfalse = nonsuc_sum_avgfalse / nonsuc_number_sampled_runs;
	  nonsuc_mean_std_dev_avgfalse = nonsuc_sum_std_dev_avgfalse / nonsuc_number_sampled_runs;
	  nonsuc_ratio_mean_avgfalse = nonsuc_mean_avgfalse / nonsuc_mean_std_dev_avgfalse;
      }
      else {
	  nonsuc_mean_avgfalse = 0;
	  nonsuc_mean_std_dev_avgfalse = 0;
	  nonsuc_ratio_mean_avgfalse = 0;
      }

      printf("final noise level statistics\n");
      printf("    statistics over all runs:\n");
      printf("      overall mean average noise level = %f\n", mean_avgfalse);
      printf("      overall mean noise std deviation = %f\n", mean_std_dev_avgfalse);
      printf("      overall ratio mean noise to mean std dev = %f\n", ratio_mean_avgfalse);
      printf("    statistics on successful runs:\n");
      printf("      successful mean average noise level = %f\n", suc_mean_avgfalse);
      printf("      successful mean noise std deviation = %f\n", suc_mean_std_dev_avgfalse);
      printf("      successful ratio mean noise to mean std dev = %f\n", suc_ratio_mean_avgfalse);
      printf("    statistics on nonsuccessful runs:\n");
      printf("      nonsuccessful mean average noise level = %f\n", nonsuc_mean_avgfalse);
      printf("      nonsuccessful mean noise std deviation = %f\n", nonsuc_mean_std_dev_avgfalse);
      printf("      nonsuccessful ratio mean noise to mean std dev = %f\n", nonsuc_ratio_mean_avgfalse);
    }

    if (hamming_flag){
	close(hamming_fp);
	printf("Final distance to hamming target = %i\n", calc_hamming_dist(atom, hamming_target, numatom));
	printf("Hamming distance data stored in %s\n", hamming_data_file);
    }

    if (numsuccesstry > 0){
	printf("ASSIGNMENT FOUND\n");
	if(printsolcnf == TRUE) print_sol_cnf();
    }
    else
	printf("ASSIGNMENT NOT FOUND\n");

}


long super(int i)
{
    long power;
    int k;

    if (i<=0){
	fprintf(stderr, "bad argument super(%d)\n", i);
	exit(1);
    }
    /* let 2^k be the least power of 2 >= (i+1) */
    k = 1;
    power = 2;
    while (power < (i+1)){
	k += 1;
	power *= 2;
    }
    if (power == (i+1)) return (power/2);
    return (super(i - (power/2) + 1));
}

void handle_interrupt(int sig)
{
    if (abort_flag) exit(-1);
    abort_flag = TRUE;
}

void scanone(int argc, char *argv[], int i, int *varptr)
{
    if (i>=argc || sscanf(argv[i],"%i",varptr)!=1){
	fprintf(stderr, "Bad argument %s\n", i<argc ? argv[i] : argv[argc-1]);
	exit(-1);
    }
}

int calc_hamming_dist(int atom[], int hamming_target[], int numatom)
{
    int i;
    int dist = 0;
    
    for (i=1; i<=numatom; i++){
	if (atom[i] != hamming_target[i]) dist++;
    }
    return dist;
}

void open_hamming_data(char initfile[])
{
    if ((hamming_fp = fopen(initfile, "w")) == NULL){
	fprintf(stderr, "Cannot open %s for output\n", initfile);
	exit(1);
    }
}


void read_hamming_file(char initfile[])
{
    int i;			/* loop counter */
    FILE * infile;
    int lit;    

    printf("loading hamming target file %s ...", initfile);

    if ((infile = fopen(initfile, "r")) == NULL){
	fprintf(stderr, "Cannot open %s\n", initfile);
	exit(1);
    }
    i=0;
    for(i = 1;i < numatom+1;i++)
      hamming_target[i] = 0;

    while (fscanf(infile, " %d", &lit)==1){
	if (ABS(lit)>numatom){
	    fprintf(stderr, "Bad hamming file %s\n", initfile);
	    exit(1);
	}
	if (lit>0) hamming_target[lit]=1;
    }
    printf("done\n");
}


void init(char initfile[], int initoptions)
{
    int i;
    int j;
    int thetruelit;
    FILE * infile;
    int lit;

    for(i = 0;i < numclause;i++)
      numtruelit[i] = 0;
    numfalse = 0;

    for(i = 1;i < numatom+1;i++)
      {
	  changed[i] = -BIG;
	  breakcount[i] = 0;
	  makecount[i] = 0;
      }

    if (initfile[0] && initoptions!=INIT_PARTIAL){
	for(i = 1;i < numatom+1;i++)
	  atom[i] = 0;
    }
    else {
	for(i = 1;i < numatom+1;i++)
	  atom[i] = random()%2;
    }

    if (initfile[0]){
	if ((infile = fopen(initfile, "r")) == NULL){
	    fprintf(stderr, "Cannot open %s\n", initfile);
	    exit(1);
	}
	i=0;
	while (fscanf(infile, " %d", &lit)==1){
	    i++;
	    if (ABS(lit)>numatom){
		fprintf(stderr, "Bad init file %s\n", initfile);
		exit(1);
	    }
	    if (lit<0) atom[-lit]=0;
	    else atom[lit]=1;
	}
	if (i==0){
	    fprintf(stderr, "Bad init file %s\n", initfile);
	    exit(1);
	}
	close(infile);
	/* printf("read %d values\n", i); */
    }

    /* Initialize breakcount and makecount in the following: */
    for(i = 0;i < numclause;i++)
      {
	  for(j = 0;j < size[i];j++)
	    {
		if((clause[i][j] > 0) == atom[ABS(clause[i][j])])
		  {
		      numtruelit[i]++;
		      thetruelit = clause[i][j];
		  }
	    }
	  if(numtruelit[i] == 0)
	    {
		wherefalse[i] = numfalse;
		false[numfalse] = i;
		numfalse++;
		for(j = 0;j < size[i];j++){
		  makecount[ABS(clause[i][j])]++;
		}
	    }
	  else if (numtruelit[i] == 1)
	    {
		breakcount[ABS(thetruelit)]++;
	    }
      }
    if (hamming_flag){
	hamming_distance = calc_hamming_dist(atom, hamming_target, numatom);
	fprintf(hamming_fp, "0 %i\n", hamming_distance);
    }
}

void
print_false_clauses(long int lowbad)
{
    int i, j;
    int cl;

    printf("Unsatisfied clauses:\n");
    for (i=0; i<lowbad; i++){
	cl = lowfalse[i];
	for (j=0; j<size[cl]; j++){
	    printf("%d ", clause[cl][j]);
	}
	printf("0\n");
    }
    printf("End unsatisfied clauses\n");
}

void
save_false_clauses(long int lowbad)
{
    int i;

    for (i=0; i<lowbad; i++)
      lowfalse[i] = false[i];
}

void initprob(void)
{
    int i;			/* loop counter */
    int j;			/* another loop counter */
    int lastc;
    int nextc;
    int *storeptr;
    int freestore;
    int lit;

    while ((lastc = getchar()) == 'c')
      {
	  while ((nextc = getchar()) != EOF && nextc != '\n');
      }
    ungetc(lastc,stdin);
    if (scanf("p cnf %i %i",&numatom,&numclause) != 2)
      {
	  fprintf(stderr,"Bad input file: wrong p line\n");
	  exit(-1);
      }
    if(numatom > MAXATOM)
      {