/* 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 "readcnf.h"
#include "satfront.h"

int numsat, flips, r;

/************************ WSAT - SKC (also G and B) (WALKSAT) **********************/

int *make;
int *brake;
int *yfalse;
int *wherefalse;
int *minbrake;
int *sat;


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

void runSolver(SATParams *params, SATResults *results)
{
   int nYsx, nXsy, minbrk, curbrk, nmin;
   int t, x, y, i, j, xflip = -1, temp, nfalse;
   int R = 100;
   int T = 100000;
	 double noiseProb;
	 int noiseProbInt;
	 int useWSATB, useWSATG;

	 #include "mobility1.c"
	 
	 T =  params->intParams[0];
	 R = params->intParams[1];
	 useWSATG = params->intParams[2];
	 useWSATB = params->intParams[3];
	 noiseProb = params->doubleParams[0];

	 if (T == 0)
		 T = 100000;

	 if (R == 0)
		 R = 5;

	 if (useWSATG && useWSATB) {
	    fprintf(stderr, "Cannot use WSAT B and WSAT G strategies together, exiting.\n");
			exit(1);
	 }

	 if (noiseProb == 0)
		 noiseProb = 0.5;

	 noiseProbInt = (int)RAND_MAX * noiseProb;

   flips = 0;

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

      for (x = 1; x <= n; x++) assign[x] = (rand()%2 > 0) * 2 - 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];

				 if (useWSATB) {
					    /* WSAT B */
            nXsy = nXs[y];
            if (rand() < noiseProbInt) {
               xflip = Xs[y][rand()%nXsy];
	  			  } else {
               nmin = 0;
               minbrk = m;
               for (i = 0; i < nXsy; i++) {
                  x = Xs[y][i];
                  if ((curbrk = brake[x]) <= minbrk) {
                     if (curbrk < minbrk) nmin = 0;
                     minbrk = curbrk;
                     minbrake[nmin++] = x;
                  }
               }
   						xflip = minbrake[rand()%nmin];
						}
				 } else if (useWSATG) {
					     /* WSAT G */
            nXsy = nXs[y];
            if (rand() < noiseProbInt) {
               xflip = Xs[y][rand()%nXsy];
   				 } else {
               nmin = 0;
               minbrk = m;
               for (i = 0; i < nXsy; i++) {
                  x = Xs[y][i];
                  if ((curbrk = brake[x] - make[x]) <= minbrk) {
                     if (curbrk < minbrk) nmin = 0;
                     minbrk = curbrk;
                     minbrake[nmin++] = x;
                  }
               }
               
   						xflip = minbrake[rand()%nmin];
   				 }
				 } else {
   				    /* WSAT SKC */
            nXsy = nXs[y];
            nmin = 0;
            minbrk = m;
            for (i = 0; i < nXsy; i++) {
               x = Xs[y][i];
               if ((curbrk = brake[x]) <= minbrk) {
                  if (curbrk < minbrk) nmin = 0;
                  minbrk = curbrk;
                  minbrake[nmin++] = x;
               }
            }
            if (minbrk > 0 && rand() < noiseProbInt) 
               xflip = Xs[y][rand()%nXsy];
            else if (nmin == 1)
               xflip = minbrake[0];
            else
               xflip = minbrake[rand()%nmin];
				 }


         nYsx = nYs[xflip];
         assign[xflip] = -assign[xflip];
         flips += 1;

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

         for (j = 0; j < nYsx; j++) {
            y = Ys[xflip][j];
            nXsy = nXs[y];
            if (assign[xflip] * Ysgns[xflip][j] < 0) {
               sat[y]--;
               if (sat[y] == 0) {
                  numsat--;
                  yfalse[nfalse] = y;
                  wherefalse[y] = nfalse;
                  nfalse++;
                  for (i = 0; i < nXsy; i++)
                     if ((x = Xs[y][i]) != xflip && Xsgns[y][i] != assign[x])
					    make[x]++;
               } else if (sat[y] == 1)
                  for (i = 0; i < nXsy; 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 < nXsy; i++)
                     if ((x = Xs[y][i]) != xflip && Xsgns[y][i] != assign[x])
					    make[x]--;
               } else if (sat[y] == 2)
                  for (i = 0; i < nXsy; 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(minbrake);
   free(sat);
}

SATParams *getSATParams()
	{
	SATParams *params;

	params = malloc(sizeof(SATParams));
	params->numIntParams = 4;
	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->intParamNames[2] = "-wsatg";
	params->intParamDescs[2] = "(0*/1) use WSAT G strategy";
	params->intParams[2] = 0;
	params->intParamNames[3] = "-wsatb";
	params->intParamDescs[3] = "(0*/1) use WSAT B strategy";
	params->intParams[3] = 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] = "-noise";
	params->doubleParamDescs[0] = "noise (greed-random) prob.";
	params->doubleParams[0] = 0;

	params->numStringParams = 0;

	return params;
	}

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