/****************************************************

											small-Satz
				written by Peter G. Stock (... 1999)


										based on Satz
	originally written by Chu Min Li (September 1996)

****************************************************/

#include <stdio.h>
#include <stdlib.h>
#include <time.h>
#include <sys/times.h>
#include <sys/types.h>
#include <limits.h>

typedef signed char s_char;
typedef unsigned char u_char;

#define TRUE 1
#define FALSE 0
#define NONE -1
#define LIVE 1
#define DEAD 0

#define WORD_LENGTH 50

/* the tables of variables and clauses are statically allocated. Modify the
	parameters tab_variable_size and tab_clause_size before compilation if necessary */
#define tab_variable_size	500
#define tab_clause_size 10000
#define multiple_tab_clause_size 10*tab_clause_size

/* macro definitions */
#define positive(literal) literal < NUM_VARS
#define negative(literal) literal >= NUM_VARS
#define get_var_from_lit(negative_literal) negative_literal-NUM_VARS
#define complement(lit1, lit2) ((lit1<lit2) ? lit2-lit1==NUM_VARS : lit1-lit2==NUM_VARS)
#define pop(stack) stack[--stack ## _fill_pointer]
#define push(item, stack) stack[stack ## _fill_pointer++] = item

#define satisfiable() CLAUSE_STACK_fill_pointer == NUM_CLAUSES


int *sat[tab_clause_size];

int *neg_in[tab_variable_size];
int *pos_in[tab_variable_size];

s_char clause_state[tab_clause_size];
s_char clause_length[tab_clause_size];

s_char var_state[tab_variable_size];
s_char var_current_value[tab_variable_size];
s_char var_rest_value[tab_variable_size];

u_char num_neg_clause_of_length2[tab_variable_size];
u_char num_neg_clause_of_length3[tab_variable_size];
u_char num_pos_clause_of_length2[tab_variable_size];
u_char num_pos_clause_of_length3[tab_variable_size];

int saved_clause_stack[tab_variable_size];
int saved_managedclause_stack[tab_variable_size];


int VARIABLE_STACK[tab_variable_size];
int VARIABLE_STACK_fill_pointer = 0;

int CLAUSE_STACK[tab_clause_size];
int CLAUSE_STACK_fill_pointer = 0;
int MANAGEDCLAUSE_STACK[multiple_tab_clause_size];
int MANAGEDCLAUSE_STACK_fill_pointer = 0;
int UNITCLAUSE_STACK[tab_clause_size];
int UNITCLAUSE_STACK_fill_pointer = 0;

int NUM_VARS;
int NUM_CLAUSES;
int INIT_NUM_CLAUSES;

long NUM_UNIT=0, NUM_PURE=0, NUM_BRANCH=0, NUM_BACK=0;


/*#define verbose*/
/*#define print_tree*/
void print_formula(void)
{
	int i, count;
	int var, lit, *lits;

	for (i=0; i<NUM_CLAUSES; i++)
	{
		if (clause_state[i]==LIVE)
		{
			count = 0;
			printf("  [");
			lits = sat[i];
			for (lit=*lits; lit!=NONE; lit=*(++lits))
			{
				if (positive(lit))
				{
					var = lit;
					if (var_state[var]==LIVE)
					{
						count++;
						printf("%d ", var+1);
					}
				}
				else
				{
					var = get_var_from_lit(lit);
					if (var_state[var]==LIVE)
					{
						count++;
						printf("-%d ", var+1);
					}
				}
			}
			printf("\b]");
			if (clause_length[i]!=count)
				printf("<%d>", clause_length[i]);
		}
	}
	printf("\n");
}

/* ---------------------------------------------------------------------------------- */


void remove_clauses(int *clauses)
/* called twice in backtrack, twice in unitclause_process,
	twice in simple_propagate, twice in examine, twice in examine1,
	three times in choose_and_instantiate_variable_in_clause */
{
	int clause;
	for(clause=*clauses; clause!=NONE; clause=*(++clauses))
	{
		if (clause_state[clause] == LIVE)
		{
			clause_state[clause] = DEAD;
			push(clause, CLAUSE_STACK);
		}
	}
}
/* ---------------------------------------------------------------------------------- */

