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

												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 DEAD 0
#define LIVE 1

#define WORD_LENGTH 50
#define WEIGHT 5
#define T 10
#define RESOLVANT_LENGTH 3
#define MAX_NODE_NUMBER 6000

/* test if the new clause is redundant or subsumed by another */
#define OLD_CLAUSE_REDUNDANT 77
#define NEW_CLAUSE_REDUNDANT 7

/* 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	5000
#define tab_clause_size 100000
#define multiple_tab_clause_size 2*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 smaller_than(lit1, lit2) \
	((lit1<NUM_VARS) ? lit1 : lit1-NUM_VARS) < ((lit2<NUM_VARS) ? lit2 : lit2-NUM_VARS)
/* used twice in redundant, three times in get_resolvant */

#define pop(stack) stack[--stack ## _fill_pointer]
#define push(item, stack) stack[stack ## _fill_pointer++] = item

#define satisfiable() CLAUSE_STACK_fill_pointer == NUM_CLAUSES



struct node {
	int clause;
	struct node *next;
};

struct resource {
	struct node *pnode;
	struct resource *next;
};

int CLAUSE_NODES_pointer = MAX_NODE_NUMBER;

struct node *CLAUSE_NODES;
struct resource *resources = NULL;

struct node *node_neg_in[tab_variable_size];
struct node *node_pos_in[tab_variable_size];


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 reduce_if_negative_num[tab_variable_size];
int reduce_if_positive_num[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 MY_VARIABLE_STACK[tab_variable_size];
int MY_VARIABLE_STACK_fill_pointer = 0;
int MY_MANAGEDCLAUSE_STACK[multiple_tab_clause_size];
int MY_MANAGEDCLAUSE_STACK_fill_pointer = 0;
int MY_UNITCLAUSE_STACK[tab_clause_size];
int MY_UNITCLAUSE_STACK_fill_pointer = 0;

int TESTED_VAR_STACK[tab_variable_size];
int TESTED_VAR_STACK_fill_pointer = 0;
int IMPLIED_LITS[tab_variable_size];
int IMPLIED_LITS_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, NUM_SEARCH=0, NUM_FIXED=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 backtracking, 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 backtracking, 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:
					push(clause, UNITCLAUSE_STACK);
					clause_length[clause]--;
					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:
					push(clause, UNITCLAUSE_STACK);
					clause_length[clause]--;
					break;
				default:
					clause_length[clause]--;
					push(clause, MANAGEDCLAUSE_STACK);
			}
		}
	}
	return TRUE;
}
void my_simple_manage_clauses(register int *clauses)
/* called twice in examine, twice in examine1 */
{
	int clause;
	for(clause=*clauses; clause!=NONE; clause=*(++clauses))
	{
		if (clause_state[clause] == LIVE)
		{
			switch (clause_length[clause])
			{
				case 2:
					push(clause, MY_UNITCLAUSE_STACK);
					clause_length[clause]--;
					break;
				default:
					clause_length[clause]--;
					push(clause, MY_MANAGEDCLAUSE_STACK);
			}
		}
	}
}
int my_manage_clauses(register int *clauses)
/* called twice in branch */
{
	int clause;
	for(clause=*clauses; clause!=NONE; clause=*(++clauses))
	{
		if (clause_state[clause] == LIVE)
		{
			switch (clause_length[clause])
			{
				case 1:
					return FALSE;
				case 2:
					push(clause, MY_UNITCLAUSE_STACK);
					clause_length[clause]--;
					break;
				default:
					clause_length[clause]--;
					push(clause, MY_MANAGEDCLAUSE_STACK);
			}
		}
	}
	return TRUE;
}
/* ---------------------------------------------------------------------------------- */


int backtracking(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];
		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
/***/
							backtracking();
							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
/***/
							backtracking();
							return;
						}
					}
				}
			}
		}
	}
	UNITCLAUSE_STACK_fill_pointer = 0;
}
/* ---------------------------------------------------------------------------------- */
/* ---------------------------------------------------------------------------------- */


