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

											 NB-Satz
			written by Peter G. Stock (December 1999)


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

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

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <time.h>
#include <sys/times.h>
/*#include <assert.h>*/

typedef signed char S_char;
typedef unsigned char U_char;
typedef struct { int var; int *dom; S_char state; int clause; } lit;
typedef struct { int var; int val; } var_val;

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

/* macro definitions */
#define pop(stack) stack[--stack ## _fill_pointer]
#define push(item, stack) stack[stack ## _fill_pointer++] = item
#define satisfiable() CLAUSE_STACK_fill_pointer == NUM_CLAUSES

lit			**sat;

lit			***lits_with_var;
lit			****lits_with_var_with_val;
lit			****lits_with_var_without_val;

S_char	*clause_state;
U_char	*clause_length;

S_char	*var_state;
S_char	*var_current_value;
S_char	**var_rest_value;
S_char	**lit_state;

int			**num_2clauses_with_var_with_val;
int			**num_3clauses_with_var_with_val;
int			*clause_flags;

int			*saved_clause_stack;
int			*saved_managedclause_stack;
int			*saved_restrictedlit_stack;
int			*saved_removedlit_stack;


int			*VARIABLE_STACK;
int			*CLAUSE_STACK;
int			*MANAGEDCLAUSE_STACK;
int			*UNITCLAUSE_STACK;
var_val	*RESTRICTEDLIT_STACK;
lit			**REMOVEDLIT_STACK;

int			VARIABLE_STACK_fill_pointer = 0;
int			CLAUSE_STACK_fill_pointer = 0;
int			MANAGEDCLAUSE_STACK_fill_pointer = 0;
int			UNITCLAUSE_STACK_fill_pointer = 0;
int			RESTRICTEDLIT_STACK_fill_pointer = 0;
int			REMOVEDLIT_STACK_fill_pointer = 0;

int			*LA_VARIABLE_STACK;
int			*LA_MANAGEDCLAUSE_STACK;
int			*LA_UNITCLAUSE_STACK;
var_val	*LA_RESTRICTEDLIT_STACK;
lit			**LA_REMOVEDLIT_STACK;
int			*TESTED_VAR_STACK;

int			LA_VARIABLE_STACK_fill_pointer = 0;
int			LA_MANAGEDCLAUSE_STACK_fill_pointer = 0;
int			LA_UNITCLAUSE_STACK_fill_pointer = 0;
int			LA_RESTRICTEDLIT_STACK_fill_pointer = 0;
int			LA_REMOVEDLIT_STACK_fill_pointer = 0;
int			TESTED_VAR_STACK_fill_pointer = 0;

int			**reduce_num;
int			NUM_VARS, NUM_CLAUSES, DOMAIN_SIZE;
int			*tmp_vals, *y_vals, *n_vals;	/* global temporaries to hold literal values */
long		NUM_UNIT=0, NUM_SEMIUNIT=0, NUM_PURE=0, NUM_SEMIPURE=0, NUM_BRANCH=0, NUM_BACK=0,
				NUM_EXAMINED=0, NUM_FAILED=0, NUM_LA_UNIT=0, NUM_LA_SEMIUNIT=0;


#ifdef print_tree
void print_formula(void)
{
	int c_length, clause, var, val, *val_ptr, first_val;
	lit *lit_ptr;

	for (clause=0; clause<NUM_CLAUSES; clause++)
	{
		if (clause_state[clause] == LIVE)
		{
			c_length = 0;
			printf("\t[ ");
			lit_ptr = sat[clause];
			for (var=lit_ptr->var; var!=NONE; var=(++lit_ptr)->var)
			{
				if (var_state[var] == LIVE && lit_ptr->state == LIVE)
				{
					c_length++;
					printf("%d{", var+1);
					first_val = TRUE;
					val_ptr = lit_ptr->dom;
					for (val=*val_ptr; val!=NONE; val=*(++val_ptr))
					{
						if (lit_state[var][val] == LIVE)
						{
							if (first_val == TRUE)
							{
								printf("%d", val);
								first_val = FALSE;
							}
							else
								printf(",%d", val);
						}
					}
					printf("} ");
				}
			}
			if (clause_length[clause]!=c_length)
				printf("<actual:%d, stored:%d>", c_length, clause_length[clause]);
			printf("]\n");
		}
	}
	printf("\n");
}
#endif
/* ---------------------------------------------------------------------------------- */


int backtrack(void)
/* called twice in unitclause_process, once in examine */
{
	int i, var, val, c;
	S_char *var_rest_value_var;
	lit *lp, **lp_ptr;

	NUM_BACK++;
	UNITCLAUSE_STACK_fill_pointer = 0;

	while (VARIABLE_STACK_fill_pointer != 0)
	{
		var = pop(VARIABLE_STACK);
		var_rest_value_var = var_rest_value[var];
		if (var_rest_value_var[0] == NONE)
			var_state[var] = LIVE;
		else
		{
			for (i=saved_clause_stack[var]; i<CLAUSE_STACK_fill_pointer; i++)
				clause_state[CLAUSE_STACK[i]] = LIVE;
			CLAUSE_STACK_fill_pointer = saved_clause_stack[var];

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

			for (i=saved_restrictedlit_stack[var]; i<RESTRICTEDLIT_STACK_fill_pointer; i++)
				lit_state[RESTRICTEDLIT_STACK[i].var][RESTRICTEDLIT_STACK[i].val] = LIVE;
			RESTRICTEDLIT_STACK_fill_pointer = saved_restrictedlit_stack[var];

			for (i=saved_removedlit_stack[var]; i<REMOVEDLIT_STACK_fill_pointer; i++)
				REMOVEDLIT_STACK[i]->state = LIVE;
			REMOVEDLIT_STACK_fill_pointer = saved_removedlit_stack[var];

			val = var_rest_value_var[0];
			var_current_value[var] = val;
			for (i=0; var_rest_value_var[i]!=NONE; i++)
				var_rest_value_var[i] = var_rest_value_var[i+1];
			push(var, VARIABLE_STACK);

			/* remove variables */
			lp_ptr = lits_with_var_without_val[var][val];
			for (lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr))
			{
				c = lp->clause;
				if (clause_state[c] == LIVE && lp->state == LIVE)
				{
					switch (clause_length[c])
					{
						case 2:
							clause_length[c]--;
							push(c, UNITCLAUSE_STACK);
							break;
						default:
							clause_length[c]--;
							push(c, MANAGEDCLAUSE_STACK);
					}
				}
			}

			/* remove clauses */
			lp_ptr = lits_with_var_with_val[var][val];
			for (lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr))
			{
				c = lp->clause;
				/* assert(lp->state == LIVE);	must be the case because lit contains val */
				if (clause_state[c] == LIVE)
				{
					clause_state[c] = DEAD;
					push(c, CLAUSE_STACK);
				}
			}

		/***/
			#ifdef verbose
			printf("Backtrack branch: %d -> %d\n", var+1, val);
			#ifdef print_tree
			print_formula();
			#endif
			#endif
		/***/
			return TRUE;
		}
	}

	return FALSE;
}
/* ---------------------------------------------------------------------------------- */