void simple_manage_clauses(register int *clauses)
/* called twice in backtrack, once in examine, twice in examine1,
	once in choose_and_instantiate_variable_in_clause */
{
	int clause;
	for(clause=*clauses; clause!=NONE; clause=*(++clauses))
	{
		if (clause_state[clause] == LIVE)
		{
			switch (clause_length[clause])
			{
				case 2:
					clause_length[clause]--;
					push(clause, UNITCLAUSE_STACK);
					break;
				default:
					clause_length[clause]--;
					push(clause, MANAGEDCLAUSE_STACK);
			}
		}
	}
}
int manage_clauses(register int *clauses)
/* called twice in unitclause_process */
{
	int clause;
	for(clause=*clauses; clause!=NONE; clause=*(++clauses))
	{
		if (clause_state[clause] == LIVE)
		{
			switch (clause_length[clause])
			{
				case 1:
					return FALSE;
				case 2:
					clause_length[clause]--;
					push(clause, UNITCLAUSE_STACK);
					break;
				default:
					clause_length[clause]--;
					push(clause, MANAGEDCLAUSE_STACK);
			}
		}
	}
	return TRUE;
}
/* ---------------------------------------------------------------------------------- */


int backtrack(void)
/* called twice in unitclause_process */
{
	int var, index;
/**/	int val;

	UNITCLAUSE_STACK_fill_pointer = 0;
	NUM_BACK++;

	do
	{
		var = pop(VARIABLE_STACK);
		if (var_rest_value[var] == NONE)
			var_state[var] = LIVE;
		else
		{
			for (index = saved_clause_stack[var];
						index < CLAUSE_STACK_fill_pointer; index++)
				clause_state[CLAUSE_STACK[index]] = LIVE;
			CLAUSE_STACK_fill_pointer = saved_clause_stack[var];

			for (index = saved_managedclause_stack[var];
						index < MANAGEDCLAUSE_STACK_fill_pointer; index++)
				clause_length[MANAGEDCLAUSE_STACK[index]]++;
			MANAGEDCLAUSE_STACK_fill_pointer = saved_managedclause_stack[var];

			var_current_value[var] = var_rest_value[var];
			var_rest_value[var] = NONE;
			push(var, VARIABLE_STACK);
			if (var_current_value[var] == FALSE)
			{
				simple_manage_clauses(pos_in[var]);
				remove_clauses(neg_in[var]);
			}
			else
			{
				simple_manage_clauses(neg_in[var]);
				remove_clauses(pos_in[var]);
			}
/***/
#ifdef verbose
	if (var_current_value[var]==TRUE)
		val = 'T';
	else
		val = 'F';
	printf("Backtrack branch: %d -> %c\n", var+1, val);
#ifdef print_tree
	print_formula();
#endif
#endif
/***/
			return TRUE;
		}
	}
	while (VARIABLE_STACK_fill_pointer != 0);
	return FALSE;
}