void reset_context(void)
/* called three times in examine, four times in examine1 */
{
	int i;

	MY_UNITCLAUSE_STACK_fill_pointer = 0;

	for (i=0; i<MY_VARIABLE_STACK_fill_pointer; i++)
		var_state[MY_VARIABLE_STACK[i]] = LIVE;
	MY_VARIABLE_STACK_fill_pointer = 0;

	for (i=0; i<MY_MANAGEDCLAUSE_STACK_fill_pointer; i++)
		clause_length[MY_MANAGEDCLAUSE_STACK[i]]++;
	MY_MANAGEDCLAUSE_STACK_fill_pointer = 0;
}

int get_resolvant_num(int clause)
/* called twice in examine1 */
{
	int *lits;
	int lit, var, resolvant_num=0;

	lits = sat[clause];
	for(lit=*lits; lit!=NONE; lit=*(++lits))
	{
		if (positive(lit))
		{
			var = lit;
			if (var_state[var] == LIVE)
				resolvant_num += (num_neg_clause_of_length2[var] * WEIGHT) +
												num_neg_clause_of_length3[var];
		}
		else
		{
			var = get_var_from_lit(lit);
			if (var_state[var] == LIVE)
				resolvant_num += (num_pos_clause_of_length2[var] * WEIGHT) +
												num_pos_clause_of_length3[var];
		}
	}
	return resolvant_num;
}

void manage_clauses_for_propagate(register int *clauses)
/* called twice in simple_propagate */
{
	int clause;
	for(clause=*clauses; clause!=NONE; clause=*(++clauses))
	{
		if (clause_state[clause] == LIVE)
		{
			clause_length[clause]--;
			push(clause, MANAGEDCLAUSE_STACK);
		}
	}
}

void simple_propagate(int lit)
/* called once in examine */
{
	int var;
	if (positive(lit))
	{
		var = lit;
		var_current_value[var] = TRUE;
		manage_clauses_for_propagate(neg_in[var]);
		var_rest_value[var] = NONE;
		var_state[var] = DEAD;
		push(var, VARIABLE_STACK);
		remove_clauses(pos_in[var]);
	}
	else
	{
		var = get_var_from_lit(lit);
		var_current_value[var] = FALSE;
		manage_clauses_for_propagate(pos_in[var]);
		var_rest_value[var] = NONE;
		var_state[var] = DEAD;
		push(var, VARIABLE_STACK);
		remove_clauses(neg_in[var]);
	}
}


int branch(void)
/* called twice in examine, twice in examine1 */
{
	int var, lit, *lits, unitclause, unitclause_position, i;

	NUM_SEARCH++;

	for (unitclause_position=0;
				unitclause_position!=MY_UNITCLAUSE_STACK_fill_pointer;
				unitclause_position++)
	{
		unitclause = MY_UNITCLAUSE_STACK[unitclause_position];
		clause_length[unitclause]++;
		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;
					if (my_manage_clauses(neg_in[var]) == TRUE)
					{
						var_state[var] = DEAD;
						push(var, MY_VARIABLE_STACK);
						break;
					}
					else
					{
						for (i=unitclause_position+1; i<MY_UNITCLAUSE_STACK_fill_pointer; i++)
							clause_length[MY_UNITCLAUSE_STACK[i]]++;
						NUM_FIXED++;
						return NONE;
					}
				}
			}
			else
			{
				var = get_var_from_lit(lit);
				if (var_state[var] == LIVE)
				{
					var_current_value[var] = FALSE;
					if (my_manage_clauses(pos_in[var]) == TRUE)
					{
						var_state[var] = DEAD;
						push(var, MY_VARIABLE_STACK);
						break;
					}
					else
					{
						for (i=unitclause_position+1; i<MY_UNITCLAUSE_STACK_fill_pointer; i++)
							clause_length[MY_UNITCLAUSE_STACK[i]]++;
						NUM_FIXED++;
						return NONE;
					}
				}
			}

		}
	}
	return TRUE;
}
/* ---------------------------------------------------------------------------------- */


