#include <stdio.h>
#include <assert.h>
#include <stdlib.h>
#include <time.h>
#include "hybrid.h"

int num_vars_;
int num_clauses_;
int clause_length_;
int num_flips_;
float flip_prob_;

static char *clause_values_;
char *temp_assign;

int main(int argc, char *argv[])
{
	int i, j;
	char **clauses;
	char bracket;
	char *assignment, ret_value;

	if(argc!=3) 
	{
		printf("usage: ./hybrid <num-flips> <flip-prob>\n");
		exit(0);
	}

	num_flips_=atoi(argv[1]);
	flip_prob_=atof(argv[2]);
	
	srand( (unsigned int)time(NULL) );
	scanf("%d", &num_vars_);
	scanf("%d", &num_clauses_);
	scanf("%d", &clause_length_);

	clauses = (char**)malloc(num_clauses_ * sizeof(char*));
	clause_values_ = (char*)malloc(num_clauses_ * sizeof(char));
	for (i = 0; i < num_clauses_; ++i)
		clauses[i] = (char*)malloc(num_vars_ * sizeof(char));
	assignment = (char*)malloc(num_vars_ * sizeof(char));
 	temp_assign = (char*)malloc(num_vars_ * sizeof(char));
	for (i = 0; i < num_vars_; ++i)
		assignment[i] = UNASSIGNED;

	for (i = 0; i < num_clauses_; ++i)
	{
		int var_index;
		clauses[i] = (char*)malloc(num_vars_ * sizeof(char));
		for (j = 0; j < num_vars_; ++j)
			clauses[i][j] = UNASSIGNED;
		scanf("%c", &bracket);
		scanf("%c", &bracket);
		for (j = 0; j < clause_length_; ++j)
		{
			scanf("%d", &var_index);
			if (var_index > 0)
				clauses[i][var_index - 1] = TRUE;
			else
			{
				var_index *= -1;
				clauses[i][var_index - 1] = FALSE;
			}
		}
		scanf("%c", &bracket);
		scanf("%c", &bracket);
	}

	ret_value = dpll(clauses, assignment);
	if (ret_value == TRUE)
	{
		for (i = 0; i < num_vars_; ++i)
		{
			if (assignment[i] == TRUE)
				printf(" %d", i + 1);
			else if (assignment[i] == FALSE)
				printf(" -%d", i + 1);
			else
				printf(" %d", i + 1);
		}
		printf("\n");
	}
	else
		printf("Unsatisfiable\n");

	return 0;
}

char dpll(char **clauses, char *assignment)
{
	int i;
	int min_index, var_index;
	char ret_value;
	
	if (check_if_all_clauses_true(clauses, assignment))
	{
		return TRUE;
	}

	if (check_if_any_clause_false(clauses, assignment))
	{
		return FALSE;
	}

	min_index = -1;
	while (1)
	{
		if ((var_index = find_pure_symbol(clauses, assignment, min_index)) != 0 )
		{
			extend(assignment, var_index);
			ret_value = dpll(clauses, assignment);
			if (ret_value == TRUE)
				return TRUE;
			unassign(assignment, var_index);
			return FALSE;
			min_index = var_index > 0 ? var_index : -var_index;
			continue;
		}
		break;
	}

	min_index = -1;
	while (1)
	{
		if ((var_index = find_unit_clause(clauses, assignment, min_index)) != 0)
		{
			extend(assignment, var_index);
			ret_value = dpll(clauses, assignment);
			if (ret_value == TRUE)
				return TRUE;
			unassign(assignment, var_index);
			return FALSE;
			min_index = var_index > 0 ? var_index : -var_index;
			continue;
		}
		break;
	}

	var_index = pick_unassigned_symbol_intelligent(clauses, assignment);
	extend(assignment, var_index);
	ret_value = dpll(clauses, assignment);
	if (ret_value == TRUE)
		return TRUE;
	unassign(assignment, var_index);

	var_index *= -1;
	extend(assignment, var_index);
	ret_value = dpll(clauses, assignment);
	if (ret_value == TRUE)
		return TRUE;
	unassign(assignment, var_index);
	return FALSE;
}

int pick_unassigned_symbol(char **clauses, char *assignment)
{
	int i;

	for (i = 0; i < num_vars_; ++i)
	{
		if (assignment[i] == UNASSIGNED)
			return (i + 1);
	}

	return 0;
}

int check_if_all_clauses_true(char **clauses, char *assignment)
{
	int i, j;

	for (i = 0; i < num_clauses_; ++i)
	{
		for (j = 0; j < num_vars_; ++j)
		{
			if (clauses[i][j] != 0 && ((clauses[i][j] ^ assignment[j]) == 0))
				break;
		}
		if (j == num_vars_)
			return 0;
	}

	return 1;
}

int check_if_any_clause_false(char **clauses, char *assignment)
{
	int i, j;

	for (i = 0; i < num_clauses_; ++i)
	{
		for (j = 0; j < num_vars_; ++j)
		{
			if (clauses[i][j] != 0 && (((clauses[i][j] ^ assignment[j]) == 0) || (assignment[j] == UNASSIGNED)))
				break;
		}
		if (j == num_vars_)
		{
			return 1;
		}
	}

	return 0;
}

