/* 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 numvio, steps, r;

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

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

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

void preSolve(SATParams *params)
{
	make = malloc(n * sizeof(int));
	brake = malloc(n * 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 cursteps;

#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;

	steps = 0;

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

		for (x = 0; x < n; x++) 
			X[x] = (rand() > HALF_RAND_MAX) * 2 - 1;
		steps++;

		numvio = 0;
		for (y = 0; y < m; y++) {
			sat[y] = 0;
			for (i=0; i<nXs[y]; i++) 
				sat[y] += X[Xs[y][i]] == Xsgns[y][i];
			numvio += sat[y] == 0;
		}
		for (x = 0; 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 && X[x] == Ysgns[x][j])
					brake[x]++;
			}
		}
		cursteps = 0;

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

			if (numvio == 0) 
				break;

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

			xflip = rand() % n;

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

				X[xflip] = -X[xflip];
				cursteps++;
				steps++;
				temp = make[xflip];
				make[xflip] = brake[xflip];
				brake[xflip] = temp;

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

	if (numvio > 0) 
		r--;

	results->numFlips = steps;
	results->numRestarts = r + 1;
	results->numSatisfied = m - numvio;
	results->isSatisfied = numvio == 0;
	#include "copysoln.c"

#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.21 $ $Date: 2001/11/23 06:46:20 $";
}