int examine(int tested_var)
/* called twice in choose_and_instantiate_variable_in_clause */
{
	int i, generating_fixed_variables_if_positive = 0,
			generating_fixed_variables_if_negative = 0,
			var, implied_lit;

	IMPLIED_LITS_fill_pointer = 0;

	var_current_value[tested_var] = TRUE;

	var_state[tested_var] = DEAD;
	push(tested_var, MY_VARIABLE_STACK);
	my_simple_manage_clauses(neg_in[tested_var]);

	generating_fixed_variables_if_positive = branch();
	reduce_if_positive_num[tested_var] = MY_MANAGEDCLAUSE_STACK_fill_pointer;

	if (generating_fixed_variables_if_positive == NONE)
	{
		reset_context();
		var_current_value[tested_var] = FALSE;
		var_rest_value[tested_var] = NONE;
		var_state[tested_var] = DEAD;
		push(tested_var, VARIABLE_STACK);
		simple_manage_clauses(pos_in[tested_var]);
		remove_clauses(neg_in[tested_var]);
		return NONE;
	}
	else
	{
		for (i=0; i<MY_VARIABLE_STACK_fill_pointer; i++)
		{
			var = MY_VARIABLE_STACK[i];
			if (var_current_value[var] == TRUE)
				implied_lit = var;
			else
				implied_lit = var + NUM_VARS;
			push(implied_lit, IMPLIED_LITS);
		}
		reset_context();
	}
	var_current_value[tested_var] = FALSE;

	var_state[tested_var] = DEAD;
	push(tested_var, MY_VARIABLE_STACK);
	my_simple_manage_clauses(pos_in[tested_var]);

	generating_fixed_variables_if_negative = branch();
	reduce_if_negative_num[tested_var] = MY_MANAGEDCLAUSE_STACK_fill_pointer;
	reset_context();

	if (generating_fixed_variables_if_negative == NONE)
	{
		for (i=0; i<IMPLIED_LITS_fill_pointer; i++)
			simple_propagate(IMPLIED_LITS[i]);
		return NONE;
	}
	push(tested_var, TESTED_VAR_STACK);
	return TRUE;
}


int examine1(int tested_var)
/* called once in choose_and_instantiate_variable_in_clause */
{
	int i, generating_fixed_variables_if_positive = 0,
			generating_fixed_variables_if_negative = 0,
			clause;

	var_current_value[tested_var] = TRUE;

	var_state[tested_var] = DEAD;
	push(tested_var, MY_VARIABLE_STACK);
	my_simple_manage_clauses(neg_in[tested_var]);

	generating_fixed_variables_if_positive = branch();

	if (generating_fixed_variables_if_positive == NONE)
	{
		reset_context();
		var_current_value[tested_var] = FALSE;
		var_rest_value[tested_var] = NONE;
		var_state[tested_var] = DEAD;
		push(tested_var, VARIABLE_STACK);
		simple_manage_clauses(pos_in[tested_var]);
		remove_clauses(neg_in[tested_var]);
		return NONE;
	}
	else
	{
		for (i=0; i<MY_MANAGEDCLAUSE_STACK_fill_pointer; i++)
		{
			clause = MY_MANAGEDCLAUSE_STACK[i];
			if (clause_length[clause] == 2)
				reduce_if_positive_num[tested_var] += get_resolvant_num(clause);
		}
		reset_context();
	}
	var_current_value[tested_var] = FALSE;

	var_state[tested_var] = DEAD;
	push(tested_var, MY_VARIABLE_STACK);
	my_simple_manage_clauses(pos_in[tested_var]);

	generating_fixed_variables_if_negative = branch();

	if (generating_fixed_variables_if_negative == NONE)
	{
		reset_context();
		simple_manage_clauses(neg_in[tested_var]);
		var_current_value[tested_var] = TRUE;
		var_rest_value[tested_var] = NONE;
		var_state[tested_var] = DEAD;
		push(tested_var, VARIABLE_STACK);
		remove_clauses(pos_in[tested_var]);
		return NONE;
	}
	else
	{
		for (i=0; i<MY_MANAGEDCLAUSE_STACK_fill_pointer; i++)
		{
			clause = MY_MANAGEDCLAUSE_STACK[i];
			if (clause_length[clause] == 2)
				reduce_if_negative_num[tested_var] += get_resolvant_num(clause);
		}
		reset_context();
	}
	push(tested_var, TESTED_VAR_STACK);
	return TRUE;
}
/* ---------------------------------------------------------------------------------- */

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	i, posi, nega;
	int num_clauses, max_num_clauses = -1;
	s_char pos2, neg2;
	long saved_num_back;
