#include <stdlib.h>
#include <stdio.h>
#include <process.h>
#include <math.h>
#include <time.h>
#include <string.h>


#define 	DEBUG

#define		VAR(t)		(( (t)-(t)%2 ) / 2 )
#define		NEG(t)		((t)%2==0 ? ' ' : '~')
#define		TERMO(v,d)	(2*(v)+(d))


int num_var;		/* Numero de variaveis no problema */
int num_claus;		/* Numero de clausulas no problema */
int num_term;		/* Numero de termos por clausula */




int **clausulas;	/* Vetor apontando para cada uma das clausulas */
					/* 2*x indica variavel, +1 indica negado */

int *aparece;		/* Indica quantas vezes cada termo aparece */

int **satisfaz;		/* Indica quais clausulas sao satisfeitas por cada termo */
int *next;

int *solucao;		/* Solucao ateh o momento, valor de cada variavel */

int *feitas;		/* Indica quantas vezes cada clausula foi satisfeita */

int *niveis;		/* Indica ateh qual clausula vai a capacidade do nivel */




void cria_clausula( int n, int t, int *termos)
{
	int i, j, aux;

	for( i=0; i<t; ++i)
	 {
		termos[i] = 2 * random( n );

		for( j=0; j<i; ++j)
			if( termos[i] == termos[j] )
				break;

		if( j != i )	--i;
		}

	for( i=0; i<t; ++i)
	 {
		if( random(1000) >= 500 )
			++termos[i];    /* variavel aparece negada */
		}


	for( i=0; i<t-1; ++i)
		for( j=i+1; j<t; ++j)
			if( termos[i] > termos[j] )
			 {
				aux = termos[i];
				termos[i] = termos[j];
				termos[j] = aux;
				}

}



int calcula( void)
{
	int nivel_atual, i, j;
	int termo;
	int *ptr;
	int quantos;


	nivel_atual = 0;

	while( nivel_atual >= 0  &&  nivel_atual < num_var )
	 {


#ifdef DEBUG

	printf("\n!!!!!!!! Solucao\n");
	for( i=0; i< num_var; ++i)
		printf("(%d)=%d ",i,solucao[i]);
	printf("\nFeitas\n");

	for( i=0; i< num_claus; ++i)
		printf("(%d)=%d ",i,feitas[i]);
	printf("\n\n");

	printf("!!!! inicio do loop !!!! Nivel_atual %d,", nivel_atual);
	printf("solucao atual neste nivel %d\n", solucao[nivel_atual] );

#endif


		if( solucao[nivel_atual] == 1 )
		 {
			/*** Backtrack ***/

#ifdef	DEBUG
	printf("Backtrack pois esgotou tentativas no nivel\n");
#endif

			--nivel_atual;

			if( nivel_atual == -1 )	continue;	/* sem solucao */


			termo = TERMO( nivel_atual, solucao[nivel_atual]);
			ptr = satisfaz[termo];
			quantos = aparece[termo];

			for( i=0; i<quantos; ++i)
				--feitas[*ptr++];
			}

		else
		 {
			/*** seleciona o branch ***/

#ifdef	DEBUG
	printf("Seleciona novo branch\n");
#endif

			++solucao[nivel_atual];

			termo = TERMO( nivel_atual, solucao[nivel_atual]);
			ptr = satisfaz[termo];
			quantos = aparece[termo];

			for( i=0; i<quantos; ++i)
				++feitas[*ptr++];


			/*** Testa se este caminho eh inviavel ***/
			if( nivel_atual != 0 )
			 {
				for( i=niveis[nivel_atual-1]+1; i<=niveis[nivel_atual]; ++i)
					if( feitas[i] == 0 )
						break;

				if( i <= niveis[nivel_atual] ) /*** Caminho eh inviavel */
				 {
					for( j=0; j<quantos; ++j)
						--feitas[*--ptr];
#ifdef	DEBUG
	printf("Este branch gera um caminho inviavel\n");
#endif

					continue;
					}
				}

			/*** Caminho eh viavel, faz o bound */

#ifdef	DEBUG
	printf("Caminho eh viavel, faz o bound deste branch\n");
#endif
			++nivel_atual;
			solucao[nivel_atual] = -1;

			}



		}

	if( nivel_atual == num_var )
	 {
		return 1;

		}

	else if( nivel_atual == -1 )
			return 0;

		else
			return -1;



}