void unitclause_process(void)
/* called twice in examine, once in main */
{
	int i, c, var, val, live_val, *val_ptr, lit_size, l_size, unitclause, uc_pos;
	S_char *lit_state_var;
	var_val vv;
	lit *lit_ptr, *lp, **lp_ptr;
/***/
	#ifdef print_tree
	int made_a_semi_unit;
	#endif
/***/

	for (uc_pos=0; uc_pos<UNITCLAUSE_STACK_fill_pointer; uc_pos++)
	{
		unitclause = UNITCLAUSE_STACK[uc_pos];
		clause_length[unitclause]++;

		if (clause_state[unitclause] == LIVE)
		{
			clause_state[unitclause] = DEAD;
			push(unitclause, CLAUSE_STACK);

			lit_ptr = sat[unitclause];
			for (var=lit_ptr->var; var!=NONE; var=(++lit_ptr)->var)
			{
				if (var_state[var] == LIVE && lit_ptr->state == LIVE)
				{
					lit_state_var = lit_state[var];
					for (i=0; i<DOMAIN_SIZE; i++)
						tmp_vals[i] = DEAD;
					lit_size = 0;
					val_ptr = lit_ptr->dom;
					for (val=*val_ptr; val!=NONE; val=*(++val_ptr))
					{
						if (lit_state_var[val] == LIVE)
						{
							tmp_vals[val] = LIVE;
							lit_size++;
							live_val = val;
						}
					}

					if (lit_size == 1)	/* normal unit propagation */
					{
						NUM_UNIT++;
						/* set variable value */
						var_current_value[var] = live_val;
						var_rest_value[var][0] = NONE;

						/* remove variables */
						lp_ptr = lits_with_var_without_val[var][live_val];
						for (lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr))
						{
							c = lp->clause;
							if (clause_state[c] == LIVE && lp->state == LIVE)
								switch (clause_length[c])
								{
									case 1:
									/***/
										#ifdef verbose
										printf("Failed unit: %d -> %d\n", var+1, live_val);
										#endif
									/***/
										for (i=uc_pos+1; i<UNITCLAUSE_STACK_fill_pointer; i++)
											clause_length[UNITCLAUSE_STACK[i]]++;
										backtrack();
										return;
									case 2:
										clause_length[c]--;
										push(c, UNITCLAUSE_STACK);
										break;
									default:
										clause_length[c]--;
										push(c, MANAGEDCLAUSE_STACK);
								}
						}

						/* set variable state */
						var_state[var] = DEAD;
						push(var, VARIABLE_STACK);

						/* remove clauses */
						lp_ptr = lits_with_var_with_val[var][live_val];
						for (lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr))
						{
							c = lp->clause;
							/* assert(lp->state == LIVE);	must be the case because lit contains val */
							if (clause_state[c] == LIVE)
							{
								clause_state[c] = DEAD;
								push(c, CLAUSE_STACK);
							}
						}
					/***/
						#ifdef verbose
						printf("Unit: %d -> %d\n", var+1, live_val);
						#ifdef print_tree
						print_formula();
						#endif
						#endif
					/***/
					}
					else	/* lit size != 1 */
					{
						/* tighten literal constraints (update lit_state[var]) */
					/***/
						#ifdef print_tree
						made_a_semi_unit = FALSE;
						#endif
					/***/
						for (val=0; val<DOMAIN_SIZE; val++)
						{
							if (lit_state_var[val] == LIVE && tmp_vals[val] == DEAD)
							{
								NUM_SEMIUNIT++;
								lit_state_var[val] = DEAD;
								vv.var = var;
								vv.val = val;
								push(vv, RESTRICTEDLIT_STACK);
							/***/
								#ifdef verbose
								printf("Semi-unit: %d //-> %d\n", var+1, val);
								#ifdef print_tree
								made_a_semi_unit = TRUE;
								#endif
								#endif
							/***/
							}
						}

						/* remove FALSE literals from clauses
							remove clauses that contain a TRUE literal */
						lp_ptr = lits_with_var[var];
						for (lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr))
						{
							c = lp->clause;
							if (clause_state[c] == LIVE && lp->state == LIVE)
							{
								l_size = 0;
								val_ptr = lp->dom;
								for (val=*val_ptr; val!=NONE; val=*(++val_ptr))
								{
									if (lit_state_var[val] == LIVE)
										l_size++;
								}
								if (l_size == 0)
								{
									/* remove literal */
									switch (clause_length[c])
									{
										case 1:
										/***/
											#ifdef verbose
											printf("Failed semi-unit: %d\n", var+1);
											#endif
										/***/
											for (i=uc_pos+1; i<UNITCLAUSE_STACK_fill_pointer; i++)
												clause_length[UNITCLAUSE_STACK[i]]++;
											backtrack();
											return;
										case 2:
											lp->state = DEAD;
											push(lp, REMOVEDLIT_STACK);
											clause_length[c]--;
											push(c, UNITCLAUSE_STACK);
											break;
										default:
											lp->state = DEAD;
											push(lp, REMOVEDLIT_STACK);
											clause_length[c]--;
											push(c, MANAGEDCLAUSE_STACK);
									}
								}
								else if (l_size == lit_size)
								{
									/* remove clause */
									clause_state[c] = DEAD;
									push(c, CLAUSE_STACK);
								}
							} /* if (clause_state[c] == LIVE && lp_ptr->state == LIVE) */
						} /* for (lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr)) */

					/***/
						#ifdef print_tree
						if (made_a_semi_unit == TRUE)
							print_formula();
						#endif
					/***/
					} /* else (lit_size != 1) */

					break;
				} /* if (var_state[var] == LIVE && lit_ptr->state == LIVE) */
			} /* for (var=lit_ptr->var; var!=NONE; var=(++lit_ptr)->var) */
		} /* if (clause_state[unitclause] == LIVE) */
	} /* for (uc_pos = 0; uc_pos < UNITCLAUSE_STACK_fill_pointer; uc_pos++) */
	UNITCLAUSE_STACK_fill_pointer = 0;
}
/* ---------------------------------------------------------------------------------- */
/* ---------------------------------------------------------------------------------- */