/**/	int val;

	NUM_BRANCH++;
	TESTED_VAR_STACK_fill_pointer = 0;

	for (var=0; var<NUM_VARS; var++)
	{
		if (var_state[var] == LIVE)
		{
			reduce_if_negative_num[var] = 0;
			reduce_if_positive_num[var] = 0;

			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
/***/
			}
			else
			{
				pos2 = num_pos_clause_of_length2[var];
				neg2 = num_neg_clause_of_length2[var];
				if ((neg2>0) && (pos2>0) && ((neg2+pos2)>3) )
				{
					if (examine(var) == NONE)
					{
						saved_num_back = NUM_BACK;
						unitclause_process();
						if (NUM_BACK > saved_num_back) return;
					}
				}
			}
		}
	}

	if (TESTED_VAR_STACK_fill_pointer < T)
	{
	/*	TESTED_VAR_STACK_fill_pointer = 0; */
		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 ((neg2>0) && (pos2>0) && ((neg2>1) || (pos2>1)) )
					if (reduce_if_negative_num[var] == 0)
						if (examine(var) == NONE)
						{
							saved_num_back = NUM_BACK;
							unitclause_process();
							if (NUM_BACK > saved_num_back)
								return;
						}
			}
	}

	if (TESTED_VAR_STACK_fill_pointer < T)
	{
		TESTED_VAR_STACK_fill_pointer = 0;
		for (var=0; var<NUM_VARS; var++)
			if (var_state[var] == LIVE)
				if (examine1(var) == NONE)
				{
					saved_num_back = NUM_BACK;
					unitclause_process();
					if (NUM_BACK > saved_num_back)
						return;
				}
	}
	for (i=0; i<TESTED_VAR_STACK_fill_pointer; i++)
	{
		var = TESTED_VAR_STACK[i];
		if (var_state[var] == LIVE)
		{
			posi = reduce_if_positive_num[var];
			nega = reduce_if_negative_num[var];
			num_clauses = posi*nega*1024 + posi + nega + 1;
			if (num_clauses > max_num_clauses)
			{
				chosen_var = var;
				max_num_clauses = num_clauses;
			}

		}
	}

	if (chosen_var == NONE)
		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
/***/
}
/* ---------------------------------------------------------------------------------- */
/* ---------------------------------------------------------------------------------- */
/* ---------------------------------------------------------------------------------- */



void remove_link(int clause)
/* called once in search_redundence */
{
	int lit;
	int *lits;
	struct node *pnode1, *pnode2, *pnode;

	lits = sat[clause];

	for (lit=*lits; lit!=NONE; lit=*(++lits))
	{
		pnode = (positive(lit) ? node_pos_in[lit] : node_neg_in[get_var_from_lit(lit)]);
		if (pnode == NULL)
			return;
		if (pnode->clause == clause)
		{
			if (positive(lit))
				node_pos_in[lit] = pnode->next;
			else
				node_neg_in[get_var_from_lit(lit)] = pnode->next;
		}
		else
		for (pnode1=pnode, pnode2=pnode->next; pnode2!=NULL; pnode2=pnode2->next)
		{
			if (pnode2->clause == clause)
			{
				pnode1->next = pnode2->next;
				break;
			}
			else
				pnode1 = pnode2;
		}
	}
}