void unitclause_process(void)
/* called three times in choose_and_instantiate_variable_in_clause, once in main */
{
	int var, i, unitclause, lit, *lits, unitclause_position;

	for (unitclause_position = 0;
				unitclause_position < UNITCLAUSE_STACK_fill_pointer;
				unitclause_position++)
	{
		unitclause = UNITCLAUSE_STACK[unitclause_position];
		/* does the clause legth of unit clauses actually need to be decremented
			in manage_clauses() and then incremented here?
			- not if the lookahead/heuristic only runs
				when the unitcluause stack is empty */
		clause_length[unitclause]++;
		if (clause_state[unitclause] == LIVE)
		{
			NUM_UNIT++;
			lits = sat[unitclause];
			for(lit=*lits; lit!=NONE; lit=*(++lits))
			{
				if (positive(lit))
				{
					var = lit;
					if (var_state[var] == LIVE)
					{
						var_current_value[var] = TRUE;
						var_rest_value[var] = NONE;
						if (manage_clauses(neg_in[var]) == TRUE)
						{
							var_state[var] = DEAD;
							push(var, VARIABLE_STACK);
							remove_clauses(pos_in[var]);
/***/
#ifdef verbose
	printf("Unit: %d -> %c\n", var+1, 'T');
#ifdef print_tree
	print_formula();
#endif
#endif
/***/
							break;
						}
						else
						{
							for (i=unitclause_position+1; i<UNITCLAUSE_STACK_fill_pointer; i++)
								clause_length[UNITCLAUSE_STACK[i]]++;
/***/
#ifdef verbose
	printf("Failed Unit: %d -> %c\n", var+1, 'T');
#endif
/***/
							backtrack();
							return;
						}
					}
				}
				else
				{
					var = get_var_from_lit(lit);
					if (var_state[var] == LIVE)
					{
						var_current_value[var] = FALSE;
						var_rest_value[var] = NONE;
						if (manage_clauses(pos_in[var]) == TRUE)
						{
							var_state[var] = DEAD;
							push(var, VARIABLE_STACK);
							remove_clauses(neg_in[var]);
/***/
#ifdef verbose
	printf("Unit: %d -> %c\n", var+1, 'F');
#ifdef print_tree
	print_formula();
#endif
#endif
/***/
							break;
						}
						else
						{
							for (i=unitclause_position+1; i<UNITCLAUSE_STACK_fill_pointer; i++)
								clause_length[UNITCLAUSE_STACK[i]]++;
/***/
#ifdef verbose
	printf("Failed Unit: %d -> %c\n", var+1, 'F');
#endif
/***/
							backtrack();
							return;
						}
					}
				}
			}
		}
	}
	UNITCLAUSE_STACK_fill_pointer = 0;
}
/* ---------------------------------------------------------------------------------- */
/* ---------------------------------------------------------------------------------- */



int get_pos_clause_num(int var)
/* called once in choose_and_instantiate_variable_in_clause */
{
	s_char pos_clause3_num = 0, pos_clause2_num = 0;
	int *clauses, clause;

	clauses = pos_in[var];
	for(clause=*clauses; clause!=NONE; clause=*(++clauses))
	{
		if (clause_state[clause] == LIVE)
		{
			if (clause_length[clause] == 2)
				pos_clause2_num++;
			else
				pos_clause3_num++;
		}
	}
	num_pos_clause_of_length2[var] = pos_clause2_num;
	num_pos_clause_of_length3[var] = pos_clause3_num;
	return pos_clause2_num + pos_clause3_num;
}

int get_neg_clause_num(int var)
/* called once in choose_and_instantiate_variable_in_clause */
{
	s_char neg_clause3_num = 0, neg_clause2_num = 0;
	int *clauses, clause;

	clauses = neg_in[var];
	for(clause=*clauses; clause!=NONE; clause=*(++clauses))
	{
		if (clause_state[clause] == LIVE)
		{
			if (clause_length[clause] == 2)
				neg_clause2_num++;
			else
				neg_clause3_num++;
		}
	}
	num_neg_clause_of_length2[var] = neg_clause2_num;
	num_neg_clause_of_length3[var] = neg_clause3_num;
	return neg_clause2_num + neg_clause3_num;
}
/* ---------------------------------------------------------------------------------- */


