/* Copyright (C) 2000  Dale Schuurmans, Finnegan Southey                     */
/* This work is licensed under the Gnu General Public License (see gpl.txt). */

#include <stdlib.h>
#include <stdio.h>
#include "satfront.h"
#include "readcnf.h"

int *yfalse, *wherefalse, *lastime, nfalse;
int numsat, flips, r;
int *make;
int *brake;
int *sat;

/************************ WSAT - NOVELTY **********************/

void preSolve(SATParams *params)
{
   make = malloc((n+1) * sizeof(int));
   brake = malloc((n+1) * sizeof(int));                             
	 sat = malloc(m * sizeof(int));
   yfalse = malloc(m * sizeof(int));
   wherefalse = malloc(m * sizeof(int));
   lastime = malloc((n+1) * sizeof(int));
}

void runSolver(SATParams *params, SATResults *results)
{
   int t, x, y, i, j, xflip = -1, temp, nfalse;
   int R;
   int T;
   int x2, diff2, diff, maxdiff, recent;
	 double hoosProb;
	 int hoosProbInt;
 	 
	 #include "mobility1.c"

	 T =  params->intParams[0];
	 R = params->intParams[1];
	 hoosProb = params->doubleParams[0];

	 if (T == 0)
		 T = 100000;

	 if (R == 0)
		 R = 5;

	 if (hoosProb == 0)
		 hoosProbInt = 0;
	 else
		 hoosProbInt = (int)RAND_MAX * hoosProb;

   flips = 0;

   for (r = 0; r < R; r++) {  /***************************/

      for (x = 1; x <= n; x++) assign[x] = (rand()%2 > 0) * 2 - 1;
      for (x = 0; x <= n; x++) lastime[x] = -1;
      flips++;
      numsat = nfalse = 0;
      for (y = 0; y < m; y++) {
         sat[y] = 0;
         for (i=0; i<nXs[y]; i++) sat[y] += assign[Xs[y][i]] == Xsgns[y][i];
         if (sat[y] > 0) 
            numsat++;
         else {
            yfalse[nfalse] = y;
            wherefalse[y] = nfalse;
            nfalse++;
         }
      }
      for (x = 1; x <= n; x++) {
         make[x] = brake[x] = 0;
         for (j = 0; j < nYs[x]; j++)
            if (sat[Ys[x][j]] == 0)
               make[x]++;
            else if (sat[Ys[x][j]] == 1 && assign[x] == Ysgns[x][j])
               brake[x]++;
      }

      for (t = 0; t < T; t++) { /***************************/

         if (numsat == m) break;

				 #include "unsat1.c"
	       #include "mobility2.c"
         #include "assigndump.c"

         y = yfalse[rand()%nfalse];

				    /* Hoos fix for novelty. */
				 if (hoosProbInt > 0 && rand() < hoosProbInt) {
					 xflip = Xs[y][rand() / (RAND_MAX / nXs[y] + 1)];
				 } else {
	         maxdiff = diff2 = -m;
	         xflip = x2 = 0;
	         recent = -1;
	         for (i = 0; i < nXs[y]; i++) {
	            x = Xs[y][i];
	            if (lastime[x] > recent) recent = lastime[x];
	            diff = make[x] - brake[x];
	            if (diff > maxdiff ||
	                     (diff == maxdiff && lastime[x] < lastime[xflip])) {
	               diff2 = maxdiff;
	               maxdiff = diff;
	               x2 = xflip;
	               xflip = x;
	            } else if (diff > diff2 ||
	                     (diff == diff2 && lastime[x] < lastime[x2])) {
	                  diff2 = diff;
	                  x2 = x;
	            }
	         }
	         if (lastime[xflip] == recent && rand()%100 < 50) xflip = x2;
				 }
         lastime[xflip] = t;
         assign[xflip] = -assign[xflip];
         flips++;

         temp = make[xflip];
         make[xflip] = brake[xflip];
         brake[xflip] = temp;

         for (j = 0; j < nYs[xflip]; j++) {
            y = Ys[xflip][j];
            if (assign[xflip] != Ysgns[xflip][j]) {
               sat[y]--;
               if (sat[y] == 0) {
                  numsat--;
                  yfalse[nfalse] = y;
                  wherefalse[y] = nfalse;
                  nfalse++;
                  for (i = 0; i < nXs[y]; i++)
                     if ((x = Xs[y][i]) != xflip && Xsgns[y][i] != assign[x])
						make[x]++;
               } else if (sat[y] == 1)
                  for (i = 0; i < nXs[y]; i++)
                     if ((x = Xs[y][i]) != xflip && Xsgns[y][i] == assign[x])
					    brake[x]++;
            } else {
               sat[y]++;
               if (sat[y] == 1) {
                  numsat++;
                  nfalse--;
                  yfalse[wherefalse[y]] = yfalse[nfalse];
                  wherefalse[yfalse[nfalse]] = wherefalse[y];
                  for (i = 0; i < nXs[y]; i++)
                     if ((x = Xs[y][i]) != xflip && Xsgns[y][i] != assign[x])
					    make[x]--;
               } else if (sat[y] == 2)
                  for (i = 0; i < nXs[y]; i++)
                     if ((x = Xs[y][i]) != xflip && Xsgns[y][i] == assign[x])
						brake[x]--;
            }
         }
      }                           /***************************/
      if (numsat == m) break;
   }                             /***************************/

	if (numsat != m) 
		r--;

	 results->numFlips = flips;
	 results->numRestarts = r + 1;
	 results->numClauses = m;
	 results->numSatisfied = numsat;
	 results->isSatisfied = numsat == m;

   #include "mobility3.c"
}

void postSolve(SATParams *params)
{
   free(make);
   free(brake);
   free(yfalse);
   free(wherefalse);
   free(lastime);
   free(sat);
}

SATParams *getSATParams()
	{
	SATParams *params;

	params = malloc(sizeof(SATParams));
	params->numIntParams = 2;
	params->intParams = malloc(params->numIntParams * sizeof(int));
	params->intParamNames = malloc(params->numIntParams * sizeof(char*));
	params->intParamDescs = malloc(params->numIntParams * sizeof(char*));
	params->intParamNames[0] = "-mf";
	params->intParamDescs[0] = "max flips before restarting";
	params->intParams[0] = 0;
	params->intParamNames[1] = "-mr";
	params->intParamDescs[1] = "max restarts before aborting";
	params->intParams[1] = 0;

	params->numDoubleParams = 1;
	params->doubleParams = malloc(params->numDoubleParams * sizeof(double));
	params->doubleParamNames = malloc(params->numDoubleParams * sizeof(char*));
	params->doubleParamDescs = malloc(params->numDoubleParams * sizeof(char*));
	params->doubleParamNames[0] = "-hoos";
	params->doubleParamDescs[0] = "Hoos fix prob for novelty (*0.01)";
	params->doubleParams[0] = 0.01;
	
	params->numStringParams = 0;

	return params;
	}

char *getSolverIdentity()
	{
	return "$RCSfile: wnovel.c,v $ $Revision: 1.16 $ $Date: 2000/12/10 06:03:56 $";
	}