s_char redundant(int *new_clause, int *old_clause)
/* called once in search_redundence */
{
	int j1=0, j2=0, lit1, lit2, old_clause_diff=0, new_clause_diff=0;

	while (((lit1=old_clause[j1]) != NONE) && ((lit2=new_clause[j2]) != NONE))
	{
		if (smaller_than(lit1, lit2))
		{
			j1++;
			old_clause_diff++;
		}
		else
		if (smaller_than(lit2, lit1))
		{
			j2++;
			new_clause_diff++;
		}
		else
		if (complement(lit1, lit2))
		{
			return FALSE;
			/* old_clause_diff++; new_clause_diff++; j1++; j2++; */
		}
		else
		{
			j1++;
			j2++;
		}
	}
	if ((lit1 == NONE) && (old_clause_diff == 0))
		/* the new clause is redundant or subsumed */
		return NEW_CLAUSE_REDUNDANT;
	if ((lit2 == NONE) && (new_clause_diff == 0))
		/* the old clause is redundant or subsumed */
		return OLD_CLAUSE_REDUNDANT;
	return FALSE;
}

int search_redundence(int *lits)
/* called once in add_resolvant, once in build_sat_instance */
{
	int lit, is_red;
	int *old_lits, *new_lits;
	struct node *pnode;

	new_lits = lits;
	for (lit=*lits; lit!=NONE; lit=*(++lits))
	{
		for (pnode = (positive(lit) ? node_pos_in[lit] : node_neg_in[get_var_from_lit(lit)]);
				pnode != NULL; pnode = pnode->next)
		{
			old_lits = sat[pnode->clause];
			is_red = redundant(new_lits, old_lits);
			if (is_red == OLD_CLAUSE_REDUNDANT)
			{
/*			printf("old clause %d is redundant\n", pnode->clause); */
				clause_state[pnode->clause] = DEAD;
				remove_link(pnode->clause);
			}
			else
			if (is_red == NEW_CLAUSE_REDUNDANT)
			{
				return NEW_CLAUSE_REDUNDANT;
			}
		}
	}
	return FALSE;
}
/* ---------------------------------------------------------------------------------- */

s_char get_resolvant(int *clause1, int *clause2, int *resolvant)
/* called once in add_resolvant */
{
	int lit1, lit2, num_diff=0, num_iden=0, num_opps=0, j1=0, j2=0, j, limited_length;

	while (((lit1=clause1[j1]) != NONE) && ((lit2=clause2[j2]) != NONE))
	{
		if (complement(lit1, lit2))
		{
			j1++;
			j2++;
			num_opps++;
		}
		else
		if (lit1 == lit2)
		{
			j1++;
			j2++;
			num_iden++;
		}
		else
		if (smaller_than(lit1, lit2))
		{
			num_diff++;
			j1++;
		}
		else
		{
			num_diff++;
			j2++;
		}
	}
	if (num_opps == 1)
	{
		if (clause1[j1] == NONE)
		{
			for ( ; clause2[j2] != NONE; j2++)
				num_diff++;
		}
		else
		{
			for ( ; clause1[j1] != NONE; j1++)
			num_diff++;
		}
		if ((j1==1) || (j2==1))
			limited_length = RESOLVANT_LENGTH;
		else
		if ((j1==2) && (j2==2))
			limited_length = 1;
		else
		if (j1<j2)
			limited_length = ((j1<RESOLVANT_LENGTH) ? j1 : RESOLVANT_LENGTH);
		else
			limited_length = ((j2<RESOLVANT_LENGTH) ? j2 : RESOLVANT_LENGTH);

		if (num_diff+num_iden <= limited_length)
		{
			j1 = 0;
			j2 = 0;
			j = 0;
			while (((lit1=clause1[j1]) != NONE) && ((lit2=clause2[j2]) != NONE))
			{
				if (lit1 == lit2)
				{
					resolvant[j] = lit1;
					j1++;
					j2++;
					j++;
				}
				else
				if (smaller_than(lit1, lit2))
				{
					resolvant[j] = lit1;
					j1++;
					j++;
				}
				else
				if (smaller_than(lit2, lit1))
				{
					resolvant[j] = lit2;
					j2++;
					j++;
				}
				else
				{
					j1++;
					j2++;
				}
			}
			if (clause1[j1] == NONE)
				while ((resolvant[j++]=clause2[j2++]) != NONE)
					;
			else
				while ((resolvant[j++]=clause1[j1++]) != NONE)
					;
			return TRUE;
		}
	}
	return FALSE;
}