void choose_and_instantiate_variable_in_clause(void)
/* called once in main */
{
	int var, chosen_var = NONE;
	int current_min = -1;
	s_char pos2, neg2, min;
/**/	int val;

	NUM_BRANCH++;

	for (var=0; var<NUM_VARS; var++)
	{
		if (var_state[var] == LIVE)
		{
			if (get_neg_clause_num(var) == 0)
			{
				NUM_PURE++;
				var_current_value[var] = TRUE;
				var_rest_value[var] = NONE;
				var_state[var] = DEAD;
				push(var, VARIABLE_STACK);
				remove_clauses(pos_in[var]);
/***/
#ifdef verbose
	printf("Pure: %d -> %c\n", var+1, 'T');
#ifdef print_tree
	print_formula();
#endif
#endif
/***/
			}
			else
			if (get_pos_clause_num(var) == 0)
			{
				NUM_PURE++;
				var_current_value[var] = FALSE;
				var_rest_value[var] = NONE;
				var_state[var] = DEAD;
				push(var, VARIABLE_STACK);
				remove_clauses(neg_in[var]);
/***/
#ifdef verbose
	printf("Pure: %d -> %c\n", var+1, 'F');
#ifdef print_tree
	print_formula();
#endif
#endif
/***/
			}
		}
	}

	/* maximise min(f(v),f(~v)) */
	for (var=0; var<NUM_VARS; var++)
	{
		if (var_state[var] == LIVE)
		{
			pos2 = num_pos_clause_of_length2[var];
			neg2 = num_neg_clause_of_length2[var];
			if (pos2 < neg2)
				min = pos2;
			else
				min = neg2;

			if (min > current_min)
				chosen_var = var;
		}
	}

	if (chosen_var == NONE)
		/* can this ever happen? */
		return;

	var_state[chosen_var] = DEAD;
	saved_clause_stack[chosen_var] = CLAUSE_STACK_fill_pointer;
	saved_managedclause_stack[chosen_var] = MANAGEDCLAUSE_STACK_fill_pointer;
	push(chosen_var, VARIABLE_STACK);
	var_current_value[chosen_var] = TRUE;
	var_rest_value[chosen_var] = FALSE;
	simple_manage_clauses(neg_in[chosen_var]);
	remove_clauses(pos_in[chosen_var]);
/***/
#ifdef verbose
	if (var_current_value[chosen_var]==TRUE)
		val = 'T';
	else
		val = 'F';
	printf("Branch: %d -> %c\n", chosen_var+1, val);
#ifdef print_tree
	print_formula();
#endif
#endif
/***/
}
/* ---------------------------------------------------------------------------------- */
/* ---------------------------------------------------------------------------------- */
/* ---------------------------------------------------------------------------------- */


s_char build_simple_sat_instance(char *input_file)
/* called twice in build */
{
	FILE* fp_in = fopen(input_file, "r");
	char ch, word[WORD_LENGTH];
	u_char neg_num[tab_variable_size], pos_num[tab_variable_size];
	int i, j, length,
			lits[tab_variable_size], *lits1, lit, var;

	if (fp_in == NULL) return FALSE;

	fscanf(fp_in, "%c", &ch);
	while (ch != 'p')
	{
		while (ch != '\n')
			fscanf(fp_in, "%c", &ch);
		fscanf(fp_in, "%c", &ch);
	}

	fscanf(fp_in, "%s%d%d", word, &NUM_VARS, &NUM_CLAUSES);
	INIT_NUM_CLAUSES = NUM_CLAUSES;

	for (i=0; i<NUM_VARS; i++)
	{
		num_neg_clause_of_length3[i] = 0;
		num_pos_clause_of_length3[i] = 0;
		num_neg_clause_of_length2[i] = 0;
		num_pos_clause_of_length2[i] = 0;
		neg_num[i] = 0;
		pos_num[i] = 0;
	}
	for (i=0; i<NUM_CLAUSES; i++)
	{
		length = 0;
		fscanf(fp_in, "%d", &lits[length]);
		while (lits[length] != 0)
		{
			length++;
			fscanf(fp_in, "%d", &lits[length]);
		}
		sat[i] = (int *) malloc((length+1)*sizeof(int));
		for (j=0; j<length; j++)
		{
			if (lits[j] < 0)
			{
				var = abs(lits[j]) - 1;
				sat[i][j] = var + NUM_VARS;
				neg_num[var]++;

				if (length==3)
					num_neg_clause_of_length3[var]++;
				else
				if (length==2)
					num_neg_clause_of_length2[var]++;
				else
				if (length==1)
					push(i, UNITCLAUSE_STACK);
			}
			else
			{
				var = lits[j] - 1;
				sat[i][j] = var;
				pos_num[var]++;

				if (length==3)
					num_pos_clause_of_length3[var]++;
				else
				if (length==2)
					num_pos_clause_of_length2[var]++;
				else
				if (length==1)
					push(i, UNITCLAUSE_STACK);
			}
		}
		sat[i][length] = NONE;
		clause_length[i] = length;
		clause_state[i] = LIVE;
	}
	fclose(fp_in);

	for (i=0; i<NUM_VARS; i++)
	{
		neg_in[i] = (int *) malloc((neg_num[i]+1)*sizeof(int));
		pos_in[i] = (int *) malloc((pos_num[i]+1)*sizeof(int));
		neg_in[i][neg_num[i]] = NONE;
		pos_in[i][pos_num[i]] = NONE;
		neg_num[i] = 0;
		pos_num[i] = 0;
		var_state[i] = LIVE;
	}
	for (i=0; i<NUM_CLAUSES; i++)
	{
		lits1 = sat[i];
		for(lit=*lits1; lit!=NONE; lit=*(++lits1))
		{
			if (positive(lit))
				pos_in[lit][pos_num[lit]++] = i;
			else
				neg_in[get_var_from_lit(lit)][neg_num[get_var_from_lit(lit)]++] = i;
		}
	}
	return TRUE;
}


