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

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

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

/************************ HSAT **********************/

void runSolver(SATParams *params, SATResults *results)
{
	int t, x, y, i, j, nmxs, maxdiff, curdiff, xflip = -1, temp, oldest, currage;
	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;

	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++) {
			timestamp[x] = -1;
			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]++;
			}
		}

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

			if (numvio == 0) break;

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

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


			xflip = maxxs[rand()%nmxs];
			timestamp[xflip] = t;
			X[xflip] = -X[xflip];
			steps ++;

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

			for (j = 0; j < nYs[xflip]; j++) {
				int y, i, x;

				y = Ys[xflip][j];
				if (X[xflip] != Ysgns[xflip][j]) { 
					/* 'xflip' is no longer satisfying 'y'. */
					sat[y]--;
					if (sat[y] == 0) {
						/* 'y' is newly falsified. */
						/* Need to update all but 'xflip'. */
						numvio++;

						for (i = 0; i < nXs[y]; i++) {
							if ((x = Xs[y][i]) != xflip)
								make[x]++;
						}
					} else if (sat[y] == 1) {
						/* Need to update single satisying var. */
						int *Xptr;
						int *Xsgnsyptr;

						Xptr = Xs[y];
						Xsgnsyptr = Xsgns[y];
						x = *Xptr;
						while (*Xsgnsyptr != X[x]) {
							Xptr++;
							Xsgnsyptr++;
							x = *Xptr;
						}
						brake[x]++;
					}
				} else {
					/* 'xflip' is now satisfying 'y'. */
					sat[y]++;
					if (sat[y] == 1) {
						/* 'y' is newly satisfied. */
						/* Need to update all but 'xflip'. */
						numvio--;

						for (i = 0; i < nXs[y]; i++)
							if ((x = Xs[y][i]) != xflip)
								make[x]--;
					} else if (sat[y] == 2) {
						int *Xptr;
						int *Xsgnsyptr;

						Xptr = Xs[y];
						Xsgnsyptr = Xsgns[y];
						x = *Xptr;
						while (*Xsgnsyptr != X[x] || x == xflip) {
							Xptr++;
							Xsgnsyptr++;
							x = *Xptr;
						}
						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(maxxs);
	free(sat);
	free(timestamp);
}

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: hsat.c,v $ $Revision: 1.23 $ $Date: 2001/11/23 06:46:20 $";
}