int add_resolvant(int *lits)
/* called once in build_sat_instance */
{
	int j, lit, is_red, resolvant[RESOLVANT_LENGTH+1];
	s_char is_res;
	int *old_lits, *new_lits, *res;
	struct node *pnode;

	new_lits = lits;
	for (lit=*lits; lit!=NONE; lit=*(++lits))
		for (pnode = (positive(lit) ? node_neg_in[lit] : node_pos_in[get_var_from_lit(lit)]);
					pnode != NULL; pnode = pnode->next)
		{
			old_lits = sat[pnode->clause];
			is_res = get_resolvant(new_lits, old_lits, resolvant);
			if (is_res != FALSE)
			{
				is_red = search_redundence(resolvant);
				if (is_red != NEW_CLAUSE_REDUNDANT)
				{
					res = (int *) malloc((RESOLVANT_LENGTH+1)*sizeof(int));
					clause_state[NUM_CLAUSES] = LIVE;
					j = 0;
					while ((res[j]=resolvant[j]) != NONE)
						++j;
					if (j==0)
						return NONE;
					sat[NUM_CLAUSES] = res;
					clause_length[NUM_CLAUSES++] = j;
				}
			}
		}

	return TRUE;
}
/* ---------------------------------------------------------------------------------- */

struct node *allocate_node(void)
/* called once in set_link */
{
	struct resource *presource;
	if (CLAUSE_NODES_pointer == MAX_NODE_NUMBER)
	{
		CLAUSE_NODES = (struct node *) malloc(MAX_NODE_NUMBER*sizeof(struct node));
		CLAUSE_NODES_pointer = 0;
		presource = (struct resource *) malloc(sizeof(struct resource));
		presource->next = resources;
		resources = presource;
		presource->pnode = CLAUSE_NODES;
	}
	return &(CLAUSE_NODES[CLAUSE_NODES_pointer++]);
}

void set_link(int clause)
/* called once in build_sat_instance */
{
	int lit;
	int *lits;
	struct node *pnode;

	lits = sat[clause];
	for (lit=*lits; lit!=NONE; lit=*(++lits))
	{
		pnode = allocate_node();
		pnode->clause = clause;
		if (positive(lit))
		{
			pnode->next = node_pos_in[lit];
			node_pos_in[lit] = pnode;
		}
		else
		{
			pnode->next = node_neg_in[get_var_from_lit(lit)];
			node_neg_in[get_var_from_lit(lit)] = pnode;
		}
	}
}

void free_resources(void)
/* called once in build_sat_instance */
{
	struct resource *presource;
	while (resources != NULL)
	{
		free(resources->pnode);
		presource = resources;
		resources = resources->next;
		free(presource);
	}
}

int* copy_clauses(struct node *node_in)
/* called twice in build_sat_instance */
{
	int j=0, *in;
	struct node *pnode;

	pnode = node_in;
	while (pnode != NULL)
	{
		j++;
		pnode = pnode->next;
	}
	in = (int *) malloc((j+1)*sizeof(int));
	j = 0;
	pnode = node_in;
	while (pnode != NULL)
	{
		in[j] = pnode->clause;
		j++;
		pnode = pnode->next;
	}
	in[j] = NONE;
	return in;
}
/* ---------------------------------------------------------------------------------- */