/* ---------------------------------------------------------------------------------- */
/* ---------------------------------------------------------------------------------- */


int verify_solution(void)
/* called once in main */
{
	int i, lit, *lits, clause_truth;

	for (i=0; i<NUM_CLAUSES; i++)
	{
		clause_truth = FALSE;
		lits = sat[i];
		for(lit=*lits; lit!=NONE; lit=*(++lits))
			if (((negative(lit)) && (var_current_value[get_var_from_lit(lit)] == FALSE)) ||
					((positive(lit)) && (var_current_value[lit] == TRUE)) )
			{
				clause_truth = TRUE;
				break;
			}
		if (clause_truth == FALSE)
			return FALSE;
	}

	return TRUE;
}

void print_values(int NUM_VARS)
/* called once in main */
{
	int i;

	for (i=0; i<NUM_VARS; i++)
	{
		if (var_current_value[i] == 1)
			printf("%6d\t", i+1);
		else
			printf("%6d\t", -i-1);

		if ((i+1)%10 == 0)
			printf("\n");
	}
	printf("\n");
}
/* ---------------------------------------------------------------------------------- */

void main(int argc, char *argv[])
{
	char saved_input_file[WORD_LENGTH];
	clock_t begintime, endtime;
	int i;
	struct tms *a_tms;

	if (argc < 2)
	{
		printf("Usage:\tsatz-small input_file\n");
		return;
	}
	for (i=0; i<WORD_LENGTH; i++)
		saved_input_file[i] = argv[1][i];

	a_tms = (struct tms *) malloc(sizeof(struct tms));


	times(a_tms);
	begintime = a_tms->tms_utime;

	switch (build_simple_sat_instance(argv[1]))
	{
		case FALSE:
			printf("Input file error\n");
			return;
		case TRUE:
/***/
#ifdef verbose
	print_formula();
#endif
/***/
			do
			{
				if (UNITCLAUSE_STACK_fill_pointer == 0)
					choose_and_instantiate_variable_in_clause();
				unitclause_process();
			} while ((VARIABLE_STACK_fill_pointer != 0) && (!(satisfiable())));
			break;
		case NONE:
			printf("An empty resolvant is found!\n");
			break;
	}

	times(a_tms);
	endtime = a_tms->tms_utime;


	if (satisfiable())
	{
		printf ("**** the instance is satisfiable ****\n");
		if (verify_solution())
		{
			printf ("**** verification of solution is OK ****\n");
			print_values(NUM_VARS);
		}
		else
			printf ("**** program error - verification failed ****\n");
	}
	else
		printf ("**** the instance is unsatisfiable ****\n");

	printf("NUM_UNIT= %ld, NUM_PURE= %ld, NUM_BRANCH= %ld, NUM_BACK= %ld \n",
			NUM_UNIT, NUM_PURE, NUM_BRANCH, NUM_BACK);

	printf ("Program terminated in %5.3f seconds.\n",
			((double)(endtime-begintime)/CLK_TCK));

	printf("satz %s  %5.3f  %ld  %ld  %d  %d  %d  %d\n",
			saved_input_file, ((double)(endtime-begintime)/CLK_TCK),
			NUM_BRANCH, NUM_BACK,
			satisfiable(), NUM_VARS, INIT_NUM_CLAUSES, NUM_CLAUSES-INIT_NUM_CLAUSES);
}