int lookahead_unitclause_process(void)
/* called once in examine */
/* similar to unitclause_process, but doesn't remove clauses from the formula */
{
	int i, c, var, val, live_val, *val_ptr, lit_size, l_size, unitclause, uc_pos;
	S_char *lit_state_var;
	var_val vv;
	lit *lit_ptr, *lp, **lp_ptr;

	for (uc_pos=0; uc_pos<LA_UNITCLAUSE_STACK_fill_pointer; uc_pos++)
	{
		unitclause = LA_UNITCLAUSE_STACK[uc_pos];
		clause_length[unitclause]++;

		lit_ptr = sat[unitclause];
		for(var=lit_ptr->var; var!=NONE; var=(++lit_ptr)->var)
		{
			if (var_state[var] == LIVE && lit_ptr->state == LIVE)
			{
				lit_state_var = lit_state[var];
				for (i=0; i<DOMAIN_SIZE; i++)
					tmp_vals[i] = DEAD;
				lit_size = 0;
				val_ptr = lit_ptr->dom;
				for (val=*val_ptr; val!=NONE; val=*(++val_ptr))
				{
					if (lit_state_var[val] == LIVE)
					{
						tmp_vals[val] = LIVE;
						lit_size++;
						live_val = val;
					}
				}

				if (lit_size == 1)	/* normal unit propagation */
				{
					/* do not need to set variable value */
					/*var_current_value[var] = live_val;*/
					/*var_rest_value[var][0] = NONE;*/

					/* remove variables */
					lp_ptr = lits_with_var_without_val[var][live_val];
					for (lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr))
					{
						c = lp->clause;
						if (clause_state[c] == LIVE && lp->state == LIVE)
							switch (clause_length[c])
							{
								case 1:
									for (i=uc_pos+1; i<LA_UNITCLAUSE_STACK_fill_pointer; i++)
										clause_length[LA_UNITCLAUSE_STACK[i]]++;
									NUM_FAILED++;
									return FALSE;
								case 2:
									clause_length[c]--;
									push(c, LA_UNITCLAUSE_STACK);
									break;
								default:
									clause_length[c]--;
									push(c, LA_MANAGEDCLAUSE_STACK);
							}
					}

					/* set variable state */
					var_state[var] = DEAD;
					push(var, LA_VARIABLE_STACK);
				}
				else	/* lit size != 1 */
				{
					/* tighten literal constraints (update lit_state[var]) */
					for (val=0; val<DOMAIN_SIZE; val++)
						if (lit_state_var[val] == LIVE && tmp_vals[val] == DEAD)
						{
							lit_state_var[val] = DEAD;
							vv.var = var;
							vv.val = val;
							push(vv, LA_RESTRICTEDLIT_STACK);
						}

					/* remove FALSE literals from clauses */
					lp_ptr = lits_with_var[var];
					for (lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr))
					{
						c = lp->clause;
						if (clause_state[c] == LIVE && lp->state == LIVE)
						{
							l_size = 0;
							val_ptr = lp->dom;
							for (val=*val_ptr; val!=NONE; val=*(++val_ptr))
							{
								if (lit_state_var[val] == LIVE)
									l_size++;
							}
							if (l_size == 0)
							{
								/* remove literal */
								switch (clause_length[c])
								{
									case 1:
										for (i=uc_pos+1; i<LA_UNITCLAUSE_STACK_fill_pointer; i++)
											clause_length[LA_UNITCLAUSE_STACK[i]]++;
										NUM_FAILED++;
										return FALSE;
									case 2:
										lp->state = DEAD;
										push(lp, LA_REMOVEDLIT_STACK);
										clause_length[c]--;
										push(c, LA_UNITCLAUSE_STACK);
										break;
									default:
										lp->state = DEAD;
										push(lp, LA_REMOVEDLIT_STACK);
										clause_length[c]--;
										push(c, LA_MANAGEDCLAUSE_STACK);
								}
							}
						} /* if (clause_state[c] == LIVE && lp_ptr->state == LIVE) */
					} /* for (lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr)) */
				} /* else (lit_size != 1) */

				break;
			} /* if (var_state[var] == LIVE && lit_ptr->state == LIVE) */
		} /* for(var=lit_ptr->var; var!=NONE; var=(++lit_ptr)->var) */
	} /* for (uc_pos=0; uc_pos!=LA_UNITCLAUSE_STACK_fill_pointer; uc_pos++) */
	return TRUE;
}
/* ---------------------------------------------------------------------------------- */