s_char build_sat_instance(char *input_file)
/* called three times in build */
{
	FILE* fp_in = fopen(input_file, "r");
	char ch, tautology, word[WORD_LENGTH];
	int i, j, length, ii, jj, lit, tmp, lits[tab_variable_size], *plit, NUM_CLAUSES1;

	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);

	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]);
		}
		tautology = FALSE;
		/* test if some literals are redundant and sort the clause */
		for (ii=0; ii<length-1; ii++)
		{
			lit = lits[ii];
			for (jj=ii+1; jj<length; jj++)
			{
				if (abs(lit) > abs(lits[jj]))
				{
					tmp = lits[jj];
					lits[jj] = lit;
					lit = tmp;
				}
				else
				if (lit == lits[jj])
				{
					lits[jj--] = lits[--length];
					lits[length] = 0;
					printf("literal %d is redundant in clause %d\n", lit, i);
				}
				else
				if (abs(lit) == lits[jj])
				{
					printf("clause %d is a tautology\n", i);
					tautology = TRUE;
					break;
				}
			}
			if (tautology == TRUE)
				break;
			else
				lits[ii] = lit;
		}
		if (tautology == FALSE)
		{
			sat[i] = (int *) malloc((length+1)*sizeof(int));
			for (j=0; lits[j]!=0; j++)
			{
				if (lits[j] > 0)
					sat[i][j] = lits[j]-1;
				else
					sat[i][j] = abs(lits[j]) + NUM_VARS -1;
			}
			sat[i][j] = NONE;
			clause_length[i] = length;
			clause_state[i] = LIVE;
		}
		else
		{
			/* mistake with this bit? */
			/* NUM_CLAUSES--; */
			i--;
		}
	}
	fclose(fp_in);

	for (i=0; i<NUM_VARS; i++)
	{
		node_neg_in[i] = NULL;
		node_pos_in[i] = NULL;
		var_state[i] = LIVE;
	}

	INIT_NUM_CLAUSES = NUM_CLAUSES;

	for(i=0; i<NUM_CLAUSES; i++)
	{
		plit = sat[i];
		length = clause_length[i];
		if (length==1)
			push(i, UNITCLAUSE_STACK);
		if (search_redundence(plit) != NEW_CLAUSE_REDUNDANT)
		{
			if (add_resolvant(plit) == NONE)
				return NONE;
			else
				set_link(i);
		}
		else
			clause_state[i] = DEAD;
	}
	NUM_CLAUSES1 = 0;
	for (i=0; i<NUM_CLAUSES; i++)
	{
		if (clause_state[i] == LIVE)
			NUM_CLAUSES1++;
	}
	NUM_CLAUSES = NUM_CLAUSES1;

	for(i=0; i<NUM_VARS; i++)
	{
		neg_in[i] = copy_clauses(node_neg_in[i]);
		pos_in[i] = copy_clauses(node_pos_in[i]);
	}
	free_resources();
	return TRUE;
}


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;
}


s_char build(int argc, char *argv[])
/* called once in main */
{
	if (argc == 3)
	{
		if ((argv[2][0] == '-') && (argv[2][1] == 's'))
			return build_simple_sat_instance(argv[1]);
		else if ((argv[1][0] == '-') && (argv[1][1] == 's'))
			return build_simple_sat_instance(argv[2]);
		else if (argv[1][0] == '-')
			return build_sat_instance(argv[2]);
		else return build_sat_instance(argv[1]);
	}
	else return build_sat_instance(argv[1]);
}
/* ---------------------------------------------------------------------------------- */
/* ---------------------------------------------------------------------------------- */


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;

/*	FILE* fp_out;
	fp_out = fopen("satz.sol", "w");
	fclose(fp_out);
*/

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

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

int main(int argc, char *argv[])
{
	clock_t begintime, endtime;
	int return_value;
	struct tms *a_tms;

	if (argc < 2)
	{
		printf("Usage:\tsatz [-s] input_file\n");
		printf("  output format:\n");
		printf("sat     time    branch  back    unit    pure\n");
		return -1;
	}

	a_tms = (struct tms *) malloc(sizeof(struct tms));
	times(a_tms);
	begintime = a_tms->tms_utime;

	switch (build(argc, argv))
	{
		case FALSE:
			printf("Input file error\n");
			return -1;
		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())
	{
		if (verify_solution())
			return_value = 1;
		else
			return_value = -1;
	}
	else
		return_value = 0;

	printf("%d %5.3f %d %d %d %d\n",
			return_value, (double)(endtime-begintime)/CLK_TCK,
			NUM_BRANCH, NUM_BACK,	NUM_UNIT, NUM_PURE);

	return return_value;
}