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

int steps, r;

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

int *minbrake;

void preSolve(SATParams *params)
{
	make = malloc(n * sizeof(int));
	brake = malloc(n * 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;
	int R = 100;
	int T = 100000;
	double noiseProb;
	int noiseProbInt;

#include "mobility1.c"

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

	if (T == 0)
		T = 100000;

	if (R == 0)
		R = 5;

	if (noiseProb == 0)
		noiseProb = 0.5;

	noiseProbInt = (int)RAND_MAX * noiseProb;

	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];
			if (sat[y] <= 0) {
				yfalse[numvio] = y;
				wherefalse[y] = numvio;
				numvio++;
			}
		}
		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]++;
		}

		if (numvio == 0)
			goto finished;

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

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

			y = yfalse[rand()%numvio];

			#ifdef WSATB
				/* 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];
				}
			#endif

			#ifdef WSATG
				/* 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];
				}
			#endif

			#ifdef WSATSKC
				/* 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];
			#endif

			nYsx = nYs[xflip];
			X[xflip] = -X[xflip];
			steps++;

				/* The included code performs the make/break update. */
			#include "mbflipimpl.c"

			if (numvio == 0)
				goto finished;		/* Found solution so jump to label. */
		}                           /***************************/
	} /***************************/


	/* We only reach this point if we exited the above loop without finding a
	* solution. **/
	r--;

	/* We jump to this label when we find a solution. */
finished:

	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(yfalse);
	free(wherefalse);
	free(minbrake);
	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] = "-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.30.6.1 $ $Date: 2002/09/22 01:38:21 $";
}