#include "WalkSatRestart.h"
#include "Clause.h"
#include "rand.h"
#include <stdio.h>

// Solve the given formula using WalkSAT
Assignment* WalkSatRestart::Solve( Formula* f )
{
    // Create the assignment
    Assignment* assign = new Assignment( f->NumVariables() );
    assign->SetValid( false );

    for( int j=0; j<=this->iMaxRestarts; j++ )
    {

        // Make Random Assignment to Variables
        for( int i=0; i<assign->NumVariables(); i++ )
            assign->SetValue( i, my_brand() );

        // Main Solving Loop
        for( int i=0; i<this->iMaxFlips; i++ )
        {
            // Check if the model is satisfied
            if( f->IsSatisfiedBy( assign ) )
            {
                assign->SetValid( true );
                return assign;
            }

            // Choose a clause at random (from the unsatisifed clauses
            Clause* random_clause = f->GetRandomUnsatisfiedClause( assign );

            // Decide whether to flip at random or with a purpose
            if( my_frand() <= this->fProbability )
            {
                // Flip random variable in clause
                // Choose a random variable
                int random_variable = my_rand( 0, random_clause->NumVariables()-1 );
                int vnum = (random_clause->GetValue( random_variable ))->var_num;

                // Flip that variables value
                assign->SetValue( vnum, !assign->GetValue( vnum ) );
            }
            else
            {
                // Flip variable that maximizes num of satisifed clauses
                int max_variable = -1;
                int max_sat = -1;

                // Find the variable whose flip will satisfy the most clauses
                for( int i=0; i<assign->NumVariables(); i++ )
                {
                    // Flip the variable
                    assign->SetValue( i, !assign->GetValue( i ) );

                    // Get Number of satisfied clauses
                    int num_sat = f->NumSatisfiedBy( assign );
                
                    // Check if this is the most satisied so far
                    if( num_sat > max_sat )
                    {
                        max_sat = num_sat;
                        max_variable = i;
                    }

                    // Flip the variable back
                    assign->SetValue( i, !assign->GetValue( i ) );
                }

                // Flip the max sat variables value
                if( max_variable >= 0 && max_sat >= 0 )
                    assign->SetValue( max_variable, !assign->GetValue( max_variable ) );
                // else ERROR
            }
        }
    }

    // Failure
    assign->SetValid( false );
    return assign;
}