int examine(int var) /* int all */
/* called three times in pick_variable */
{
	int i, c, val, *val_ptr, y_vals_cnt, n_vals_cnt, l_size, prediction, saved_num_back,
			*reduce_num_var;
	S_char *lit_state_var;
	var_val vv;
	lit *lp, **lp_ptr, ***lits_with_var_without_val_var=lits_with_var_without_val[var];
/***/
	#ifdef print_tree
	int made_a_semi_unit;
	#endif
/***/

	NUM_EXAMINED++;

	lit_state_var = lit_state[var];
	reduce_num_var = reduce_num[var];
	y_vals_cnt = 0;
	n_vals_cnt = 0;
	for (val=0; val<DOMAIN_SIZE; val++)
	{
		if (lit_state_var[val] == LIVE)
		{
		/***/
			#ifdef verbose
			printf("LA: %d,%d  ", var+1, val);
			#endif
		/***/
			/* do not need to set variable value */
			/*var_current_value[var] = val;*/
			/*var_rest_value[var][0] = NONE;*/
			var_state[var] = DEAD;
			push(var, LA_VARIABLE_STACK);

			/* remove variables */
			lp_ptr = lits_with_var_without_val_var[val];
			for(lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr))
			{
				c = lp->clause;
				if (clause_state[c] == LIVE && lp->state == LIVE)
				{
					switch (clause_length[c])
					{
						case 2:
							clause_length[c]--;
							push(c, LA_UNITCLAUSE_STACK);
							break;
						default:
							clause_length[c]--;
							push(c, LA_MANAGEDCLAUSE_STACK);
					}
				}
			}

			prediction = lookahead_unitclause_process();
			reduce_num_var[val] = LA_MANAGEDCLAUSE_STACK_fill_pointer;
			if (prediction == FALSE)
			{
				n_vals[n_vals_cnt++] = val;
			/***/
				#ifdef verbose
				printf("F\n");
				#endif
			/***/
			}
			else
			{
 				y_vals[y_vals_cnt++] = val;
			/***/
				#ifdef verbose
				printf("T\n");
				#endif
			/***/
			}

			LA_UNITCLAUSE_STACK_fill_pointer = 0;
			for (i=0; i<LA_VARIABLE_STACK_fill_pointer; i++)
				var_state[LA_VARIABLE_STACK[i]] = LIVE;
			LA_VARIABLE_STACK_fill_pointer = 0;
			for (i=0; i<LA_MANAGEDCLAUSE_STACK_fill_pointer; i++)
				clause_length[LA_MANAGEDCLAUSE_STACK[i]]++;
			LA_MANAGEDCLAUSE_STACK_fill_pointer = 0;
			for (i=0; i<LA_RESTRICTEDLIT_STACK_fill_pointer; i++)
				lit_state[LA_RESTRICTEDLIT_STACK[i].var][LA_RESTRICTEDLIT_STACK[i].val] = LIVE;
			LA_RESTRICTEDLIT_STACK_fill_pointer = 0;
			for (i=0; i<LA_REMOVEDLIT_STACK_fill_pointer; i++)
				LA_REMOVEDLIT_STACK[i]->state = LIVE;
			LA_REMOVEDLIT_STACK_fill_pointer = 0;
		}
	}

	if (y_vals_cnt == 0)
	{
		/* all value instantiations lead to contradictions */
	/***/
		#ifdef verbose
		printf("Failed LA: %d\n", var+1);
		#endif
	/***/
		backtrack();
		return FALSE;
	}
	else if (y_vals_cnt == 1)	/* normal unit propagation */
	{
		NUM_LA_UNIT++;
		/* propagate the literal */
		val = y_vals[0];
		var_current_value[var] = val;
		var_rest_value[var][0] = NONE;
		var_state[var] = DEAD;
		push(var, VARIABLE_STACK);

		/* remove variables */
		lp_ptr = lits_with_var_without_val_var[val];
		for (lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr))
		{
			c = lp->clause;
			if (clause_state[c] == LIVE && lp->state == LIVE)
			{
				/* assert(clause_length[c] != 1);	cannot happen because no unit clauses can exist
						on the first call to here. Although some may be generated by this function,
						unitclause_process is called at the end of it */
				switch (clause_length[c])
				{
					case 2:
						clause_length[c]--;
						push(c, UNITCLAUSE_STACK);
						break;
					default:
						clause_length[c]--;
						push(c, MANAGEDCLAUSE_STACK);
				}
			}
		}

		/* remove clauses */
		lp_ptr = lits_with_var_with_val[var][val];
		for (lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr))
		{
			c = lp->clause;
			/* assert(lp->state == LIVE);	must be the case because lit contains val */
			if (clause_state[c] == LIVE)
			{
				clause_state[c] = DEAD;
				push(c, CLAUSE_STACK);
			}
		}
	/***/
		#ifdef verbose
		printf("LA Unit: %d -> %d\n", var+1, val);
		#ifdef print_tree
		print_formula();
		#endif
		#endif
	/***/
		saved_num_back = NUM_BACK;
		unitclause_process();
		if (NUM_BACK > saved_num_back)
			return FALSE;
	}
	else if (n_vals_cnt > 0)	/* restrict the literal */
	{
		/* tighten literal constraints (update lit_state[var]) */
	/***/
		#ifdef print_tree
		made_a_semi_unit = FALSE;
		#endif
	/***/
		for (i=0; i<n_vals_cnt; i++)
		{
			NUM_LA_SEMIUNIT++;
			val = n_vals[i];
			lit_state_var[val] = DEAD;
			vv.var = var;
			vv.val = val;
			push(vv, RESTRICTEDLIT_STACK);
		/***/
			#ifdef verbose
			printf("LA Semi-unit: %d //-> %d\n", var+1, val);
			#ifdef print_tree
			made_a_semi_unit = TRUE;
			#endif
			#endif
		/***/
		}

		/* remove FALSE literals from clauses
			remove clauses that contain a TRUE literal */
		lp_ptr = lits_with_var[var];
		for (lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr))
		{
			c = lp->clause;
			if (clause_state[c] == LIVE && lp->state == LIVE)
			{
				l_size = 0;
				val_ptr = lp->dom;
				for (val=*val_ptr; val!=NONE; val=*(++val_ptr))
				{
					if (lit_state_var[val] == LIVE)
						l_size++;
				}
				if (l_size == 0)
				{
					/* remove literal */
					/* assert(clause_length[c] != 1);	cannot happen because no unit clauses can exist
							on the first call to here. Although some may be generated by this function,
							unitclause_process is called at the end of it */
					switch (clause_length[c])
					{
						case 2:
							lp->state = DEAD;
							push(lp, REMOVEDLIT_STACK);
							clause_length[c]--;
							push(c, UNITCLAUSE_STACK);
							break;
						default:
							lp->state = DEAD;
							push(lp, REMOVEDLIT_STACK);
							clause_length[c]--;
							push(c, MANAGEDCLAUSE_STACK);
					}
				}
				else if (l_size == y_vals_cnt)
				{
					/* remove clause */
					clause_state[c] = DEAD;
					push(c, CLAUSE_STACK);
				}
			}
		}

	/***/
		#ifdef print_tree
		if (made_a_semi_unit == TRUE)
			print_formula();
		#endif
	/***/
		saved_num_back = NUM_BACK;
		unitclause_process();
		if (NUM_BACK > saved_num_back)
			return FALSE;
	}

	push(var, TESTED_VAR_STACK);
	return TRUE;
}
/* ---------------------------------------------------------------------------------- */
/* ---------------------------------------------------------------------------------- */

