/* Implements the WALKSAT CNF solver */

#include<stdlib.h>
#include<limits.h>
#include "../includes/globals.h"
#include "WalkSat.h"

int WalkSat(float prob_rand_walk,int max_flips,int max_tries,int *flipNum, int *retryNum,int *literalAssignment)
{
    int try,flip,lit_no,lit_number;
    int clause_num,lit_num_in_clause;
    int unSatClauseNum;
    double r;
    LITERAL lit_node;


    for ( try = 1 ; try <= max_tries ; try++) {
    	if ( literalAssignment == NULL ) {
    		/* Perform a random assignment of TRUE/FALSE to the 
       		literals in the clauses */
    		srand(time(NULL));
    		for( lit_no = 0 ; lit_no < numberOfLiterals ; lit_no++ ) {
        		r = fabs( (double)rand() / (double)(RAND_MAX) ); // r in [0,1]
	    		if ( r < 0.5 )
		    		literals[lit_no].value = -(lit_no+1);
	    		else
		    		literals[lit_no].value = (lit_no+1);
    		}
    	}
	else { // Initialization is provided by external program
    		for( lit_no = 0 ; lit_no < numberOfLiterals ; lit_no++ ) 
		    literals[lit_no].value = literalAssignment[lit_no];
	}
	

 	for ( flip = 1 ; flip <= max_flips ; flip++) {

	// HEURISTIC-1    
	/* If current setting of T/F satisfies given set of clauses,
	*  unSatClauseNum takes value -1, otherwise it takes the
	   value of an unsatisfied clause number.*/
	unSatClauseNum = allClausesSatisfied();
	if ( unSatClauseNum == -1 ) {
	        *flipNum = flip;
		*retryNum = try;
		return SUCCESS;
	}
	/* Select a clause randomly from clauses that is false */
	clause_num = unSatClauseNum; 
		  
	/* With prob prob_rand_walk, flip the value in a randomly
	* selected literal in clause_num
	*/

	r = fabs( (double)rand() / (double)(RAND_MAX) ); // r in [0,1]
	if ( r < prob_rand_walk ) {
		lit_num_in_clause = 1+(int) (((float)maxLiteralsPerClause)*rand() /(RAND_MAX+1.0));
		lit_number = abs(clauses[clause_num-1].literals[lit_num_in_clause-1]); 


		// Flipping ...
		if ( literals[lit_number-1].value  > 0  ) // TRUE
			literals[lit_number-1].value = -lit_number; 
		else
			literals[lit_number-1].value = lit_number; 
	}
        else{ // else flip the literal satisfying max clauses after flipping
		flipMaxClauseSatisfyingLiteral(clause_num);
	}

         } // flip ..
    } // try ..

    /* Not satisfied after max_tries also !!! return Failure */
    *flipNum = flip;
    *retryNum = try;
    return FAILURE;
}

int allClausesSatisfied(void)
{
	int cl,lit,this_clause;
	int litNumber; // stores the current literal 
	int litSign; // is the literal in its current assignment state or flipped sign state ?
	int truthValueOfLiteral;

	// A current assignment of literals exists
    	// Check each clause
      
    	for ( cl = 0 ; cl < numberOfClauses ; cl++ ) {
	    this_clause = FALSE;
	    for ( lit = 0 ; lit < clauses[cl].literalCount ; lit++ ) {
		litNumber = abs(clauses[cl].literals[lit]);
		litSign  = (int)(clauses[cl].literals[lit]/(abs(clauses[cl].literals[lit])));
		truthValueOfLiteral = literals[litNumber-1].value;  
		if ( (litSign * truthValueOfLiteral)  > 0 ) { // TRUE
		    this_clause = TRUE;
		    break;
		}
	    } // lit ..
	    if ( this_clause == FALSE ) { // none of the literals were true
		return (cl+1);
	    }
	}
	return -1;
}



/*  Flips the literal in the specified clause which causes the 
 *  maximum increase in the number of satisfied clauses 
 */
