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

int numsat, flips, r;

/************************ SIMULATED ANNEALING **********************/

double drand48();
double exp(double);
double sqrt(double);

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

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

void runSolver(SATParams *params, SATResults *results)
{
   int x, y, i, j, xflip = -1, temp;
   int R;
   int T;
   double temper;
	 int curflips;

   #include "mobility1.c"
 
	 T =  params->intParams[0];
	 R = params->intParams[1];
	 temper = params->doubleParams[0];

	 if (T == 0)
		 T = 100000;

	 if (R == 0)
		 R = 5;

	 if (temper == 0)
		 temper = 0.2;
  
   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]++;
         }
      }
			curflips = 0;

      while (curflips < T) { /***************************/

         if (numsat == m) break;
 				 
				 #include "unsat1.c"
				 #include "mobility2.c"
         #include "assigndump.c"

         xflip = rand()%n + 1;

         if ( make[xflip] - brake[xflip] >= 0 || 
              drand48() < exp( (make[xflip]-brake[xflip])/temper )) {

            assign[xflip] = -assign[xflip];
						curflips++;
            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 (numsat == m) break;
   }                             /***************************/

	 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(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] = "-tm";
	params->doubleParamDescs[0] = "temperature";
	params->doubleParams[0] = 0;

	params->numStringParams = 0;

	return params;
	}

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