int pick_variable(void)
/* called once in branch */
{
	int i, var, val, vals_cnt, chosen_var = NONE, *reduce_num_var;
	long Atotal, num_clauses, max_num_clauses = -1;
	S_char *lit_state_var;

	/* examine all variables */
	TESTED_VAR_STACK_fill_pointer = 0;
	for (var=0; var<NUM_VARS; var++)
	{
		if (var_state[var] == LIVE)
			if (examine(var) == FALSE)
				return NONE;
	}

	/* choose variable */
	for (i=0; i<TESTED_VAR_STACK_fill_pointer; i++)
	{
		var = TESTED_VAR_STACK[i];
		if (var_state[var] == LIVE)
		{
			lit_state_var = lit_state[var];
			reduce_num_var = reduce_num[var];
			Atotal = 0;
			vals_cnt = 0;
			for (val=0; val<DOMAIN_SIZE; val++)
			{
				if (lit_state_var[val] == LIVE)
				{
					vals_cnt++;
					Atotal += reduce_num_var[val];
				}
			}

/*			num_clauses = Mtotal*1024 + Atotal + 1;*/
			num_clauses = (Atotal+1) / vals_cnt;

			if (num_clauses > max_num_clauses)
			{
				chosen_var = var;
				max_num_clauses = num_clauses;
			}
		}
	}
	return chosen_var;
}
/* ---------------------------------------------------------------------------------- */
/* ---------------------------------------------------------------------------------- */

void branch(void)
/* called once in main */
{
	int i, var, chosen_var, val, chosen_val, pure_val, c,
		y_vals_cnt, n_vals_cnt, clause_flags_cnt, clause2_num, clause3_num,
		*num_2clauses_wv_wv_var, *num_3clauses_wv_wv_var;
	S_char *lit_state_var, *var_rest_value_chosen_var;
	var_val vv;
	lit *lp, **lp_ptr, ***lits_with_var_with_val_var;

	for (var=0; var<NUM_VARS; var++)
	{
		if (var_state[var] == LIVE)
		{
			lit_state_var = lit_state[var];
			lits_with_var_with_val_var = lits_with_var_with_val[var];
			num_2clauses_wv_wv_var = num_2clauses_with_var_with_val[var];
			num_3clauses_wv_wv_var = num_3clauses_with_var_with_val[var];
			y_vals_cnt = 0;
			n_vals_cnt = 0;
			for (i=0; i<NUM_CLAUSES; i++)
				clause_flags[i] = FALSE;
			clause_flags_cnt = 0;
			for (val=0; val<DOMAIN_SIZE; val++)
			{
				if (lit_state_var[val] == LIVE)
				{
					/* set the number of clauses with var with val */
					clause2_num = 0;
					clause3_num = 0;
					lp_ptr = lits_with_var_with_val_var[val];
					for (lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr))
					{
						c = lp->clause;
						if (clause_state[c] == LIVE && lp->state == LIVE)
						{
							if (clause_length[c] == 2)
								clause2_num++;
							else
								clause3_num++;

							/* make sure that the relevant clause flag is set */
							if (clause_flags[c] == FALSE)
							{
								clause_flags[c] = TRUE;
								clause_flags_cnt++;
							}
						}
					}
					num_2clauses_wv_wv_var[val] = clause2_num;
					num_3clauses_wv_wv_var[val] = clause3_num;

					if (clause2_num + clause3_num == 0)
						n_vals[n_vals_cnt++] = val;
					else
						y_vals[y_vals_cnt++] = val;
				}
			}

			if (y_vals_cnt == 0)
			{
				NUM_PURE++;
				/* eliminate a variable not in the formula */
				var_current_value[var] = NONE;
				var_rest_value[var][0] = NONE;
				var_state[var] = DEAD;
				push(var, VARIABLE_STACK);
			/***/
				#ifdef verbose
				printf("Pure: %d -> any\n", var+1);
				#endif
			/***/
			}
			else
			{
				pure_val = NONE;
				for (val=0; val<DOMAIN_SIZE; val++)
				{
					if (lit_state_var[val] == LIVE)
					{
						if (num_2clauses_wv_wv_var[val] + num_3clauses_wv_wv_var[val] == clause_flags_cnt)
						{
							pure_val = val;
							break;
						}
					}
				}

				if (pure_val != NONE)
				{
					NUM_PURE++;
					/* normal pure literal elimination */
					var_current_value[var] = pure_val;
					var_rest_value[var][0] = NONE;
					var_state[var] = DEAD;
					push(var, VARIABLE_STACK);

					/* remove clauses */
					lp_ptr = lits_with_var_with_val_var[pure_val];
					for (lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr))
					{
						c = lp->clause;
						/* assert(lp->state == LIVE);	must be the case because lit contains val */
						if (clause_state[c] == LIVE)
						{
							clause_state[c] = DEAD;
							push(c, CLAUSE_STACK);
						}
					}

				/***/
					#ifdef verbose
					printf("Pure: %d -> %d\n", var+1, pure_val);
					#ifdef print_tree
					print_formula();
					#endif
					#endif
				/***/
				}
				else if (n_vals_cnt > 0)
				{
					/* tighten literal constraints (update lit_state[var]) */
					for (i=0; i<n_vals_cnt; i++)
					{
						NUM_SEMIPURE++;
						val = n_vals[i];
						lit_state_var[val] = DEAD;
						vv.var = var;
						vv.val = val;
						push(vv, RESTRICTEDLIT_STACK);
					/***/
						#ifdef verbose
						printf("Semi-pure: %d //-> %d\n", var+1, val);
						#endif
					/***/
					}
				}
			}

		} /* if (var_state[var] == LIVE) */
	} /* for (var=0; var<NUM_VARS; var++) */

	chosen_var = pick_variable();
	if (chosen_var == NONE)
		return;

	lit_state_var = lit_state[chosen_var];
	num_2clauses_wv_wv_var = num_2clauses_with_var_with_val[chosen_var];
	num_3clauses_wv_wv_var = num_3clauses_with_var_with_val[chosen_var];

	y_vals_cnt = 0;
	for (val=0; val<DOMAIN_SIZE; val++)
	{
		if (lit_state_var[val] == LIVE)
			if ((num_2clauses_wv_wv_var[val] + num_3clauses_wv_wv_var[val]) != 0)
				y_vals[y_vals_cnt++] = val;
	}
	chosen_val = y_vals[0];

	saved_clause_stack[chosen_var] = CLAUSE_STACK_fill_pointer;
	saved_managedclause_stack[chosen_var] = MANAGEDCLAUSE_STACK_fill_pointer;
	saved_restrictedlit_stack[chosen_var] = RESTRICTEDLIT_STACK_fill_pointer;
	saved_removedlit_stack[chosen_var] = REMOVEDLIT_STACK_fill_pointer;

	var_state[chosen_var] = DEAD;
	push(chosen_var, VARIABLE_STACK);
	var_current_value[chosen_var] = chosen_val;
	var_rest_value_chosen_var = var_rest_value[chosen_var];
	for (i=1; i<y_vals_cnt; i++)
		var_rest_value_chosen_var[i-1] = y_vals[i];
	var_rest_value_chosen_var[i-1] = NONE;

	/* remove variables */
	lp_ptr = lits_with_var_without_val[chosen_var][chosen_val];
	for (lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr))
	{
		c = lp->clause;
		if (clause_state[c] == LIVE && lp->state == LIVE)
		{
			switch (clause_length[c])
			{
				case 2:
					clause_length[c]--;
					push(c, UNITCLAUSE_STACK);
					break;
				default:
					clause_length[c]--;
					push(c, MANAGEDCLAUSE_STACK);
			}
		}
	}

	/* remove clauses */
	lp_ptr = lits_with_var_with_val[chosen_var][chosen_val];
	for (lp=*lp_ptr; lp!=NULL; lp=*(++lp_ptr))
	{
		c = lp->clause;
		/* assert(lp->state == LIVE);	must be the case because lit contains val */
		if (clause_state[c] == LIVE)
		{
			clause_state[c] = DEAD;
			push(c, CLAUSE_STACK);
		}
	}

	NUM_BRANCH++;