int find_pure_symbol(char **clauses, char *assignment, int min_index)
{
	int i, j;
	char prev_value;

	for (i = 0; i < num_clauses_; ++i)
	{
		clause_values_[i] = FALSE;
		for (j = 0; j < num_vars_; ++j)
		{
			if (clauses[i][j] != 0 && ((clauses[i][j] ^ assignment[j]) == 0))
			{
				clause_values_[i] = TRUE;
				break;
			}
		}
	}
	for (j = min_index + 1; j < num_vars_; ++j)
	{
		if (assignment[j] != 0)
			continue;
		prev_value = UNASSIGNED;
		for (i = 0; i < num_clauses_; ++i)
		{
			if (clause_values_[i] == FALSE && clauses[i][j] != 0)
			{
				if (prev_value == UNASSIGNED)
					prev_value = clauses[i][j];
				else if (clauses[i][j] != prev_value)
					break;
			}
		}
		if (i == num_clauses_)
		{
			if (prev_value == TRUE)
				return (j + 1);
			else if (prev_value == FALSE)
				return -(j + 1);
		}
	}

	return 0;
}

int find_unit_clause(char **clauses, char *assignment, int min_index)
{
	int i, j, index;
	char value;
	
	for (i = 0; i < num_clauses_; ++i)
	{
		value = FALSE;
		for (j = 0; j < num_vars_; ++j)
		{
			if (clauses[i][j] != 0)
			{
				if ((clauses[i][j] ^ assignment[j]) == 0)
					break;
				else if (assignment[j] == UNASSIGNED)
				{
					if (value == TRUE)
						break;
					else
					{
						index = (j + 1) * clauses[i][j];
						value = TRUE;
					}
				}
			}
		}
		if (j == num_vars_ && value == TRUE && index > min_index)
			return index;
	}

	return 0;
}

// Returns a random boolean value
int my_brand()
{
    if (rand() > RAND_MAX/2) 
	return 1;
    else
	return -1;
}

// Returns a random integer value between min and max inclusively
int my_rand( int min, int max )
{
    return ( (rand() / (RAND_MAX/((max-min)+1))) + min );
}

// Returns a random floating point number
float my_frand()
{
    return ( ((float)rand())/RAND_MAX );
}

int isSatisfiedBy(char **clauses,int clausenum, char *assignment)
{
 int j;
 for (j=0;j< num_vars_;j++)
	if(clauses[clausenum][j] !=0 && ((clauses[clausenum][j] ^ assignment[j]) == 0))
		break;
 if(j!=num_vars_)
	return 1;
 else return 0;
}

int hasFreeVariable(char **clauses,int clausenum, char *assignment)
{
 int j;
 for (j=0;j< num_vars_;j++)
	if(clauses[clausenum][j] !=0 && (assignment[j] == 0))
		return 1;
  return 0;
}

int NumSatisfiedBy(char **clauses, char * assignment)
{
	int count = 0;
	int i;

	for(i=0;i<num_clauses_;i++)
		if (isSatisfiedBy(clauses, i,assignment))
			count++;
	return count;
}

int walksat(char **clauses, char *assignment)
{
 int i,j,k;
 int random_clause_num;
 int random_variable;
 int max_variable  = -1;
 int max_sat = -1; 
 int num_sat = -1;
 int potential[1000];
 int num_potential;

 for (i = 0; i < num_vars_; ++i)
	if(assignment[i]==UNASSIGNED)
		temp_assign[i] = my_brand();
 	else
		temp_assign[i] = assignment[i];

 for(j=0;j<num_flips_;j++)
 {
	max_variable = -1;
 	max_sat = -1; 
 	num_sat = -1;

	 if(NumSatisfiedBy(clauses, temp_assign)==num_clauses_) {
		for (k = 0; k < num_vars_; ++k)
		{
			if (temp_assign[k] == TRUE)
				printf(" %d", k + 1);
			else if (temp_assign[k] == FALSE)
				printf(" -%d", k + 1);
			else
				printf(" %d", k + 1);
		}
		printf("\n");
		exit(0);
		 return num_clauses_;
	 }
	
 	num_potential=0;
	for(k=0;k< num_clauses_;k++)
		if(!isSatisfiedBy(clauses, k, temp_assign) && hasFreeVariable(clauses, k, assignment))
			potential[num_potential++]=k;
		
	if(num_potential==0)
		return 0;
	
	random_clause_num = potential[my_rand( 0, num_potential-1)];

	if(my_frand() <= flip_prob_ )
	{
		num_potential=0;
		for(k=0; k<num_vars_;k++)
			if((clauses[random_clause_num][k] != UNASSIGNED) && (assignment[k]==UNASSIGNED))
				potential[num_potential++]=k;

		random_variable = potential[my_rand( 0, num_potential-1)];
		temp_assign[random_variable] *= -1;	
	}
	else
	{
		for(i=0;i<num_vars_;i++)
		{
			if(assignment[i]==UNASSIGNED)
			{
				temp_assign[i] *= -1;

				num_sat = NumSatisfiedBy(clauses, temp_assign);

				if(num_sat>max_sat)
				{
					max_sat = num_sat;
					max_variable = i;
				}
	
				temp_assign[i] *= -1;
			}
		}
		temp_assign[max_variable] *= -1;
	}
 }

 return NumSatisfiedBy(clauses, temp_assign);

}

int pick_unassigned_symbol_intelligent(char **clauses, char *assignment)
{
	int i;
	int max_clauses_num=-1;
	int max_clauses_index=-1;
	int ret_val, var_index;

	for (i = 0; i < num_vars_; ++i)
	{
		if (assignment[i] == UNASSIGNED)
		{
			var_index = i+1;
			extend(assignment, var_index);
			ret_val = walksat(clauses, assignment);
			if(ret_val>max_clauses_num) 
			{
				max_clauses_num = ret_val;
				max_clauses_index = i;
			}
			unassign(assignment, var_index);
			
			var_index *= -1;
			extend(assignment, var_index);
			ret_val = walksat(clauses, assignment);
			if(ret_val>max_clauses_num) 
			{
				max_clauses_num = ret_val;
				max_clauses_index = i;
			}
			unassign(assignment, var_index);
			
		}
	}

	return (max_clauses_index+1);
}