/* 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;

int *make;
int *brake;
int *maxxs;
int *sat;

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

/************************ GSAT **********************/

void runSolver(SATParams *params, SATResults *results)
{
   int t, x, y, i, j, nmxs, maxdiff, curdiff, xflip = -1, temp;
   int R;
   int T;

   #include "mobility1.c"

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

	 if (T == 0)
		 T = 100000;

	 if (R == 0)
		 R = 5;

   flips = 0;

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

      for (x = 1; x <= n; x++) assign[x] = (rand()%100 < 50) * 2 - 1;
      flips++;

      numsat = 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];
         numsat += sat[y] > 0;
      }
      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"

         maxdiff = -m;
         nmxs = 0;
         for (x = 1; x <= n; x++)
            if ((curdiff = make[x]-brake[x]) > maxdiff) {
               maxdiff = curdiff;
               maxxs[nmxs = 0] = x;
			   nmxs++;
            } else if (curdiff == maxdiff)
               maxxs[nmxs++] = x;

         xflip = maxxs[rand()%nmxs];
         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]) {
               if (--sat[y] == 0) {
                  numsat--;
                  for (i = 0; i < nXs[y]; i++)
                     if (Xsgns[y][i] != assign[x=Xs[y][i]] && x != xflip)
                        make[x]++;
               } else if (sat[y] == 1)
                  for (i = 0; i < nXs[y]; i++)
                     if (Xsgns[y][i] == assign[x=Xs[y][i]] && x != xflip)
                        brake[x]++;
            } else {
               if (++sat[y] == 1) {
                  numsat++;
                  for (i = 0; i < nXs[y]; i++)
                     if (Xsgns[y][i] != assign[x=Xs[y][i]] && x != xflip) 
                        make[x]--;
               } else if (sat[y] == 2)
                  for (i = 0; i < nXs[y]; i++)
                     if (Xsgns[y][i] == assign[x=Xs[y][i]] && x != xflip) 
                        brake[x]--;
            }
         }
/*		 if (maxdiff < 0) printf("step down!\n");
		 if (maxdiff < 0) break;
*/
      }                           /***************************/
      if (numsat == m) break;
   }													 /***************************/

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

   #include "mobility3.c"
}

void postSolve(SATParams *params)
{
   free(make);
   free(brake);
   free(maxxs);
   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 = 0;
	params->numStringParams = 0;

	return params;
	}

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