/***/
	#ifdef verbose
	printf("Branch: %d -> %d\n", chosen_var+1, chosen_val);
	#ifdef print_tree
	print_formula();
	#endif
	#endif
/***/
}
/* ---------------------------------------------------------------------------------- */
/* ---------------------------------------------------------------------------------- */
/* ---------------------------------------------------------------------------------- */


int build_simple_sat_instance(char *input_file)
/* called once in main */
{
	FILE *ifp = fopen(input_file, "r");
	char ch;
	int i, j, k, c_length, l_length, *lit_size, longest_clause = 0,
		*num_with_var, **num_with_var_with_val, **num_with_var_without_val,
		var, val, *val_ptr;
	lit *lits, *lit_ptr;

	if (ifp == NULL)
		return FALSE;
	fscanf(ifp, "%c", &ch);
	while (ch != 'n')
	{
		while (ch != '\n')
			fscanf(ifp, "%c", &ch);
		fscanf(ifp, "%c", &ch);
	}

	if (fscanf(ifp, "b cnf%d%d%d", &NUM_VARS, &NUM_CLAUSES, &DOMAIN_SIZE) != 3)
		return FALSE;

	/* allocate space for the data structures */
	sat = (lit **) malloc(NUM_CLAUSES * sizeof(lit *));
	lits_with_var = (lit ***) malloc(NUM_VARS * sizeof(lit **));
	lits_with_var_with_val = (lit ****) malloc(NUM_VARS * sizeof(lit ***));
	lits_with_var_without_val = (lit ****) malloc(NUM_VARS * sizeof(lit ***));

	clause_state = (S_char *) malloc(NUM_CLAUSES * sizeof(S_char));
	clause_length = (U_char *) malloc(NUM_CLAUSES * sizeof(U_char));

	var_state = (S_char *) malloc(NUM_VARS * sizeof(S_char));
	var_current_value = (S_char *) malloc(NUM_VARS * sizeof(S_char));
	var_rest_value = (S_char **) malloc(NUM_VARS * sizeof(S_char *));
	lit_state = (S_char **) malloc(NUM_VARS * sizeof(S_char *));

	num_2clauses_with_var_with_val = (int **) malloc(NUM_VARS * sizeof(int *));
	num_3clauses_with_var_with_val = (int **) malloc(NUM_VARS * sizeof(int *));
	clause_flags = (int *) malloc(NUM_CLAUSES * sizeof(int));
	reduce_num = (int **) malloc(NUM_VARS * sizeof(int *));

	saved_clause_stack = (int *) malloc(NUM_VARS * sizeof(int));
	saved_managedclause_stack = (int *) malloc(NUM_VARS * sizeof(int));
	saved_restrictedlit_stack = (int *) malloc(NUM_VARS * sizeof(int));
	saved_removedlit_stack = (int *) malloc(NUM_VARS * sizeof(int));

	tmp_vals = (int *) malloc(DOMAIN_SIZE * sizeof(int));
	y_vals = (int *) malloc(DOMAIN_SIZE * sizeof(int));
	n_vals = (int *) malloc(DOMAIN_SIZE * sizeof(int));

	num_with_var = (int *) malloc(NUM_VARS * sizeof(int));
	num_with_var_with_val = (int **) malloc(NUM_VARS * sizeof(int *));
	num_with_var_without_val = (int **) malloc(NUM_VARS * sizeof(int *));
	lits = (lit *) malloc(NUM_VARS * sizeof(lit));
	lit_size = (int *) malloc(NUM_VARS * sizeof(int));

	for (j=0; j<NUM_VARS; j++)
	{
		lits_with_var_with_val[j] = (lit ***) malloc(DOMAIN_SIZE * sizeof(lit **));
		lits_with_var_without_val[j] = (lit ***) malloc(DOMAIN_SIZE * sizeof(lit **));
		var_rest_value[j] = (S_char *) malloc((DOMAIN_SIZE+1) * sizeof(S_char));
		lit_state[j] = (S_char *) malloc(DOMAIN_SIZE * sizeof(S_char));
		num_2clauses_with_var_with_val[j] = (int *) malloc(DOMAIN_SIZE * sizeof(int));
		num_3clauses_with_var_with_val[j] = (int *) malloc(DOMAIN_SIZE * sizeof(int));
		reduce_num[j] = (int *) malloc(DOMAIN_SIZE * sizeof(int));

		num_with_var_with_val[j] = (int *) malloc(DOMAIN_SIZE * sizeof(int));
		num_with_var_without_val[j] = (int *) malloc(DOMAIN_SIZE * sizeof(int));
		lits[j].dom = (int *) malloc(DOMAIN_SIZE * sizeof(int));

		num_with_var[j] = 0;
		for (k=0; k<DOMAIN_SIZE; k++)
		{
			num_with_var_with_val[j][k] = 0;
			num_with_var_without_val[j][k] = 0;
		}
	}

	/* allocate space for the unit clause stack */
	UNITCLAUSE_STACK = (int *) malloc(NUM_CLAUSES * sizeof(int));

	/* read in the next clause from the input */
	for (i=0; i<NUM_CLAUSES; i++)
	{
		c_length = 0;
		fscanf(ifp, "%d", &lits[c_length].var);
		fscanf(ifp, "{%d%c", &lits[c_length].dom[l_length=0], &ch);
		while (ch != '}')
			fscanf(ifp, "%d%c", &lits[c_length].dom[++l_length], &ch);
		lit_size[c_length] = l_length + 1;
		do
		{
			c_length++;
			fscanf(ifp, "%d", &lits[c_length].var);
			if (lits[c_length].var != 0)
			{
				fscanf(ifp, "{%d%c", &lits[c_length].dom[l_length=0], &ch);
				while (ch != '}')
					fscanf(ifp, "%d%c", &lits[c_length].dom[++l_length], &ch);
				lit_size[c_length] = l_length + 1;
			}
		} while (lits[c_length].var != 0);
		if (c_length > longest_clause)
			longest_clause = c_length;

		/* allocate sat[i] and copy the read-in clause */
		sat[i] = (lit *) malloc((c_length+1) * sizeof(lit));
		for (j=0; j<c_length; j++)
		{
			sat[i][j].dom = (int *) malloc((lit_size[j]+1) * sizeof(int));

			var = lits[j].var-1;
			sat[i][j].var = var;
			for (k=0; k<DOMAIN_SIZE; k++)
				tmp_vals[k] = FALSE;
			for (k=0; k<lit_size[j]; k++)
			{
				val = lits[j].dom[k];
				sat[i][j].dom[k] = val;
				tmp_vals[val] = TRUE;
			}
			sat[i][j].dom[lit_size[j]] = NONE;
			sat[i][j].state = LIVE;
			sat[i][j].clause = i;

			num_with_var[var]++;
			for (k=0; k<DOMAIN_SIZE; k++)
			{
				if (tmp_vals[k] == TRUE)
					num_with_var_with_val[var][k]++;
				else
					num_with_var_without_val[var][k]++;
			}
		}
		sat[i][c_length].var = NONE;
		clause_length[i] = c_length;
		clause_state[i] = LIVE;

		if (c_length==1)
			push(i, UNITCLAUSE_STACK);
	}
	fclose(ifp);

	/* set the size of lits_with_var_with_val[var][dom]
		and lits_with_var_without_val[var][dom] */
	for (j=0; j<NUM_VARS; j++)
	{
		lits_with_var[j] = (lit **) malloc((num_with_var[j]+1) * sizeof(lit *));
		lits_with_var[j][num_with_var[j]] = NULL;
		num_with_var[j] = 0;
		for (k=0; k<DOMAIN_SIZE; k++)
		{
			lits_with_var_with_val[j][k] =
					(lit **) malloc((num_with_var_with_val[j][k]+1) * sizeof(lit *));
			lits_with_var_without_val[j][k] =
					(lit **) malloc((num_with_var_without_val[j][k]+1) * sizeof(lit *));
			lits_with_var_with_val[j][k][num_with_var_with_val[j][k]] = NULL;
			lits_with_var_without_val[j][k][num_with_var_without_val[j][k]] = NULL;
			num_with_var_with_val[j][k] = 0;
			num_with_var_without_val[j][k] = 0;
			lit_state[j][k] = LIVE;
		}
		var_state[j] = LIVE;
	}

	/* copy the values into lits_with_var_with<out>_val[var][dom][] */
	for (i=0; i<NUM_CLAUSES; i++)
	{
		for (lit_ptr=sat[i]; lit_ptr->var!=NONE; lit_ptr++)
		{
			var = lit_ptr->var;
			for (k=0; k<DOMAIN_SIZE; k++)
				tmp_vals[k] = FALSE;
			for (val_ptr=lit_ptr->dom; *val_ptr!=NONE; val_ptr++)
				tmp_vals[*val_ptr] = TRUE;

			lits_with_var[var][num_with_var[var]++] = lit_ptr;
			for (k=0; k<DOMAIN_SIZE; k++)
			{
				if (tmp_vals[k] == TRUE)
					lits_with_var_with_val[var][k][num_with_var_with_val[var][k]++] = lit_ptr;
				else
					lits_with_var_without_val[var][k][num_with_var_without_val[var][k]++] = lit_ptr;
			}
		}
	}

	/* allocate space for the rest of the stacks */
	VARIABLE_STACK = (int *) malloc(NUM_VARS * sizeof(int));
	CLAUSE_STACK = (int *) malloc(NUM_CLAUSES * sizeof(int));
	MANAGEDCLAUSE_STACK = (int *) malloc(NUM_CLAUSES * longest_clause * sizeof(int));
	RESTRICTEDLIT_STACK = (var_val *) malloc(NUM_VARS * DOMAIN_SIZE * sizeof(var_val));
	REMOVEDLIT_STACK = (lit **) malloc(NUM_CLAUSES * longest_clause * sizeof(lit *));

	LA_VARIABLE_STACK = (int *) malloc(NUM_VARS * sizeof(int));
	LA_MANAGEDCLAUSE_STACK = (int *) malloc(NUM_CLAUSES * longest_clause * sizeof(int));
	LA_UNITCLAUSE_STACK = (int *) malloc(NUM_CLAUSES * sizeof(int));
	LA_RESTRICTEDLIT_STACK = (var_val *) malloc(NUM_VARS * DOMAIN_SIZE * sizeof(var_val));
	LA_REMOVEDLIT_STACK = (lit **) malloc(NUM_CLAUSES * longest_clause * sizeof(lit *));
	TESTED_VAR_STACK = (int *) malloc(NUM_VARS * sizeof(int));

	/* free the space allocated locally to this function */
	for (j=0; j<NUM_VARS; j++)
	{
		free(num_with_var_with_val[j]);
		free(num_with_var_without_val[j]);
		free(lits[j].dom);
	}
	free(num_with_var);
	free(num_with_var_with_val);
	free(num_with_var_without_val);
	free(lits);
	free(lit_size);

	return TRUE;
}

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