int confere( void)
{
int i, j;
int var, ter;

	for( i=0; i<num_claus; ++i)
	 {
		for( j=0; j<num_term; ++j)
		{
			var = VAR( clausulas[i][j] );
			ter = TERMO( var, solucao[var]);

			if( ter == clausulas[i][j] )
				break;
			}
		if( j == num_term )
			return 0;
		}

	return 1;
}



void main( int argc, char *argv[])
{
int i,j;
int *aux;
char opcao;
int resp;

time_t inicio, fim;


/*** Escolhe semente para randomizacao ***/
	randomize();



/*** Testa argumentos de execucao ***/

	if( argc != 3 )
		{	printf("satisfia <n> <opcao:n|p> \n");
			exit(1);
			}

	num_var = atoi( argv[1] );
	if( num_var < 3  ||  num_var > 250 )
		{	printf("Numero invalido de variaveis: %d\n", num_var);
			exit(1);
			}

	opcao = argv[2][0];
	if( opcao!='p'  &&  opcao != 'n' )
		{	printf("Opcao deve ser 'p' ou 'n'\n");
			exit(1);
			}


/*** Define tamanho do problema ***/

	num_term = 3;

	num_claus = (int) (4.25 * num_var);



/*** Cria cada uma das clausulas ***/

	clausulas = calloc( num_claus, sizeof(int *) );
	if( clausulas == NULL )
		{	printf("Erro na alocacao de memoria <clausulas>\n");
			exit(1);
			}


	for( i=0; i<num_claus; ++i)
	 {
		clausulas[i] = calloc( num_term, sizeof(int) );
		cria_clausula( num_var, num_term, clausulas[i]);
		}

	for( i=0; i<num_claus; ++i)
		if( clausulas[i] == NULL )
			{	printf("Erro na alocacao de memoria <clausulas[%d]>\n",i);
				exit(1);
				}


/*** Ordena as clausulas em funcao do ultimo termo ***/

	for( i=0; i<num_claus-1; ++i)
		for( j=i+1; j<num_claus; ++j)
			if( clausulas[i][num_term-1] > clausulas[j][num_term-1] )
			 {
				aux = clausulas[i];
				clausulas[i] = clausulas[j];
				clausulas[j] = aux;
				}

/*** Determina quantas vezes cada termo aparece ***/

	aparece = calloc( num_var * 2, sizeof(int) );
	if( aparece == NULL )
		{	printf("Erro na alocacao de memoria <aparece>\n");
			exit(1);
			}

	for( i=0; i<num_var * 2; ++i)
		aparece[i] = 0;

	for( i=0; i<num_claus; ++i)
		for( j=0; j<num_term; ++j)
			++aparece[ clausulas[i][j] ];


/*** Aloca memoria para a tabela satisfaz, e next para controlar insercao ***/

	satisfaz = calloc( num_var * 2, sizeof(int *) );
	if( satisfaz == NULL )
		{	printf("Erro na alocacao de memoria <satisfaz>\n");
			exit(1);
			}

	next = calloc( num_var * 2, sizeof(int) );
	if( next == NULL )
		{	printf("Erro na alocacao de memoria <next>\n");
			exit(1);
			}

	for( i=0; i < 2*num_var; ++i)
	 {
		satisfaz[i] = calloc( aparece[i], sizeof(int) );
		next[i] = 0;
		}
	for( i=0; i<2*num_var; ++i)
		if( satisfaz[i] == NULL &&  aparece[i] != 0 )
			{	printf("Erro na alocacao de memoria <satisfaz[%d]>\n",i);
				exit(1);
				}



/*** Completa a tabela satisfaz ***/

	for( i=0; i<num_claus; ++i)
		for( j=0; j<num_term; ++j)
		 {
			satisfaz[clausulas[i][j]][next[clausulas[i][j]]] = i;
			++next[clausulas[i][j]];
			}

/*** Aloca e inicializa vetor com a solucao ***/

	solucao = calloc( num_var, sizeof(int) );
	if(	solucao == NULL )
		{	printf("Erro na alocacao de memoria <solucao>\n");
			exit(1);
			}

	for( i=0; i<num_var; ++i)
		solucao[i] = -1;


/*** Aloca e inicializa vetor de feitas ***/

	feitas = calloc( num_claus, sizeof(int) );

	for( i=0; i<num_claus; ++i)
		feitas[i] = 0;

	if( feitas == NULL )
		{	printf("Erro na alocacao de memoria <feitas>\n");
			exit(1);
			}


/*** Aloca e inicializa vetor de niveis ***/

	niveis = calloc( num_var, sizeof(int) );
	if( niveis == NULL )
		{	printf("Erro na alocacao de memoria <niveis>\n");
			exit(1);
			}

	for( i=0; i<num_var; ++i)
		niveis[i] = -1;

	for( j=0; j<num_claus; ++j)
		niveis[ VAR(clausulas[j][num_term-1]) ] = j;

	for( i=1; i<num_var; ++i)
		if( niveis[i] == -1 )
			niveis[i] = niveis[i-1];



/*** Print de tudo para conferir ***/


	printf("Branch & Bound aplicado ao problema da Satisfiability\n");


	printf("Variaveis=%d, Clausulas=%d, Termos=%d\n\n",
												num_var,num_claus,num_term);


	/*** Imprime dados de entrada ***/

	if( opcao == 'p' )
	 {
		printf("Solucao ateh o momento:\n");
		for( i=0; i< num_var; ++i)
			printf("(%d)=%d ",i,solucao[i]);
		printf("\n");


		for( i=0; i<num_claus; ++i)
		 {
			for( j=0; j<num_term; ++j)
				printf(" %c %d + ", NEG(clausulas[i][j]),
													VAR(clausulas[i][j]) );
			printf(" }AND \n");
			}


		printf("Quantas vezes cada termo aparece:\n");
		for( i=0; i< 2*num_var; i+=2)
			printf("(%d)=%d (~%d)=%d ",VAR(i),aparece[i],VAR(i),aparece[i+1]);

		printf("\nIdem\n");
		for( i=0; i< 2*num_var; i+=2)
			printf("(%d)=%d (~%d)=%d ",VAR(i),next[i],VAR(i),next[i+1]);



		for( i=0; i<2*num_var; ++i)
		 {
			printf("\n (%c%d) = ", NEG(i), VAR(i) );
			for( j=0; j<aparece[i]; ++j)
				printf("%d ", satisfaz[i][j]);
			}


		printf("\nUltima clausula dependente deste nivel:\n");
		for( i=0; i< num_var; ++i)
			printf("(%d)=%d ",i,niveis[i]);

		}



/*** Calcula uma solucao para o problema ***/

	printf("\n... Calculando ...\n");

	time(&inicio);
	resp = calcula();
	time(&fim);

	if( resp == 1 )
	 {
		printf("FIM: encontrou solucao em %lf segundos:\n",
													difftime(fim,inicio) );

		for( i=0; i< num_var; ++i)
			printf("(%d)=%d ",i,solucao[i]);
		printf("\n");

		if( confere() )
			printf("Confere !\n");
		else
			printf("NAO CONFERE !\n");

		}

	else if( resp == 0 )
			printf("FIM: Nao existe solucao em %lf segundos\n",
													difftime(fim,inicio) );

		else
			printf("ERRO: Valor nao esperado\n");



	exit(0);
}