void flipMaxClauseSatisfyingLiteral(int clause_num)
{
    int clauseArrayIndex = clause_num - 1;
    int litSatisfyingMaxClauses;
    int maxCountSoFar, currCount ;
    int lit_number,lit,old_value_of_literal;
    int satIncreased;

    maxCountSoFar = numOfClausesSatisfied(); 

    // flip each literal in the specified literal and see what
    // its effect on number of clauses satisfied is

    satIncreased = FALSE;
    for ( lit = 0 ; lit < clauses[clauseArrayIndex].literalCount ; lit++) {

	 lit_number = abs(clauses[clauseArrayIndex].literals[lit]);
	 old_value_of_literal = literals[lit_number-1].value; 

	 // Flip this literal
	if ( literals[lit_number-1].value  > 0  ) // TRUE
		literals[lit_number-1].value = -lit_number; 
	else
		literals[lit_number-1].value = lit_number; 

	// Count the number of clauses satisfied by this flipped literal
	currCount = numOfClausesSatisfied();

	if ( currCount >= maxCountSoFar ) { // Flipping increased number of satisfied clauses
	    satIncreased = TRUE;
	    maxCountSoFar = currCount;
	    litSatisfyingMaxClauses = lit_number;
	}

	// revert to old value
        literals[lit_number-1].value = old_value_of_literal;
    } // lit ..
   
    if ( satIncreased == TRUE ) {
     // litSatisfyingMaxClauses is the literal whose flip
     // causes max number of clauses to be satisfied
     // so actually flip it now
     
      if ( literals[litSatisfyingMaxClauses-1].value  > 0  ) // TRUE
		literals[litSatisfyingMaxClauses-1].value = -litSatisfyingMaxClauses; 
      else
		literals[litSatisfyingMaxClauses-1].value = litSatisfyingMaxClauses;
    }

}

/* Specifies the number of clauses satisfied by current assignment
   of literals 
*/
int numOfClausesSatisfied(void)
{
	int cl,lit,this_clause;
	int true_clause_count = 0;
	int litNumber; // stores the current literal 
	int litSign; // is the literal in its current assignment state or flipped sign state ?
	int truthValueOfLiteral;
	// A current assignment of literals exists
    	// Check each clause

	for ( cl = 0 ; cl < numberOfClauses ; cl++ ) {
	    this_clause = FALSE;
	    for ( lit = 0 ; lit < clauses[cl].literalCount ; lit++ ) {
		litNumber = abs(clauses[cl].literals[lit]);
		litSign  = (int)(clauses[cl].literals[lit]/(abs(clauses[cl].literals[lit])));
		truthValueOfLiteral = literals[litNumber-1].value;  
		if ( (litSign * truthValueOfLiteral)  > 0 ) { // TRUE
		    this_clause = TRUE;
		    true_clause_count++;
		    break;
		}
	    } // lit ..
	} // cl ..
	return true_clause_count;
}

int IsTrueClause(int cl_num)
{

	int litNumber; // stores the current literal 
	int litSign; // is the literal in its current assignment state or flipped sign state ?
	int truthValueOfLiteral;
	int lit;

	for ( lit = 0 ; lit < clauses[cl_num-1].literalCount ; lit++ ) {
		litNumber = abs(clauses[cl_num-1].literals[lit]);
		litSign  = (int)(clauses[cl_num-1].literals[lit]/(abs(clauses[cl_num-1].literals[lit])));
		truthValueOfLiteral = literals[litNumber-1].value;  
		if ( (litSign * truthValueOfLiteral)  > 0 ) { // TRUE
			return SUCCESS;
		}
	} // lit ..
	return FAILURE;
}

void printLiterals(void)
{
    int i;
    for( i = 0 ; i < numberOfLiterals ; i++)
	printf("[%d] ",literals[i].value);
    printf("\n");
}

/*
LITERAL getLiteralFromClause(int clause_num,int lit_num_in_clause)
{
	int arrayIndex = clause_num - 1;
	int lit_in_clause_index = lit_num_in_clause-1;
	int lit_number, litArrayIndex;

	lit_number = abs(clauses[arrayIndex].literals[lit_in_clause_index]);
	litArrayIndex = lit_number - 1;

	return literals[litArrayIndex];
}
*/