void free_resources(void)
/* called once in main */
{
	int i, j, k;

	for (i=0; i<NUM_CLAUSES; i++)
	{
		for (j=0; sat[i][j].var!=NONE; j++)
			free(sat[i][j].dom);
		free(sat[i]);
	}
	free(sat);

	for (j=0; j<NUM_VARS; j++)
	{
		for (k=0; k<DOMAIN_SIZE; k++)
		{
			free(lits_with_var_with_val[j][k]);
			free(lits_with_var_without_val[j][k]);
		}
		free(lits_with_var[j]);
		free(lits_with_var_with_val[j]);
		free(lits_with_var_without_val[j]);
		free(var_rest_value[j]);
		free(lit_state[j]);
		free(num_2clauses_with_var_with_val[j]);
		free(num_3clauses_with_var_with_val[j]);
	}

	free(lits_with_var);
	free(lits_with_var_with_val);
 	free(lits_with_var_without_val);

	free(clause_state);
	free(clause_length);

	free(var_state);
	free(var_current_value);
	free(var_rest_value);
	free(lit_state);

	free(num_2clauses_with_var_with_val);
	free(num_3clauses_with_var_with_val);
	free(clause_flags);

	free(saved_clause_stack);
	free(saved_managedclause_stack);
	free(saved_restrictedlit_stack);
	free(saved_removedlit_stack);

	free(VARIABLE_STACK);
	free(CLAUSE_STACK);
	free(MANAGEDCLAUSE_STACK);
	free(UNITCLAUSE_STACK);
	free(RESTRICTEDLIT_STACK);
	free(REMOVEDLIT_STACK);

	free(LA_VARIABLE_STACK);
	free(LA_MANAGEDCLAUSE_STACK);
	free(LA_UNITCLAUSE_STACK);
	free(LA_RESTRICTEDLIT_STACK);
	free(LA_REMOVEDLIT_STACK);
	free(TESTED_VAR_STACK);

	free(tmp_vals);
	free(y_vals);
	free(n_vals);
}

int verify_solution(void)
/* called once in main */
{
	int i, var, val, *val_ptr, clause_truth;
	lit *lit_ptr;

	for (i=0; i<NUM_CLAUSES; i++)
	{
		clause_truth = FALSE;
		lit_ptr = sat[i];
		for (var=lit_ptr->var; var!=NONE; var=(++lit_ptr)->var)
		{
			if (var_current_value[var] == NONE || var_state[var] == LIVE)
			{
				clause_truth = TRUE;
				break;
			}

			val_ptr = lit_ptr->dom;
			for (val=*val_ptr; val!=NONE; val=*(++val_ptr))
			{
				if (val == var_current_value[var])
				{
					clause_truth = TRUE;
					break;
				}
			}
			if (clause_truth == TRUE)
				break;
		}
		if (clause_truth == FALSE)
			return FALSE;
	}

	return TRUE;
}

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

	printf("Variable asignments:");
	for (i=0; i<NUM_VARS; i++)
	{
		if (var_current_value[i] == NONE || var_state[i] == LIVE)
		{
			if (i%10 == 0)
			{
				printf("\n");
				printf("%3d{-}", i+1);
			}
			else
				printf("\t%3d{-}", i+1);
		}
		else
		{
			if (i%10 == 0)
			{
				printf("\n");
				printf("%3d{%d}", i+1, var_current_value[i]);
			}
			else
				printf("\t%3d{%d}", i+1, var_current_value[i]);
		}
	}
	printf("\n");
}
/* ---------------------------------------------------------------------------------- */

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

	if (argc < 2 || argc > 3)
	{
		printf("Usage:\tNB-satz [-q -v] input_file\n");
		printf("  output format:\n");
		printf("sat      time     branch   back\n");
		printf("unit     s_unit   pure     s_pure\n");
		printf("examined failed   la_unit  la_pure\n");
		return -1;
	}

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

	if (argc == 2)
	{
		if (build_simple_sat_instance(argv[1]) == FALSE)
		{
			printf("Input file error\n");
			return -1;
		}
	}
	else if (argc == 3)
	{
		if (strcmp(argv[1], "-q") == 0)
			quiet = 0;
		else if (strcmp(argv[1], "-v") == 0)
			quiet = 2;
		else
		{
			printf("Usage:\tNB-satz [-q -v] input_file\n");
			return -1;
		}

		if (build_simple_sat_instance(argv[2]) == FALSE)
		{
			printf("Input file error\n");
			return -1;
		}
	}
	else
		return -1;

/***/
	#ifdef print_tree
	print_formula();
	#endif
/***/
	do
	{
		if (UNITCLAUSE_STACK_fill_pointer == 0)
			branch();
		unitclause_process();
	} while ((VARIABLE_STACK_fill_pointer != 0) && (!(satisfiable())));

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


	if (quiet == 0)
	{
		if (satisfiable())
		{
			if (verify_solution())
				return_value = 1;
			else
				return_value = -1;
		}
		else
			return_value = 0;
	}
	else if (quiet == 1)
	{
		if (satisfiable())
		{
			if (verify_solution())
				return_value = 1;
			else
				return_value = -1;
		}
		else
			return_value = 0;

		/* sat      time     branch   back
			 unit     s_unit   pure     s_pure
			 examined failed   la_unit  la_pure */
		printf("%d %5.3f %d %d %d %d %d %d %d %d %d %d\n",
				return_value, (double)(endtime-begintime)/CLK_TCK,
				NUM_BRANCH, NUM_BACK,
				NUM_UNIT, NUM_SEMIUNIT, NUM_PURE, NUM_SEMIPURE,
				NUM_EXAMINED, NUM_FAILED, NUM_LA_UNIT, NUM_LA_SEMIUNIT);
	}
	else if (quiet == 2)
	{
		if (satisfiable())
		{
			printf("#yes\n");
			printf("**** the instance is satisfiable ****\n");

			if (verify_solution())
			{
				printf("**** verification of solution is OK ****\n");
				return_value = 1;
			}
			else
			{
				printf("**** program error - verification failed ****\n");
				return_value = -1;
			}

			print_values();
		}
		else
		{
			printf("#no\n");
			printf("**** the instance is unsatisfiable ****\n");
			return_value = 0;
		}

		printf("Unit:%ld Semi-unit:%ld  Pure:%ld Semi-pure:%ld  Branch:%ld Back:%ld\n",
				NUM_UNIT, NUM_SEMIUNIT, NUM_PURE, NUM_SEMIPURE, NUM_BRANCH, NUM_BACK);
		printf("Lookahead:%ld  Failed lits:%ld    LA Unit:%ld  LA Semi-unit:%ld\n",
				NUM_EXAMINED, NUM_FAILED, NUM_LA_UNIT, NUM_LA_SEMIUNIT);

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

	free_resources();

	return return_value;
}