/****************************************************************************/
/* g2wsat has participated in SAT2005 competition and has won a Silver Medal*/
/* in satisfiable random formula category. The current version is optimized */
/* after the competition and generally more than 50% faster                 */
/*                                                                          */
/*                  Author: Chu Min LI (chu-min.li@u-picardie.fr)           */
/*                  Copyright LaRIA, Universite de Picardie Jules Verne     */
/*                  Sept. 2005                                              */
/****************************************************************************/

/* Reference

Chu Min LI & Wenqi HUANG, "Diversification and Determinism in Local search
for Satisfiability", in proceedings of 8th international conference, SAT2005,
LNCS 3569 Springer, St Andrews, UK, June 2005, Pages 158-172
*/

/*
Use 

gcc -O3 g2wsat2005.c -o g2wsat2005 

to compile the file in a Unix computer

Use the command "g2wsat2005 -help" or "g2wsat2005" to see argument list
*/ 

#include <stdio.h>
#include <stdlib.h>
#include <sys/time.h>
#include <time.h>

#include <sys/times.h>
#include <sys/types.h>
#include <limits.h>

typedef signed int my_type;
typedef unsigned int my_unsigned_type;

#define WORD_LENGTH 100 
#define TRUE 1
#define FALSE 0
#define NONE -1
#define SATISFIABLE 2
#define walk_satisfiable() (MY_CLAUSE_STACK_fill_pointer == 0)

#define WEIGTH 4
#define T 10

/* 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  100000
#define tab_clause_size 500000
#define tab_unitclause_size \
 ((tab_clause_size/4<2000) ? 2000 : tab_clause_size/4)
#define my_tab_variable_size \
 ((tab_variable_size/2<1000) ? 1000 : tab_variable_size/2)
#define my_tab_clause_size \
 ((tab_clause_size/2<2000) ? 2000 : tab_clause_size/2)
#define my_tab_unitclause_size \
 ((tab_unitclause_size/2<1000) ? 1000 : tab_unitclause_size/2)
#define tab_literal_size 2*tab_variable_size
#define double_tab_clause_size 2*tab_clause_size
#define positive(literal) literal<NB_VAR
#define negative(literal) literal>=NB_VAR
#define get_var_from_lit(negative_literal) negative_literal-NB_VAR
#define RESOLVANT_LENGTH 3
#define RESOLVANT_SEARCH_THRESHOLD 5000
#define complement(lit1, lit2) \
 ((lit1<lit2) ? lit2-lit1 == NB_VAR : lit1-lit2 == NB_VAR)

#define inverse_signe(signe) \
 (signe == POSITIVE) ? NEGATIVE : POSITIVE
#define unsat(val) (val==0)?"UNS":"SAT"
#define pop(stack) stack[--stack ## _fill_pointer]
#define push(item, stack) stack[stack ## _fill_pointer++] = item
#define satisfiable() CLAUSE_STACK_fill_pointer == NB_CLAUSE

#define NEGATIVE 0
#define POSITIVE 1
#define PASSIVE 0
#define ACTIVE 1
#define INUTILE 2
#define MAX_NODE_NUMBER 6000
struct node {
  int clause;
  struct node *next;
};

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

int CLAUSE_NODES_pointer=MAX_NODE_NUMBER;

struct node *CLAUSE_NODES;
struct ressource *ressources=NULL;

struct node *allocate_node() {
  struct ressource *pressource;
  if (CLAUSE_NODES_pointer == MAX_NODE_NUMBER) {
    CLAUSE_NODES = (struct node *)malloc(MAX_NODE_NUMBER * sizeof(struct node));
    CLAUSE_NODES_pointer = 0;
    pressource= (struct ressource *)malloc(sizeof (struct ressource));
    pressource->next = ressources;
    ressources=pressource;
    pressource->pnode = CLAUSE_NODES;
  }  
  return &(CLAUSE_NODES[CLAUSE_NODES_pointer++]);
}

void free_ressources() {
  struct ressource *pressource;
  while (ressources != NULL) {
    free(ressources->pnode);
    pressource = ressources;
    ressources = ressources->next;
    free(pressource);
  }
}

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

int *neg_in[tab_variable_size];
int *pos_in[tab_variable_size];
int neg_nb[tab_variable_size];
int pos_nb[tab_variable_size];
my_type var_current_value[tab_variable_size];
my_type var_rest_value[tab_variable_size];
my_type var_state[tab_variable_size];

int saved_clause_stack[tab_variable_size];
int saved_managedclause_stack[tab_variable_size];
my_unsigned_type nb_neg_clause_of_length2[tab_variable_size];
my_unsigned_type nb_neg_clause_of_length3[tab_variable_size];
my_unsigned_type nb_pos_clause_of_length2[tab_variable_size];
my_unsigned_type nb_pos_clause_of_length3[tab_variable_size];

float reduce_if_negative_nb[tab_variable_size];
float reduce_if_positive_nb[tab_variable_size];

int *sat[tab_clause_size];
int *var_sign[tab_clause_size];
my_type clause_state[tab_clause_size];
my_type clause_length[tab_clause_size];

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


int VARIABLE_STACK[tab_variable_size];
int CLAUSE_STACK[tab_clause_size];
int UNITCLAUSE_STACK[tab_unitclause_size];
int MANAGEDCLAUSE_STACK[tab_clause_size];
int TESTED_VAR_STACK[tab_variable_size];
int TESTED_VAR_STACK_fill_pointer=0;


int tab_variable_nb_unit[2*tab_variable_size]={0};
int clause_possible[tab_clause_size]={0};
int SAVED_VAR_VARIABLE_STACK[tab_variable_size];
int SAVED_VAR_VARIABLE_STACK_fill_pointer = 0;
int SAVED_DEB_CLAUSE_STACK[tab_variable_size];
int SAVED_DEB_CLAUSE_STACK_fill_pointer;
int SAVED_FIN_CLAUSE_STACK[tab_variable_size];
int SAVED_FIN_CLAUSE_STACK_fill_pointer;
int SAVED_VARIABLE_STACK[tab_variable_size];
int SAVED_VARIABLE_STACK_fill_pointer = 0;
int SAVED_MANAGEDCLAUSE_STACK[tab_clause_size];
int SAVED_MANAGEDCLAUSE_STACK_fill_pointer = 0;
int SAVED_CLAUSE_STACK[tab_clause_size];
int SAVED_CLAUSE_STACK_fill_pointer = 0;
int PREVIOUS_MANAGEDCLAUSE_STACK_fill_pointer = 0;

int CLAUSE_VAR_SUBSUME[tab_clause_size];
int SUBSUMECLAUSE_STACK[tab_clause_size];
int SUBSUMECLAUSE_STACK_fill_pointer=0;
int saved_subsumeclause_stack[tab_variable_size] = {0};
int CPT=0;

int NB_VAR;
int NB_ACTIVE_VAR;
int NB_CLAUSE;
int INIT_NB_CLAUSE;
my_type R = 3;

long NB_UNIT=1, NB_MONO=0, NB_BRANCHE=0, NB_BACK = 0;

#define double_tab_clause_size 2*tab_clause_size

struct var_node {
  int var;
  int weight;
  struct var_node *next;
};

#define VAR_NODES1_nb 6
int VAR_NODES1_index=0;
struct var_node VAR_NODES1[10*VAR_NODES1_nb];
struct var_node *VAR_FOR_TEST1=NULL;

struct var_node *allocate_var_node1() {
  return &VAR_NODES1[VAR_NODES1_index++];
}

int test_flag[tab_variable_size];

int MAX_REDUCED;
int T_SEUIL;

int SEED, SEED_FLAG=FALSE, BUILD_FLAG=TRUE;
char saved_input_file[WORD_LENGTH];
char *INPUT_FILE;

unsigned long IMPLIED_LIT_FLAG=0;
int IMPLIED_LIT_STACK_fill_pointer=0;
int IMPLIED_LIT_STACK[tab_variable_size];
unsigned long LIT_IMPLIED[tab_variable_size]={0};

long NB_SECOND_SEARCH=0;
long NB_SECOND_FIXED = 0;

void remove_clauses(int var) {
  register int clause;
  register int *clauses;
  if (var_current_value[var] == POSITIVE) clauses = pos_in[var];
  else clauses = neg_in[var];
  for(clause=*clauses; clause!=NONE; clause=*(++clauses)) {
    if (clause_state[clause] == ACTIVE) {
      clause_state[clause] = PASSIVE;
      push(clause, CLAUSE_STACK);
    }
  }
}

int manage_clauses(int var) {
  register int clause;
  register int *clauses;
  if (var_current_value[var] == POSITIVE) clauses = neg_in[var];
  else clauses = pos_in[var];
  for(clause=*clauses; clause!=NONE; clause=*(++clauses)) {
    if (clause_state[clause] == ACTIVE) {
      switch (clause_length[clause]) {
      case 1: return FALSE;
      case 2: push(clause, UNITCLAUSE_STACK);
	push(clause, MANAGEDCLAUSE_STACK);
	clause_length[clause]--; break;
      default: clause_possible[clause] = 1;
	clause_length[clause]--;
	push(clause, MANAGEDCLAUSE_STACK);
      }
    }
  }
  return TRUE;
}

int manage1_clauses(int var) {
  register int clause;
  register int *clauses;
  if (var_current_value[var] == POSITIVE) clauses = neg_in[var];
  else clauses = pos_in[var];
  for(clause=*clauses; clause!=NONE; clause=*(++clauses)) {
    if (clause_state[clause] == ACTIVE) {
      switch (clause_length[clause]) {
      case 1: return FALSE;
      case 2: push(clause, UNITCLAUSE_STACK);
	push(clause, MANAGEDCLAUSE_STACK);
	clause_length[clause]--; break;
      default: clause_length[clause]--;
	push(clause, MANAGEDCLAUSE_STACK);
      }
    }
  }
  return TRUE;
}

void simple_manage_clauses(int var) {
  register int clause;
  register int *clauses;
  if (var_current_value[var] == POSITIVE) clauses = neg_in[var];
  else clauses = pos_in[var];
  for(clause=*clauses; clause!=NONE; clause=*(++clauses)) { 
    if (clause_state[clause] == ACTIVE) {
      switch (clause_length[clause]) {
      case 2: push(clause, UNITCLAUSE_STACK);
	push(clause, MANAGEDCLAUSE_STACK);
	clause_length[clause]--; break;
      default: clause_length[clause]--;
	clause_possible[clause] = 1;
	push(clause, MANAGEDCLAUSE_STACK);
      }
    }
  }
}

void simple1_manage_clauses(int var) {
  register int clause;
  register int *clauses;
  if (var_current_value[var] == POSITIVE) clauses = neg_in[var];
  else clauses = pos_in[var];
  for(clause=*clauses; clause!=NONE; clause=*(++clauses)) { 
    if (clause_state[clause] == ACTIVE) {
      switch (clause_length[clause]) {
      case 2: push(clause, UNITCLAUSE_STACK);
	push(clause, MANAGEDCLAUSE_STACK);
	clause_length[clause]--; break;
      default: clause_length[clause]--;
	push(clause, MANAGEDCLAUSE_STACK);
      }
    }
  }
}


void my_simple_manage_clauses(int var) {
  register int clause;
  register int *clauses;
  if (var_current_value[var] == POSITIVE) clauses = neg_in[var];
  else clauses = pos_in[var];
  for(clause=*clauses; clause!=NONE; clause=*(++clauses)) { 
    if (clause_state[clause] == ACTIVE) { 
      switch (clause_length[clause]) {
      case 2: push(clause, UNITCLAUSE_STACK);
	clause_length[clause]--; break;
      default: clause_length[clause]--;
 	push(clause, MANAGEDCLAUSE_STACK);
      }
    }
  }
}

int my_manage_clauses(int var) {
  register int clause;
  register int *clauses;
  if (var_current_value[var] == POSITIVE) clauses = neg_in[var];
  else clauses = pos_in[var];
  for(clause=*clauses; clause!=NONE; clause=*(++clauses)) {
    if (clause_state[clause] == ACTIVE ){ 
      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 print_values(int nb_var) {
  FILE* fp_out;
  int i;
  fp_out = fopen("satx.sol", "w");
  for (i=0; i<nb_var; i++) {
    if (var_current_value[i] == 1) 
      fprintf(fp_out, "%d ", i+1);
    else
      fprintf(fp_out, "%d ", 0-i-1);
  }
  fprintf(fp_out, "\n");
  fclose(fp_out);			
} 

int backtracking() {
  int var, index,clause;
      
  UNITCLAUSE_STACK_fill_pointer = 0;
  NB_BACK++;

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

      for (index = saved_managedclause_stack[var];
	   index < MANAGEDCLAUSE_STACK_fill_pointer;
	   index++) {	
	clause = MANAGEDCLAUSE_STACK[index];
	clause_length[MANAGEDCLAUSE_STACK[index]]++;
	if (clause_length[clause]==2 )
	  clause_possible[clause] = 1;
	else
	  clause_possible[clause] = 0;
      }
      MANAGEDCLAUSE_STACK_fill_pointer = saved_managedclause_stack[var];

      PREVIOUS_MANAGEDCLAUSE_STACK_fill_pointer = MANAGEDCLAUSE_STACK_fill_pointer ;
      //      printf("Back %d\n",var);
      var_current_value[var] = var_rest_value[var];
      var_rest_value[var] = NONE;
      push(var, VARIABLE_STACK);
      simple_manage_clauses(var);
      remove_clauses(var);

      return TRUE;
    }
  } while (VARIABLE_STACK_fill_pointer != 0);
  return FALSE;
}

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

int smaller_than(int lit1, int lit2) {
  return ((lit1<NB_VAR) ? lit1 : lit1-NB_VAR) < 
    ((lit2<NB_VAR) ? lit2 : lit2-NB_VAR);
}

my_type redundant(int *new_clause, int *old_clause) {
  int lit1, lit2, old_clause_diff=0, new_clause_diff=0;
    
  lit1=*old_clause; lit2=*new_clause;
  while ((lit1 != NONE) && (lit2 != NONE)) {
    if (smaller_than(lit1, lit2)) {
      lit1=*(++old_clause); old_clause_diff++;
    }
    else
      if (smaller_than(lit2, lit1)) {
	lit2=*(++new_clause); new_clause_diff++;
      }
      else
	if (complement(lit1, lit2)) {
	  return FALSE; /* old_clause_diff++; new_clause_diff++; j1++; j2++; */
	}
	else {
          lit1=*(++old_clause);  lit2=*(++new_clause);
	}
  }
  if ((lit1 == NONE) && (old_clause_diff == 0))
    /* la nouvelle clause est redondante ou subsumee */
    return NEW_CLAUSE_REDUNDANT;
  if ((lit2 == NONE) && (new_clause_diff == 0))
    /* la old clause est redondante ou subsumee */
    return OLD_CLAUSE_REDUNDANT;
  return FALSE;
}

void remove_passive_clauses() {
  int  clause, put_in, first=NONE;
  for (clause=0; clause<NB_CLAUSE; clause++) {
    if (clause_state[clause]==PASSIVE) {
      first=clause; break;
    }
  }
  if (first!=NONE) {
    put_in=first;
    for(clause=first+1; clause<NB_CLAUSE; clause++) {
      if (clause_state[clause]==ACTIVE) {
	sat[put_in]=sat[clause]; var_sign[put_in]=var_sign[clause];
	clause_state[put_in]=ACTIVE; 
	clause_length[put_in]=clause_length[clause];
	put_in++;
      }
    }
    NB_CLAUSE=put_in;
  }
}

void remove_passive_vars_in_clause(int clause) {
  int *vars_signs, *vars_signs1, var, var1, first=NONE;
  vars_signs=var_sign[clause];
  for(var=*vars_signs; var!=NONE; var=*(vars_signs+=2)) {
    if (var_state[var]!=ACTIVE) {
      first=var; break;
    }
  }
  if (first!=NONE) {
    for(vars_signs1=vars_signs+2, var1=*vars_signs1; var1!=NONE; 
	var1=*(vars_signs1+=2)) {
      if (var_state[var1]==ACTIVE) {
	*vars_signs=var1; *(vars_signs+1) = *(vars_signs1+1);
	vars_signs+=2;
      }
    }
    *vars_signs=NONE;
  }
}

int clean_structure() {
  int clause, var, *vars_signs;
  remove_passive_clauses();
  if (NB_CLAUSE==0) return FALSE;
  for (clause=0; clause<NB_CLAUSE; clause++) 
    remove_passive_vars_in_clause(clause);
  NB_ACTIVE_VAR=0;
  for (var=0; var<NB_VAR; var++) { 
    neg_nb[var] = 0;
    pos_nb[var] = 0;
    if (var_state[var]==ACTIVE) NB_ACTIVE_VAR++;
  }
  for (clause=0; clause<NB_CLAUSE; clause++) {
    vars_signs=var_sign[clause];
    for(var=*vars_signs; var!=NONE; var=*(vars_signs+=2)) {
      if (*(vars_signs+1)==POSITIVE) 
	pos_in[var][pos_nb[var]++]=clause;
      else  neg_in[var][neg_nb[var]++]=clause;
    }
  }
  for (var=0; var<NB_VAR; var++) { 
    neg_in[var][neg_nb[var]]=NONE;
    pos_in[var][pos_nb[var]]=NONE;
  }
  return TRUE;
}

int unitclause_process();
int simplify_formula();

void lire_clauses(FILE *fp_in) {
  int i, j, jj, ii, length, tautologie, lits[1000], lit, lit1;
  for (i=0; i<NB_CLAUSE; i++) {
    length=0; 
    fscanf(fp_in, "%d", &lits[length]);
    while (lits[length] != 0) {
      length++;
      fscanf(fp_in, "%d", &lits[length]);
    }
    tautologie = 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])) {
	  lit1=lits[jj]; lits[jj]=lit; lit=lit1;
	}
	else
	  if (lit == lits[jj]) {
	    lits[jj] = lits[length-1]; 
	    jj--; length--; lits[length] = 0;
	    printf("literal %d is redundant in clause %d \n", lit, i+1);
	  }
	  else
            if (abs(lit) == abs(lits[jj])) {
	      tautologie = TRUE; break;
            }
      }
      if (tautologie == TRUE) break;
      else lits[ii] = lit;
    }
    if (tautologie == FALSE) {
      sat[i]= (int *)malloc((length+1) * sizeof(int));
      for (j=0; j<length; j++) {
	if (lits[j] < 0) 
	  sat[i][j] = abs(lits[j]) - 1 + NB_VAR ;
	else 
	  sat[i][j] = lits[j]-1;
      }
      sat[i][length]=NONE;
      clause_length[i]=length;
      clause_state[i] = ACTIVE;
    }
    else { i--; NB_CLAUSE--;}
  }
}

void build_structure() {
  int i, j, var, *lits1, length, clause, *vars_signs, lit;
  for (i=0; i<NB_VAR; i++) { 
    neg_nb[i] = 0; pos_nb[i] = 0;
  }
  for (i=0; i<NB_CLAUSE; i++) {
    for(j=0; j<clause_length[i]; j++) {
      if (sat[i][j]>=NB_VAR) {
	var=sat[i][j]-NB_VAR; neg_nb[var]++;
      }
      else {
	var=sat[i][j]; pos_nb[var]++;
      }
    }
    if (sat[i][clause_length[i]] !=NONE)
      printf("erreur ");
  }
  for(clause=0;clause<NB_CLAUSE;clause++) {
    length = clause_length[clause];
    var_sign[clause] = (int *)malloc((2*length+1)*sizeof(int));
    lits1 = sat[clause]; vars_signs = var_sign[clause];
    for(lit=*lits1; lit!=NONE; lit=*(++lits1),(vars_signs+=2)) {
      if (negative(lit)) {
	*(vars_signs+1)= NEGATIVE;
	*vars_signs = get_var_from_lit(lit);
      }
      else {
	*(vars_signs+1)=POSITIVE;
	*vars_signs = lit;
      }
    }
    *vars_signs = NONE;  
  }
  for (i=0; i<NB_VAR; i++) { 
    neg_in[i] = (int *)malloc((neg_nb[i]+1) * sizeof(int));
    pos_in[i] = (int *)malloc((pos_nb[i]+1) * sizeof(int));
    neg_in[i][neg_nb[i]]=NONE; pos_in[i][pos_nb[i]]=NONE;
    neg_nb[i] = 0; pos_nb[i] = 0;
    var_state[i] = ACTIVE;
  }   
  for (i=0; i<NB_CLAUSE; i++) {
    // if (i==774)
    //  printf("kjhsdf");
    lits1 = sat[i];
    for(lit=*lits1; lit!=NONE; lit=*(++lits1)) {
      if (positive(lit)) 
	pos_in[lit][pos_nb[lit]++] = i;
      else
	neg_in[get_var_from_lit(lit)]
	  [neg_nb[get_var_from_lit(lit)]++] = i;
    }
  }
}

void eliminate_redundance() {
  int *lits, i, lit, *clauses, res, clause;

  for (i=0; i<NB_CLAUSE; i++) {
    if (clause_state[i]==ACTIVE) {
      if (clause_length[i]==1)
	push(i, UNITCLAUSE_STACK);
      lits = sat[i];
      for(lit=*lits; lit!=NONE; lit=*(++lits)) {
	if (positive(lit)) 
	  clauses=pos_in[lit];
	else clauses=neg_in[lit-NB_VAR];
	for(clause=*clauses; clause!=NONE; clause=*(++clauses)) {
	  if ((clause<i) && (clause_state[clause]==ACTIVE)) {
	    res=redundant(sat[i], sat[clause]);
	    if (res==NEW_CLAUSE_REDUNDANT) {
	      clause_state[i]=PASSIVE;
	      break;
	    }
	    else if (res==OLD_CLAUSE_REDUNDANT)
	      clause_state[clause]=PASSIVE;
	  }
	}
	if (res==NEW_CLAUSE_REDUNDANT)
	  break;
      }
    }
  }
}

my_type build_simple_sat_instance(char *input_file) {
  FILE* fp_in=fopen(input_file, "r");
  char ch, word2[WORD_LENGTH];
  int i, j, length, NB_CLAUSE1, res, ii, jj, tautologie, lit1,
    lits[1000], *lits1, lit, var, *pos_nb, *neg_nb;
  int clause,*vars_signs,cpt;
  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", word2, &NB_VAR, &NB_CLAUSE);
  INIT_NB_CLAUSE = NB_CLAUSE;
  neg_nb=(int *)reduce_if_negative_nb;
  pos_nb=(int *)reduce_if_positive_nb;

  lire_clauses(fp_in);
  fclose(fp_in);
  build_structure();
  eliminate_redundance();
  if (unitclause_process()==NONE) return NONE;
  // res=simplify_formula();
  //if (res==NONE) return NONE;
  //else if (res==FALSE) return FALSE;
  if (clean_structure()==FALSE)
    return FALSE;
  return TRUE;
}

int verify_sol_input(char *input_file) {
  FILE* fp_in=fopen(input_file, "r");
  char ch, word2[WORD_LENGTH];
  int i, j, lit, var, nb_var1, nb_clause1;

  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", word2, &nb_var1, &nb_clause1);
  for (i=0; i<nb_clause1; i++) {
    fscanf(fp_in, "%d", &lit);
    while (lit != 0) {
      if (lit<0) {
	if (var_current_value[abs(lit)-1]==FALSE)
	  break;
      }
      else {
	if (var_current_value[lit-1]==TRUE)
	  break;
      }
      fscanf(fp_in, "%d", &lit);
    }
    if (lit==0) {
      fclose(fp_in);
      return FALSE;
    }
    else {
      do fscanf(fp_in, "%d", &lit);
      while (lit != 0) ;
    }
  }
  fclose(fp_in);
  return TRUE;
}

int verify_solution() {
  int i, var, *vars_signs, clause_truth,cpt;

  for (i=0; i<NB_CLAUSE; i++) {
    clause_truth = FALSE;
    vars_signs = var_sign[i];
    for(var=*vars_signs; var!=NONE; var=*(vars_signs+=2))
      if (*(vars_signs+1) == var_current_value[var] ) {
	clause_truth = TRUE;
	break;
      }
    if (clause_truth == FALSE) return FALSE;
  }
  return TRUE;
}

long NB_SEARCH = 0; long NB_FIXED = 0;
  
int unitclause_process() {
  int  i, unitclause, var, *vars_signs, unitclause_position,cpt;
  
  for (unitclause_position = 0; 
       unitclause_position < UNITCLAUSE_STACK_fill_pointer;
       unitclause_position++) {
    unitclause = UNITCLAUSE_STACK[unitclause_position];
    if (clause_state[unitclause] == ACTIVE) {
      NB_UNIT++;
      vars_signs = var_sign[unitclause];
      for(var=*vars_signs; var!=NONE; var=*(vars_signs+=2)) {
	if (var_state[var] == ACTIVE ){
	  var_current_value[var] = *(vars_signs+1);
	  var_rest_value[var] = NONE;
	  if (manage_clauses(var)==TRUE) {
	    var_state[var] = PASSIVE;
	    push(var, VARIABLE_STACK);
	    remove_clauses(var);
	    break;
	  }
	  else {
	    return NONE;
	  }
	}
      }
    }     
  }
  UNITCLAUSE_STACK_fill_pointer = 0;
  return TRUE;
}


int unitclause_process1() {
  int  i, unitclause, var, *vars_signs, unitclause_position,cpt,lit;
  
  for (unitclause_position = 0; 
       unitclause_position < UNITCLAUSE_STACK_fill_pointer;
       unitclause_position++) {
    unitclause = UNITCLAUSE_STACK[unitclause_position];
    if (clause_state[unitclause] == ACTIVE) {
      NB_UNIT++;
      vars_signs = var_sign[unitclause];
      for(var=*vars_signs; var!=NONE; var=*(vars_signs+=2)) {
	if (var_state[var] == ACTIVE ){ 
	  var_current_value[var] = *(vars_signs+1);
	  var_rest_value[var] = NONE;
	  lit = (*(vars_signs+1) == POSITIVE)?var:var+NB_VAR;
	  tab_variable_nb_unit[lit]=CPT;
	  if (manage1_clauses(var)==TRUE) {
	    var_state[var] = PASSIVE;
	    push(var, VARIABLE_STACK);
	    //    remove_clauses(var);
	    break;
	  }
	  else return NONE;
	}
      }
    }     
  }
  UNITCLAUSE_STACK_fill_pointer = 0;
  return TRUE;
}

int get_nb_clauses(int var) {
  return ((nb_neg_clause_of_length2[var] + 
	   nb_pos_clause_of_length2[var]) * WEIGTH) + 
    nb_neg_clause_of_length3[var] + 
    nb_pos_clause_of_length3[var];
}

int get_resolvant_nb(int saved_managedclause_fill_pointer) {
  int *vars_signs;
  int lit, var, i, clause, resolvant_nb=0,resolvant_nb_tmp=1;
       
  for (i=saved_managedclause_fill_pointer; 
       i<MANAGEDCLAUSE_STACK_fill_pointer; i++) {
    clause = MANAGEDCLAUSE_STACK[i];
    if (clause_length[clause] == 2) {
      resolvant_nb_tmp = 1;
      vars_signs = var_sign[clause];
      for(var=*vars_signs; var!=NONE; var=*(vars_signs+=2)) {
	if (var_state[var] == ACTIVE ) {
	  if (*(vars_signs+1) == POSITIVE){
	    resolvant_nb_tmp *= (nb_neg_clause_of_length2[var] * WEIGTH)
	      +nb_neg_clause_of_length3[var]; 
	  }
	  else {
	    resolvant_nb_tmp *= (nb_pos_clause_of_length2[var] * WEIGTH) 
	      +nb_pos_clause_of_length3[var]; 
	  }
	}
      }
      resolvant_nb += resolvant_nb_tmp;
    }
  }
  return resolvant_nb;
}

void reset_context(int saved_var_stack_fill_pointer,
		   int saved_managedclause_fill_pointer) {
  int i;

  for (i=0; i<UNITCLAUSE_STACK_fill_pointer; i++)
    clause_length[UNITCLAUSE_STACK[i]]++;
  UNITCLAUSE_STACK_fill_pointer = 0;

  for (i=saved_var_stack_fill_pointer; 
       i<VARIABLE_STACK_fill_pointer; i++)
    var_state[VARIABLE_STACK[i]] = ACTIVE;
  VARIABLE_STACK_fill_pointer = saved_var_stack_fill_pointer;

  for (i=saved_managedclause_fill_pointer; 
       i<MANAGEDCLAUSE_STACK_fill_pointer; i++)
    clause_length[MANAGEDCLAUSE_STACK[i]]++;
  MANAGEDCLAUSE_STACK_fill_pointer = 
    saved_managedclause_fill_pointer;  
}

void reset_context1(int saved_var_stack_fill_pointer,
		   int saved_managedclause_fill_pointer) {
  int i, var;

  for (i=0; i<UNITCLAUSE_STACK_fill_pointer; i++)
    clause_length[UNITCLAUSE_STACK[i]]++;
  UNITCLAUSE_STACK_fill_pointer = 0;

  for (i=saved_var_stack_fill_pointer; 
       i<VARIABLE_STACK_fill_pointer; i++) {
    var=VARIABLE_STACK[i];
    var_state[var] = ACTIVE;
    if (var_current_value[var]==TRUE) LIT_IMPLIED[var]=IMPLIED_LIT_FLAG;
    else LIT_IMPLIED[var+NB_VAR]=IMPLIED_LIT_FLAG;
  }
  VARIABLE_STACK_fill_pointer = saved_var_stack_fill_pointer;

  for (i=saved_managedclause_fill_pointer; 
       i<MANAGEDCLAUSE_STACK_fill_pointer; i++)
    clause_length[MANAGEDCLAUSE_STACK[i]]++;
  MANAGEDCLAUSE_STACK_fill_pointer = 
    saved_managedclause_fill_pointer;  
}

void reset_context2(int saved_var_stack_fill_pointer,
		   int saved_managedclause_fill_pointer) {
  int i, var;

  for (i=0; i<UNITCLAUSE_STACK_fill_pointer; i++)
    clause_length[UNITCLAUSE_STACK[i]]++;
  UNITCLAUSE_STACK_fill_pointer = 0;

  for (i=saved_var_stack_fill_pointer; 
       i<VARIABLE_STACK_fill_pointer; i++) {
    var=VARIABLE_STACK[i];
    var_state[var] = ACTIVE;
    if (var_current_value[var]==TRUE) {
      if (LIT_IMPLIED[var]==IMPLIED_LIT_FLAG) push(var, IMPLIED_LIT_STACK);
    }
    else if (LIT_IMPLIED[var+NB_VAR]==IMPLIED_LIT_FLAG)
      push(var+NB_VAR, IMPLIED_LIT_STACK);
  }
  VARIABLE_STACK_fill_pointer = saved_var_stack_fill_pointer;

  for (i=saved_managedclause_fill_pointer; 
       i<MANAGEDCLAUSE_STACK_fill_pointer; i++)
    clause_length[MANAGEDCLAUSE_STACK[i]]++;
  MANAGEDCLAUSE_STACK_fill_pointer = 
    saved_managedclause_fill_pointer;  
}

int PREVIOUS_UNITCLAUSE_STACK_fill_pointer = 0;

int branch() {
  int var, *vars_signs, unitclause, unitclause_position,cpt;
  NB_SEARCH++;
  for (unitclause_position =0;
       unitclause_position != UNITCLAUSE_STACK_fill_pointer;
       unitclause_position++) {
    unitclause = UNITCLAUSE_STACK[unitclause_position];
    if (clause_state[unitclause] == ACTIVE) {
      vars_signs = var_sign[unitclause];
      for(var=*vars_signs; var!=NONE; var=*(vars_signs+=2)) {
	if (var_state[var] == ACTIVE) {
	  var_current_value[var] = *(vars_signs+1);
	  if (my_manage_clauses(var) == TRUE) {
	    var_state[var] = PASSIVE;
	    push(var, VARIABLE_STACK);
	    break;
	  }
	  else {
	    NB_FIXED++;
	    
	    return NONE;
	  }
	}
      }
    }
  }
  return MANAGEDCLAUSE_STACK_fill_pointer;
}

int branch1() {
  int var, *vars_signs, unitclause, unitclause_position,cpt;
  NB_SEARCH++;
  for (unitclause_position = 0;
       unitclause_position != UNITCLAUSE_STACK_fill_pointer;
       unitclause_position++) {
    unitclause = UNITCLAUSE_STACK[unitclause_position];
    if (clause_state[unitclause] == ACTIVE) {
      vars_signs = var_sign[unitclause];
      for(var=*vars_signs; var!=NONE; var=*(vars_signs+=2)) {
	if (var_state[var] == ACTIVE) {
	  var_current_value[var] = *(vars_signs+1);
	  if (manage_clauses(var) == TRUE) {
	    var_state[var] = PASSIVE;
	    push(var, VARIABLE_STACK);
	    remove_clauses(var);
	    break;
	  }
	  else {
	    NB_FIXED++;
	    return NONE;
	  }
	}
      }
    }
  }
  return MANAGEDCLAUSE_STACK_fill_pointer;
}

int get_complement(int lit) {
  if (positive(lit)) return lit+NB_VAR;
  else return lit-NB_VAR;
}

int further_examin_var_if_positive(int var) {
  int  nb_reduced_clauses_if_further_positif,
    saved_var_stack_fill_pointer,
    saved_managedclause_fill_pointer;

  saved_var_stack_fill_pointer=VARIABLE_STACK_fill_pointer;
  saved_managedclause_fill_pointer=
    MANAGEDCLAUSE_STACK_fill_pointer; 

  var_current_value[var] = TRUE;
  var_state[var] = PASSIVE;
  push(var, VARIABLE_STACK);
  my_simple_manage_clauses(var);
  NB_SECOND_SEARCH++; 
  nb_reduced_clauses_if_further_positif = branch();
  reset_context(saved_var_stack_fill_pointer, 
		saved_managedclause_fill_pointer);
    
  if (nb_reduced_clauses_if_further_positif == NONE) {
    NB_SECOND_FIXED++;
    var_current_value[var] = FALSE;
    var_state[var] = PASSIVE;
    push(var, VARIABLE_STACK);
    my_simple_manage_clauses(var);
    if (branch() == NONE) return NONE;
  }
  else  NB_SEARCH--; 
  return TRUE;
}

int further_examin_var_if_negative(int var) {
  int  nb_reduced_clauses_if_further_negatif,
    saved_var_stack_fill_pointer,
    saved_managedclause_fill_pointer;

  saved_var_stack_fill_pointer=VARIABLE_STACK_fill_pointer;
  saved_managedclause_fill_pointer=
    MANAGEDCLAUSE_STACK_fill_pointer; 
  
  var_current_value[var] = FALSE;
  var_state[var] = PASSIVE;
  push(var, VARIABLE_STACK);
  my_simple_manage_clauses(var);
  NB_SECOND_SEARCH++;
  nb_reduced_clauses_if_further_negatif = branch();
  reset_context(saved_var_stack_fill_pointer, 
		saved_managedclause_fill_pointer);
  
  if (nb_reduced_clauses_if_further_negatif == NONE) {
    NB_SECOND_FIXED++;
    var_current_value[var] = TRUE;
    var_state[var] = PASSIVE;
    push(var, VARIABLE_STACK);
    my_simple_manage_clauses(var);
    if (branch() == NONE) return NONE;
  }
  else  NB_SEARCH--; 
  return TRUE;
}

int further_examin(int saved_managedclause_fill_pointer) {
  int var, i, *vars_signs, lit, clause,cpt;

  for(i=saved_managedclause_fill_pointer; 
      i<MANAGEDCLAUSE_STACK_fill_pointer; i++) {
    clause=MANAGEDCLAUSE_STACK[i];
    if (clause_length[clause] == 2) {
      vars_signs = var_sign[clause];
      for(var=*vars_signs; var!=NONE; var=*(vars_signs+=2)) {
	if ((var_state[var] == ACTIVE) && 
	    (test_flag[var] < NB_SEARCH)){
	  if (*(vars_signs+1) == POSITIVE) {
	    test_flag[var] = NB_SEARCH; 
	    if (nb_neg_clause_of_length2[var]>0) {
	      if (further_examin_var_if_positive(var)==NONE) {
		MAX_REDUCED=-1;
		return NONE; 
	      } 
	    }
	  }
	  else {
	    test_flag[var] = NB_SEARCH; 
	    if (nb_pos_clause_of_length2[var]>0) {
	      if (further_examin_var_if_negative(var)==NONE) {
		MAX_REDUCED=-1;
		return NONE; 
	      }
	    }
	  }
	}
      }
    }
  }
  return TRUE;
}

int further_testable(int saved_managedclause_fill_pointer) {
  if ((MANAGEDCLAUSE_STACK_fill_pointer-
       saved_managedclause_fill_pointer>T_SEUIL) &&
      (MANAGEDCLAUSE_STACK_fill_pointer-
       saved_managedclause_fill_pointer>MAX_REDUCED)) {
    MAX_REDUCED=MANAGEDCLAUSE_STACK_fill_pointer-
      saved_managedclause_fill_pointer;
    return TRUE;
  }
  return FALSE;
}

int examine3(int tested_var) {
  int generating_if_positif, generating_if_negatif,
    saved_var_stack_fill_pointer,
    saved_managedclause_fill_pointer;

  saved_var_stack_fill_pointer=VARIABLE_STACK_fill_pointer;
  saved_managedclause_fill_pointer=
    MANAGEDCLAUSE_STACK_fill_pointer; 
  
  var_current_value[tested_var] = TRUE;
  
  var_state[tested_var] = PASSIVE;
  push(tested_var, VARIABLE_STACK);
  my_simple_manage_clauses(tested_var);
  generating_if_positif = branch();
  reduce_if_positive_nb[tested_var]=
    MANAGEDCLAUSE_STACK_fill_pointer-saved_managedclause_fill_pointer;
  
  if ((generating_if_positif == NONE) ||
      ((further_testable(saved_managedclause_fill_pointer)==TRUE) 
       && (further_examin(saved_managedclause_fill_pointer)==NONE))) {
    reset_context(saved_var_stack_fill_pointer, 
		  saved_managedclause_fill_pointer);
    var_current_value[tested_var] = FALSE;
    var_rest_value[tested_var] = NONE;
    var_state[tested_var] = PASSIVE;
    push(tested_var, VARIABLE_STACK);
    simple_manage_clauses(tested_var);
    remove_clauses(tested_var); 
    return NONE;
  }
  else {
    reset_context1(saved_var_stack_fill_pointer, 
		  saved_managedclause_fill_pointer);
  }
  
  var_current_value[tested_var] = FALSE;
  
  var_state[tested_var] = PASSIVE;
  push(tested_var, VARIABLE_STACK);
  my_simple_manage_clauses(tested_var);
  
  generating_if_negatif = branch();
  reduce_if_negative_nb[tested_var]=
    MANAGEDCLAUSE_STACK_fill_pointer-saved_managedclause_fill_pointer;
  
  if ((generating_if_negatif == NONE) ||
      ((further_testable(saved_managedclause_fill_pointer)==TRUE) 
       && (further_examin(saved_managedclause_fill_pointer)==NONE)))  {
    reset_context(saved_var_stack_fill_pointer, 
		  saved_managedclause_fill_pointer);
    var_current_value[tested_var] = TRUE;
    simple_manage_clauses(tested_var);
    var_rest_value[tested_var] = NONE;
    var_state[tested_var] = PASSIVE;
    push(tested_var, VARIABLE_STACK);
    remove_clauses(tested_var);
    return NONE;
  }
  else {
    reset_context2(saved_var_stack_fill_pointer, 
		  saved_managedclause_fill_pointer);
  }
  push(tested_var, TESTED_VAR_STACK);
  return TRUE;
}

int examine3bis(int tested_var) {
  int generating_if_positif, generating_if_negatif,
    saved_var_stack_fill_pointer,
    saved_managedclause_fill_pointer;

  saved_var_stack_fill_pointer=VARIABLE_STACK_fill_pointer;
  saved_managedclause_fill_pointer=
    MANAGEDCLAUSE_STACK_fill_pointer; 
  
  
  var_current_value[tested_var] = FALSE;
  
  var_state[tested_var] = PASSIVE;
  push(tested_var, VARIABLE_STACK);
  my_simple_manage_clauses(tested_var);
  
  generating_if_negatif = branch();
  reduce_if_negative_nb[tested_var]=
    MANAGEDCLAUSE_STACK_fill_pointer-saved_managedclause_fill_pointer;
  
  if ((generating_if_negatif == NONE) ||
      ((further_testable(saved_managedclause_fill_pointer)==TRUE) 
       && (further_examin(saved_managedclause_fill_pointer)==NONE)))  {
    reset_context(saved_var_stack_fill_pointer, 
		  saved_managedclause_fill_pointer);
    var_current_value[tested_var] = TRUE;
    simple_manage_clauses(tested_var);
    var_rest_value[tested_var] = NONE;
    var_state[tested_var] = PASSIVE;
    push(tested_var, VARIABLE_STACK);
    remove_clauses(tested_var);
    return NONE;
  }
  else {
    reset_context1(saved_var_stack_fill_pointer, 
		  saved_managedclause_fill_pointer);
  }

 var_current_value[tested_var] = TRUE;
  
  var_state[tested_var] = PASSIVE;
  push(tested_var, VARIABLE_STACK);
  my_simple_manage_clauses(tested_var);
  generating_if_positif = branch();
  reduce_if_positive_nb[tested_var]=
    MANAGEDCLAUSE_STACK_fill_pointer-saved_managedclause_fill_pointer;
  
  if ((generating_if_positif == NONE) ||
      ((further_testable(saved_managedclause_fill_pointer)==TRUE) 
       && (further_examin(saved_managedclause_fill_pointer)==NONE))) {
    reset_context(saved_var_stack_fill_pointer, 
		  saved_managedclause_fill_pointer);
    var_current_value[tested_var] = FALSE;
    var_rest_value[tested_var] = NONE;
    var_state[tested_var] = PASSIVE;
    push(tested_var, VARIABLE_STACK);
    simple_manage_clauses(tested_var);
    remove_clauses(tested_var); 
    return NONE;
  }
  else {
    reset_context2(saved_var_stack_fill_pointer, 
		  saved_managedclause_fill_pointer);
  }

  push(tested_var, TESTED_VAR_STACK);
  return TRUE;
}

int get_neg_clause_nb(int var) {
  my_type neg_clause3_nb = 0, neg_clause2_nb = 0;
  int *clauses, clause;
  clauses = neg_in[var];

  for(clause=*clauses; clause!=NONE; clause=*(++clauses)) {
    if (clause_state[clause] == ACTIVE) {
      if (clause_length[clause] == 2)
	neg_clause2_nb++;
      else
	neg_clause3_nb++;
    }
  }
  nb_neg_clause_of_length2[var] = neg_clause2_nb;
  nb_neg_clause_of_length3[var] = neg_clause3_nb;
  return neg_clause2_nb + neg_clause3_nb;
}

int get_pos_clause_nb(int var) {

  my_type pos_clause3_nb = 0, pos_clause2_nb = 0;
  int *clauses, clause;
  clauses = pos_in[var];

  for(clause=*clauses; clause!=NONE; clause=*(++clauses)) {
    if (clause_state[clause] == ACTIVE) {
      if (clause_length[clause] == 2)
	pos_clause2_nb++;
      else
	pos_clause3_nb++;
    }
  }
  nb_pos_clause_of_length2[var] = pos_clause2_nb;
  nb_pos_clause_of_length3[var] = pos_clause3_nb;
  return pos_clause2_nb + pos_clause3_nb;
}

int satisfy_literal(int lit) {
  int var;
  if (positive(lit)) {
    if (var_state[lit]==ACTIVE) {
      var_current_value[lit] = TRUE;
      if (manage_clauses(lit)==FALSE) return NONE;
      var_rest_value[lit]=NONE;
      var_state[lit] = PASSIVE;
      push(lit, VARIABLE_STACK);
      remove_clauses(lit);
    }
    else
      if (var_current_value[lit]==FALSE) return NONE;
  } 
  else {
    var = get_var_from_lit(lit);
    if (var_state[var]==ACTIVE) {
      var_current_value[var] = FALSE;
      if (manage_clauses(var)==FALSE) return NONE;
      var_rest_value[var]=NONE;
      var_state[var] = PASSIVE;
      push(var, VARIABLE_STACK);
      remove_clauses(var);
    }
    else
      if (var_current_value[var]==TRUE) return NONE;
  }
  if (unitclause_process()==NONE) 
    return NONE; 
  else return FALSE;
}

int treat_implied_lits() {
  int i, lit;
  for (i=0; i<IMPLIED_LIT_STACK_fill_pointer; i++) {
      if (satisfy_literal(IMPLIED_LIT_STACK[i])==NONE)
	return NONE;
  }
  return TRUE;
}


int simplify_formula() {
  int var, pos2, neg2, flag;

  TESTED_VAR_STACK_fill_pointer=0; MAX_REDUCED=-1;
  VARIABLE_STACK_fill_pointer = 0;
  CLAUSE_STACK_fill_pointer = 0;
  MANAGEDCLAUSE_STACK_fill_pointer = 0;
  do {
    flag=FALSE;
    for (var = 0; var < NB_VAR; var++) {
      if (var_state[var] == ACTIVE) {
	reduce_if_negative_nb[var]=0;
	reduce_if_positive_nb[var]=0;
	if (get_neg_clause_nb(var) == 0) {
	  NB_MONO++;
	  var_current_value[var] = TRUE;
	  var_rest_value[var] = NONE;
	  var_state[var] = PASSIVE;
	  push(var, VARIABLE_STACK);
	  remove_clauses(var);
	  flag=TRUE;
	}
	else
	  if (get_pos_clause_nb(var) == 0) {
	    NB_MONO++;
	    var_current_value[var] = FALSE;
	    var_rest_value[var] = NONE;
	    var_state[var] = PASSIVE;
	    push(var, VARIABLE_STACK);
	    remove_clauses(var);
	    flag=TRUE;
	  }
	  else {
	    pos2 = nb_pos_clause_of_length2[var];
	    neg2 = nb_neg_clause_of_length2[var];
	    if ((neg2>0) || (pos2>0)) {
	      IMPLIED_LIT_FLAG++;
	      IMPLIED_LIT_STACK_fill_pointer=0;
	      if (examine3(var) == NONE) {
		flag=TRUE;
		if (unitclause_process() == NONE) return NONE;
	      }
	      else if (IMPLIED_LIT_STACK_fill_pointer>0) {
		flag=TRUE;
		if (treat_implied_lits()==NONE)  return NONE;
	      }
	    }
	  }
      }
    }
  } while (flag==TRUE);
  return TRUE;
}

my_type build(int build_flag, char* input_file) {
  if (build_flag==TRUE)
    return build_simple_sat_instance(input_file);
  else return build_simple_sat_instance(input_file);
}

void reset_all() {
  int index;
      
  UNITCLAUSE_STACK_fill_pointer = 0; NB_BACK=0; NB_BRANCHE=0;
  NB_MONO=0; NB_UNIT=0;  NB_SEARCH=0; NB_FIXED=0;
  NB_SECOND_SEARCH=0; NB_SECOND_FIXED=0;
  for (index=0; index<VARIABLE_STACK_fill_pointer; index++)
    var_state[VARIABLE_STACK[index]] = ACTIVE;
  VARIABLE_STACK_fill_pointer = 0;
   
  for (index = 0; index < CLAUSE_STACK_fill_pointer; index++)
    clause_state[CLAUSE_STACK[index]] = ACTIVE;
  CLAUSE_STACK_fill_pointer = 0;
   
  for (index = 0; index < MANAGEDCLAUSE_STACK_fill_pointer; index++)
    clause_length[MANAGEDCLAUSE_STACK[index]]++;
  MANAGEDCLAUSE_STACK_fill_pointer = 0;
}

#define DECREASING 1
#define INCREASING 2
#define PLATEAU 0
int var_count[tab_variable_size]={1};
int neibor_stack[tab_variable_size];
int neibor_stack_fill_pointer=0;
int **neibor_relations[tab_variable_size];
int *neibor[tab_variable_size];
int score[tab_variable_size];
int tmp_score[tab_variable_size];
int decreasing_vars_stack[tab_variable_size];
int decreasing_vars_stack_fill_pointer=0;
int tabu[tab_variable_size]={FALSE};
int tabu_stack[tab_variable_size];
int tabu_stack_fill_pointer=0;
int tabu_list[tab_variable_size];
int tendance[tab_variable_size];
int MY_CLAUSE_STACK_fill_pointer=0;
int MY_CLAUSE_STACK[tab_clause_size];
int nb_lit_true[tab_clause_size];
int clause_truth[tab_clause_size];
int dommage_if_flip[tab_variable_size];
int zerodommage[tab_variable_size];
int zerodommage_vars_stack[tab_variable_size];
int zerodommage_vars_stack_fill_pointer=0;
int flip_time[tab_variable_size];
int enter_stack_time[tab_variable_size];
int walk_time[tab_variable_size];
int MAXTRIES=1;
int MAXSTEPS=10000000;
int NOISE=50;
int LNOISE=5;
int saved_var_current_value[tab_variable_size];

void clause_value() {
  int clause, var, *vars_signs, nb_true;
   
  MY_CLAUSE_STACK_fill_pointer=0;  
  for (clause=0; clause<NB_CLAUSE; clause++) {
    nb_true=0;
    vars_signs = var_sign[clause];
    for(var=*vars_signs; var!=NONE; var=*(vars_signs+=2))
      if (var_current_value[var]==*(vars_signs+1))  
	nb_true++;        
    nb_lit_true[clause]=nb_true;
    if (nb_true ==0 ) {
      clause_truth[clause]=FALSE;
      push(clause, MY_CLAUSE_STACK);
    }
    else
      clause_truth[clause]=TRUE;    
  } 
}

void pass(int the_var, int *clauses) {
  int clause, var, *vars_signs;
  for(clause=*clauses; clause!=NONE; clause=*(++clauses)) {
    if (clause_state[clause] == ACTIVE) {
      vars_signs = var_sign[clause];
      for(var=*vars_signs; var!=NONE; var=*(vars_signs+=2)) {
	if (var_state[var]==ACTIVE && var != the_var) {
	  if (var_count[var]==1) push(var, neibor_stack);
	  // nb of cells for other variables (than var and the_var: length-2)
	  //and a sign for dxdy and a separator from the next clauses
	  var_count[var]+=2*(clause_length[clause]-1);
	}
      }
    }
  }
}

int *build_neibor_relation(int var, int neibor_var, 
			  int *neibor_relations, int *clauses) {
  int i, clause, var1, *vars_signs, present, *relations, sign1, sign2;

  for(clause=*clauses; clause!=NONE; clause=*(++clauses)) {
    if (clause_state[clause] == ACTIVE) {
      vars_signs = var_sign[clause];
      present=FALSE;
      for(var1=*vars_signs; var1!=NONE; var1=*(vars_signs+=2)) {
	if (var1==neibor_var) {present=TRUE; break;}
      }
      if (present==TRUE) {
	relations=neibor_relations; neibor_relations++;
	vars_signs = var_sign[clause];
	for(var1=*vars_signs; var1!=NONE; var1=*(vars_signs+=2)) {
	  if (var_state[var1]==ACTIVE) {
	    if (var1==var) sign1=*(vars_signs+1);
	    else if (var1==neibor_var) sign2=*(vars_signs+1);
	    else {
	      *neibor_relations=var1; 
	      *(neibor_relations+1)=*(vars_signs+1);
	      neibor_relations+=2;
	    }
	  }
	}
	*relations=(sign1==sign2);
	*neibor_relations=NONE;
	neibor_relations++;
      }
    }
  }
  return neibor_relations;
}
      

void preprocess() {
  int var, neibor_var, i, **vector_relations, *vector, *relations;

  for (var=0; var<NB_VAR; var++) {
    var_count[var]=1;
    tabu[var]=FALSE;
    tabu_list[var]=FALSE;
  }

  for (var=0; var<NB_VAR; var++) {
    for(i=0; i<neibor_stack_fill_pointer; i++) var_count[neibor_stack[i]]=1;
    neibor_stack_fill_pointer=0;
    pass(var, neg_in[var]);
    pass(var, pos_in[var]);
    vector=(int *)malloc((neibor_stack_fill_pointer+1)*sizeof(int));
    // vector_relations=(int **)malloc((neibor_stack_fill_pointer+1)*sizeof(int));
    for(i=0; i<neibor_stack_fill_pointer; i++) {
      neibor_var=neibor_stack[i];
      vector[i]=neibor_var;
      // neibor_var occupies var_count cells for all clauses
      // in which var and neibor_var both occur
      //vector_relations[i]=(int *)malloc((var_count[neibor_var])*sizeof(int));
      //relations=build_neibor_relation(var, neibor_var, 
      //vector_relations[i], neg_in[var]);
    // relations=build_neibor_relation(var, neibor_var, 
      //			      relations, pos_in[var]);
      //the end
      //*relations=NONE;
    }
    vector[i]=NONE;
    neibor[var]=vector;
// neibor_relations[var]=vector_relations;
  }
}

int random_integer(int max)
{
  unsigned long int RAND;
  RAND=rand();
  return RAND % max;
}

//-------------------------------------------------------------------------

//Modifaction du germe du générateur aléatoire

//-------------------------------------------------------------------------
/*
void modify_seed()
{
  struct tms *a_tms;
  int seed=2;
  time_t tp, mess;

  mess=time(&tp);

//  tv=(struct timeval *)malloc(sizeof(struct timeval));
//  tzp=(struct timezone *)malloc(sizeof(struct timezone));
//  gettimeofday(tv,tzp);
//  seed = (( tv->tv_sec & 0177 ) * 1000000) + tv->tv_usec;  

  if (mess==-1) {
    a_tms = ( struct tms *) malloc( sizeof (struct tms));
    mess=times(a_tms);
    seed = a_tms->tms_utime;
  }
  else seed=mess;
  srand(seed);
}
*/

  struct timeval tv;
  struct timezone tzp;

void modify_seed() {
  int seed;
  if (SEED_FLAG==TRUE) {
    srand(SEED); SEED++;
  }
  else {
    gettimeofday(&tv,&tzp);
    seed = (( tv.tv_sec & 0177 ) * 1000000) + tv.tv_usec;
    srand(seed);
  }
}

int get_gradient(int var, int *clauses) {
  int clause, var1, *vars_signs, gradient=0, clause_gradient=1;
  for(clause=*clauses; clause!=NONE; clause=*(++clauses)) {
    if (clause_state[clause] == ACTIVE) {
      vars_signs = var_sign[clause];  clause_gradient=1;
      for(var1=*vars_signs; var1!=NONE; var1=*(vars_signs+=2)) {
	if ((var_state[var1]==ACTIVE) && (var1!=var)) {
	  if (var_current_value[var1]==*(vars_signs+1)) {
	    clause_gradient=0; break;
	  }
	}
      }
      gradient+=clause_gradient;
    }
  }
  return gradient;
}

void free_tabu() {
  int i, var;
  for (i=0; i<tabu_stack_fill_pointer; i++) {
    var=tabu_stack[i];
    tabu[var]=FALSE;
    tabu_list[var]=FALSE;
  }
  tabu_stack_fill_pointer=0;
}

inline int decreasing_var(int var) {
  return (score[var]>0);
}

int initialize() {
  int var, gradient, neg_gradient, pos_gradient;

  decreasing_vars_stack_fill_pointer=0;
  zerodommage_vars_stack_fill_pointer=0;
  for (var=0; var<NB_VAR; var++) {
    tmp_score[var]=0;
    if (var_state[var]==ACTIVE) {
      neg_gradient=get_gradient(var, neg_in[var]);
      pos_gradient=get_gradient(var, pos_in[var]);
      if (var_current_value[var]==TRUE)
	score[var]=neg_gradient-pos_gradient;
      else score[var]=pos_gradient-neg_gradient;
      if (var_current_value[var]==TRUE)
	dommage_if_flip[var]=pos_gradient;
      else dommage_if_flip[var]=neg_gradient;
      if ((dommage_if_flip[var]==0)  && ( score[var] != 0)) {
	push(var, zerodommage_vars_stack);
	zerodommage[var]=TRUE;
      }
      else zerodommage[var]=FALSE;
      if (decreasing_var(var)) {
	push(var, decreasing_vars_stack);
	tendance[var]=DECREASING;
      }
      else if (score[var]==0)
	tendance[var]=PLATEAU;
      else tendance[var]=INCREASING;
    }
  }
  free_tabu();
  return TRUE;
}
/*
int score1[tab_variable_size];

int check_gradient(int flag, int var_to_flip, int saved) {
  int i, var, pos_gradient, neg_gradient, clause, nb, *vars_signs, 
    nb_unsat=0, nb_dec=0, nb_zerodommage;

  if (flag) {
    if (saved!=abs(score[var_to_flip])+MY_CLAUSE_STACK_fill_pointer)
      printf("problem1 : %d %d %d\n", saved, score[var_to_flip],
	     MY_CLAUSE_STACK_fill_pointer);
  }
  else { 
    // la tendance de var_to_flip a été déjà inversé à cause du dernier flip
    // CaD, INCREASING implique qu'elle était DECREASING et vice versa.
    if ((tendance[var_to_flip]==INCREASING &&
	 saved-abs(score[var_to_flip])!= MY_CLAUSE_STACK_fill_pointer) 
	|| 
	(tendance[var_to_flip]==DECREASING && 
	 saved+abs(score[var_to_flip])!= MY_CLAUSE_STACK_fill_pointer)
	||
	(tendance[var_to_flip]==PLATEAU && 
	 saved-abs(score[var_to_flip])!= MY_CLAUSE_STACK_fill_pointer)) 
      printf("problem2 : %d %d %d\n", saved, score[var_to_flip],
	     MY_CLAUSE_STACK_fill_pointer);
  }

  for(clause=0; clause<NB_CLAUSE; clause++) {
    if (clause_state[clause]==ACTIVE) {
      vars_signs=var_sign[clause]; nb=0;
      for(var=*vars_signs; var!=NONE; var=*(vars_signs+=2)) {
	if (var_current_value[var]==*(vars_signs+1))
	  nb++;
      }
      if (nb != nb_lit_true[clause])
	 printf("problème...\n");
      if (nb==0) nb_unsat++;
    }
  }
  if (nb_unsat != MY_CLAUSE_STACK_fill_pointer)
    printf("problème...\n");
  for(i=0; i<MY_CLAUSE_STACK_fill_pointer; i++) {
    clause=MY_CLAUSE_STACK[i];
    if (nb_lit_true[clause]!=0)
      printf("problème...\n");
  }
  nb_zerodommage=0;
  for (var=0; var<NB_VAR; var++) {
    if (var_state[var]==ACTIVE) {
      neg_gradient=get_gradient(var, neg_in[var]);
      pos_gradient=get_gradient(var, pos_in[var]);
      score1[var]=neg_gradient-pos_gradient;
      if (score1[var] != 0) {
	if ((var_current_value[var]==NEGATIVE && neg_gradient==0)
	    || (var_current_value[var]==POSITIVE && pos_gradient==0)) {
	  if (zerodommage[var]!=TRUE)
	    printf("problème...");
	  nb_zerodommage++;
	}
	else if (zerodommage[var]==TRUE)
	  printf("problème...");
      }
      else if (zerodommage[var]==TRUE)
	  printf("problème...");
    }
    if (score[var]!= score1[var])
      printf("problème...\n");
    if (score[var]==0) {
      if (tendance[var]!=PLATEAU)
	printf("problème...\n");
    }
    else if (score[var]>0) {
      if (var_current_value[var]==TRUE) {
	if  (tendance[var]!=DECREASING)
	  printf("problème...\n");
	nb_dec++;
      }
      else if  (tendance[var]!=INCREASING)
	printf("problème...\n");
    }
    else {
      if (var_current_value[var]==TRUE) {
	if  (tendance[var]!=INCREASING)
	  printf("problème...\n");
      }
      else {
	if  (tendance[var]!=DECREASING)
	  printf("problème...\n");
	nb_dec++;
      }
    }
  }
  if (nb_dec != decreasing_vars_stack_fill_pointer)
    printf("problème...\n");
  for(i=0; i<decreasing_vars_stack_fill_pointer; i++) {
    var=decreasing_vars_stack[i];
    if (tendance[var]!=DECREASING)
      printf("problème...\n");
  }
  if (nb_zerodommage!=zerodommage_vars_stack_fill_pointer)
      printf("problème...\n");
  for(i=0; i<zerodommage_vars_stack_fill_pointer; i++) {
    var=zerodommage_vars_stack[i];
    if (zerodommage[var]!=TRUE || dommage_if_flip[var]!=0 ||
	score1[var] == 0)
      printf("problème...\n");
  }
  return TRUE;
}
*/

int nb_clauses_violated(int *clauses) {
  int clause, nb_violated=0;
    
  for (clause=*clauses;clause!=NONE;clause=*(++clauses))
    if (nb_lit_true[clause]==1)
      nb_violated++;       
  return nb_violated; 
}

int choose_least_flipped_var() {
  int var, chosen_var, i, flip=MAXSTEPS;

  for (i=0; i<VARIABLE_STACK_fill_pointer; i++) {
    var=VARIABLE_STACK[i];
    if (flip_time[var]<flip) {
      chosen_var=var; flip=flip_time[var];
    }
  }
  return chosen_var;
}

int get_var_to_flip_in_clause(int random_clause_unsat) {
  int var, best_var, second_best_var, nb, max_nb, pos_gradient, second_max=-NB_CLAUSE,
    neg_gradient, real_nb, flip=-1, flip_index, var_to_flip, old=MAXSTEPS, old_var;
  register int *vars_signs;

  vars_signs = var_sign[random_clause_unsat]; max_nb=-NB_CLAUSE;
  for(var=*vars_signs; var!=NONE; var=*(vars_signs+=2)) {
    nb=score[var];
    if ((nb>max_nb) || ((nb==max_nb) && (flip_time[var]<flip_time[best_var]))) {
      second_best_var=best_var; second_max=max_nb; best_var=var; max_nb=nb;
    }
    else if ((nb>second_max) || 
	     ((nb==second_max) && (flip_time[var]<flip_time[second_best_var]))) {
      second_max=nb; second_best_var=var;
    }
    if (flip_time[var]>flip) 
      flip=flip_time[var];
    if (flip_time[var]<old) {
      old=flip_time[var];
      old_var=var;
    }
  }
  if (random_integer(100)<LNOISE)
    return old_var;
  else {
    if (flip_time[best_var]==flip) {
      if (random_integer(100)<NOISE) 
	return second_best_var; 
      else return best_var;
      // flip_index=random_integer(clause_length[random_clause_unsat]);
      // var_to_flip=var_sign[random_clause_unsat][2*flip_index];
      //return var_to_flip;
    }
    else return best_var;
  }
}
  
/* let x1 be the new value of x and x0 be the old value of x
   then for each clause in *clauses here, (x1-x0)df/dx is negative */
void satisfy_clauses(int var, int *clauses) {
  int clause,  neibor_var, *vars_signs, dommage=0;
  for (clause=*clauses;clause!=NONE;clause=*(++clauses)) {
    vars_signs=var_sign[clause];
    switch(nb_lit_true[clause]) {
    case 0: clause_truth[clause]=TRUE; nb_lit_true[clause]++;
      dommage++;
      for(neibor_var=*vars_signs; neibor_var!=NONE; 
	  neibor_var=*(vars_signs+=2)) {
	if (neibor_var!=var) {
	    tmp_score[neibor_var]--;
	}
      }
      break;
    case 1: nb_lit_true[clause]++;
      for(neibor_var=*vars_signs; neibor_var!=NONE; 
	  neibor_var=*(vars_signs+=2)) {
	if ((neibor_var!=var) && 
	    (var_current_value[neibor_var]==*(vars_signs+1))) {
	  // dommage_if_flip[neibor_var]--;
	  tmp_score[neibor_var]++;
	  break;
	}
      }
      break;
    default:  nb_lit_true[clause]++;
    }
  }
  if (dommage==0) 
    printf("c'est curieux...");
  /*
  dommage_if_flip[var]=dommage;
  if (dommage==0) {
    if (score[var] !=0) {
      printf("c'est curieux...");
      zerodommage[var]=TRUE;
    }
    else zerodommage[var]=FALSE;
  }
  else zerodommage[var]=FALSE;
  */
}

/* let x1 be the new value of x and x0 be the old value of x
   then for each clause in *clauses here, (x1-x0)df/dx is positive */
void unsatisfy_clauses(int var, int *clauses) {
  int clause, neibor_var, *vars_signs;
  for (clause=*clauses;clause!=NONE;clause=*(++clauses)) {
    vars_signs=var_sign[clause];
    switch(nb_lit_true[clause]) {
    case 1:  clause_truth[clause]=FALSE; nb_lit_true[clause]--;
      push(clause,MY_CLAUSE_STACK);
      for(neibor_var=*vars_signs; neibor_var!=NONE; 
	  neibor_var=*(vars_signs+=2)) {
	if (neibor_var!=var) {
	  tmp_score[neibor_var]++;
	}
      }
      break;
    case 2: nb_lit_true[clause]--;
      for(neibor_var=*vars_signs; neibor_var!=NONE; 
	  neibor_var=*(vars_signs+=2)) {
	if ((neibor_var!=var) && 
	    (var_current_value[neibor_var]==*(vars_signs+1))) {
	  tmp_score[neibor_var]--;
	  // dommage_if_flip[neibor_var]++;
	  break;
	}
      }
      break;
    default:  nb_lit_true[clause]--;
    }
  }
}

void check_implied_clauses(int var, int value, int nb_flip) { 
  int *neibors, neibor_var;
  //neibors=neibor[var];
  //  for(neibor_var=*neibors; neibor_var!=NONE; neibor_var=*(++neibors)) 
  //  tmp_score[neibor_var]=0;
  if (value==TRUE) {
    satisfy_clauses(var, pos_in[var]);
    unsatisfy_clauses(var, neg_in[var]);
  }
  else {
    satisfy_clauses(var, neg_in[var]);
    unsatisfy_clauses(var, pos_in[var]);
  }
  neibors=neibor[var];
  for(neibor_var=*neibors; neibor_var!=NONE; neibor_var=*(++neibors)) {
    if ((score[neibor_var]<=0) && (score[neibor_var]+tmp_score[neibor_var]>0))
      push(neibor_var, decreasing_vars_stack);
    score[neibor_var]+=tmp_score[neibor_var];
    tmp_score[neibor_var]=0;
  }
}

void eliminate_satisfied_clauses() {
  int first_satisfied=NONE,put_in,i;
  
  for (i=0;i<MY_CLAUSE_STACK_fill_pointer;i++)
    if(clause_truth[MY_CLAUSE_STACK[i]]==TRUE) {
      first_satisfied=i;
      break;
    }    
  if (first_satisfied!=NONE) { 
    put_in=first_satisfied;
    for (i=first_satisfied+1;i<MY_CLAUSE_STACK_fill_pointer;i++)
      if (clause_truth[MY_CLAUSE_STACK[i]]!=TRUE) {
	MY_CLAUSE_STACK[put_in]=MY_CLAUSE_STACK[i];
	put_in++;              
      }
    MY_CLAUSE_STACK_fill_pointer=put_in;
  }
}

void push_unsatisfied_clauses(int var, int value) { 
  int *clauses,clause;
   
  if (value==TRUE) clauses=neg_in[var];
  else clauses=pos_in[var];
  for (clause=*clauses;clause!=NONE;clause=*(++clauses)) {
    if (nb_lit_true[clause]==1 ) {
      push(clause,MY_CLAUSE_STACK);
      clause_truth[clause]=FALSE;         
    }
    nb_lit_true[clause]--;
  } 
}

void dec_nb_lit_true(int var, int value) {
  int *clauses,clause;
  if (positive(var))
    clauses=neg_in[var];
  else
    clauses=pos_in[var];
  for (clause=*clauses;clause!=NONE;clause=*(++clauses))    
    nb_lit_true[clause]--;    
}

int simple_eliminate_increasing_vars() {
  int i, first=NONE, put_in, var, current=0, nb=0, chosen_var=NONE, flip=MAXSTEPS;
  for (i=0; i<decreasing_vars_stack_fill_pointer; i++) {
    var=decreasing_vars_stack[i];
    if (score[var]<=0) {
      first=i;
      break;
    }
    else {
      if (score[var]>nb) {
	nb=score[var]; flip=flip_time[var];
	chosen_var=var; 
      }
      else if (score[var]==nb) {
	if  (flip_time[var]<flip) {
	  chosen_var=var; flip=flip_time[var];
	}
      }
    }
  }
  if (first !=NONE) {
    put_in=first;
    for (i=first+1; i<decreasing_vars_stack_fill_pointer; i++) {
      var=decreasing_vars_stack[i];
      if (score[var]>0) {
	decreasing_vars_stack[put_in++]=var;
	if (score[var]>nb) {
	  nb=score[var]; flip=flip_time[var];
	  chosen_var=var; 
	}
	else if (score[var]==nb) {
	  if  (flip_time[var]<flip) {
	    chosen_var=var; flip=flip_time[var];
	  }
	}
      }
    }
    decreasing_vars_stack_fill_pointer=put_in;
  }
  return chosen_var;
}

void eliminate_dommage_vars() {
  int i, first=NONE, put_in, var, current=-1;
  for (i=0; i<zerodommage_vars_stack_fill_pointer; i++) {
    var=zerodommage_vars_stack[i];
    if (zerodommage[var]==FALSE) {
      first=i;
      break;
    }
  }
  if (first !=NONE) {
    put_in=first;
    for (i=first+1; i<zerodommage_vars_stack_fill_pointer; i++) {
      var=zerodommage_vars_stack[i];
      if (zerodommage[var]==TRUE)
	zerodommage_vars_stack[put_in++]=var;
    }
    zerodommage_vars_stack_fill_pointer=put_in;
  }
}

int choose_best_decreasing_var() {
  int var, chosen_var=NONE, i, nb=0, flip=MAXSTEPS;

  for (i=0; i<decreasing_vars_stack_fill_pointer; i++) {
    var=decreasing_vars_stack[i];
    if (score[var]>nb) {
      nb=score[var]; flip=flip_time[var];
      chosen_var=var; 
    }
    else if (score[var]==nb) {
      if  (flip_time[var]<flip) {
	chosen_var=var; flip=flip_time[var];
      }
    }
  }
  return chosen_var;
}
  
int update_gradient_and_choose_flip_var(int var) {
  int neibor_var, chosen1, sign, index,
    other_var_in_same_clause, clause_gradient, gradient, chosen_var=NONE;

  score[var]=0-score[var];
  chosen_var=simple_eliminate_increasing_vars();
  //chosen_var=choose_best_decreasing_var();
  return chosen_var;
}

int choose_var_by_random_walk() {
  int  random_unsatisfied_clause,  var_to_flip;
  random_unsatisfied_clause=random_integer(MY_CLAUSE_STACK_fill_pointer);
  random_unsatisfied_clause=MY_CLAUSE_STACK[random_unsatisfied_clause];
  var_to_flip=get_var_to_flip_in_clause(random_unsatisfied_clause);
  return  var_to_flip;
}

int flipped_var_stack[tab_variable_size];
int flipped_var_stack_fill_pointer=0;
int flipped[tab_variable_size];

void clean_flipped() {
  int i;
  for(i=0; i<flipped_var_stack_fill_pointer; i++)
    flipped[flipped_var_stack[i]]=0;
  flipped_var_stack_fill_pointer=0;
}

void save_assignment() {
  int i;
  clean_flipped();
  // for(i=0; i<NB_VAR; i++) 
  //  saved_var_current_value[i]=var_current_value[i];
}

int compute_distance() {
  int k, dist=0, var, i;
  for(i=0; i<flipped_var_stack_fill_pointer; i++) {
    var=flipped_var_stack[i];
    if (flipped[var]%2 == 1) 
      dist++;
  }
  //for(k=0;k<NB_VAR;k++) {
  //  if (var_current_value[k] != saved_var_current_value[k])
  //    dist++; 
  //}
  return dist;
}

void search(char *input_file) {
  int i,j,k,SAT=FALSE,random_clause,var_to_flip=NONE, index, flag, saved,
    *min,  nbminima=0, nb_suc=0, walkperiod=FALSE, nbwalk=0,
    nb, dist, verify=0;

  double avgdepth, depth=0;
  double avgdepths=0, total_min=0, total_last=0, total_nbwalk=0, total_nb_flip=0;
  long begintime, endtime, mess;
  struct tms *a_tms;
  FILE *fp_time;

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

  min=(int *)malloc(MAXTRIES*sizeof(int));
  preprocess();

  printf("#lowest #last    #flip    #walk      meanDepth  sucRate   verifySol\n");

  for (i=0;i<MAXTRIES;i++) {
    modify_seed(); min[i]=NB_CLAUSE; nbwalk=0; SAT=FALSE; depth=0;  
    // Generation de valeurs aleatoires pour le vecteur var_current_value
    for (k=0;k<NB_VAR;k++) {
      if (var_state[k]==ACTIVE) {
	var_current_value[k]=random_integer(2);
	enter_stack_time[k]=0;
	flip_time[k]=0;
	walk_time[k]=0;
	flipped[k]=0;
      }
    }
    initialize();
    clause_value();
    
    if (zerodommage_vars_stack_fill_pointer>0) {
      index=random_integer(zerodommage_vars_stack_fill_pointer);
      var_to_flip=zerodommage_vars_stack[index];
    }
    else 
    if (decreasing_vars_stack_fill_pointer>0) {
      index=random_integer(decreasing_vars_stack_fill_pointer);
      var_to_flip=decreasing_vars_stack[index];
      // var_to_flip=choose_best_decreasing_var();
    }
    else var_to_flip=NONE;
    for (j=0;j<MAXSTEPS;j++) {
      flag=TRUE;
      if (walk_satisfiable()) {
	SAT=TRUE;
	break;
      }
      // var_to_flip=choose_var_by_random_walk(flipped_var, nbminima);
      //if (j==990)
      //	printf("sjfh");
      if (var_to_flip==NONE) {// when there is no non-tabu decreasing var 
	nbwalk++; 
	var_to_flip=choose_var_by_random_walk();
	flag=FALSE; 
      }
      // saved=MY_CLAUSE_STACK_fill_pointer;
      var_current_value[var_to_flip]=1-var_current_value[var_to_flip]; 
      check_implied_clauses(var_to_flip, var_current_value[var_to_flip], j);
      eliminate_satisfied_clauses();
      flip_time[var_to_flip]=j;
      // flipped_var=var_to_flip;
      var_to_flip=update_gradient_and_choose_flip_var(var_to_flip);
      // check_gradient(flag, flipped_var, saved );
      if ( MY_CLAUSE_STACK_fill_pointer<min[i])
	min[i]= MY_CLAUSE_STACK_fill_pointer;
      depth+=MY_CLAUSE_STACK_fill_pointer;
    }
    if (SAT==TRUE) {
      nb_suc++;
      clause_value();
      total_nb_flip+=j;
      if (!walk_satisfiable())
	printf("I'AM SORRY SOMETHING IS WRONG\n");
    }
    avgdepth=depth/(double)j;
    if (min[i]>0) {total_min += min[i]; total_last+=MY_CLAUSE_STACK_fill_pointer;}
    total_nbwalk+=nbwalk;
    if (SAT==TRUE)
      verify=verify_sol_input(input_file);
    else verify=0;
    printf("\n %4d %6d %9d %9d %10.3lf %11.2lf %6d\n", 
	   min[i], MY_CLAUSE_STACK_fill_pointer, j, nbwalk,
	   avgdepth, ((double)(nb_suc*100))/(double)(i+1), verify);
    avgdepths+=avgdepth; 
  }
  mess=times(a_tms); endtime = a_tms->tms_utime;
  
  printf("\n****success Rate=%5.2lf****\n", ((double)(nb_suc*100))/(double)MAXTRIES);
  printf("g2wsat2005-%d-%d-%d-%d %s %5.3f %5.2lf %d %d %d %d %5.3lf %d %d\n", 
	 NOISE, LNOISE, NB_VAR, INIT_NB_CLAUSE,
	 INPUT_FILE, ((double)(endtime-begintime)/CLK_TCK), 
	 ((double)(nb_suc*100))/(double)MAXTRIES, MAXTRIES, 
	 ((nb_suc>0) ? (int)(total_nb_flip/nb_suc) : 0), MAXSTEPS, 
	 (int)total_nbwalk/MAXTRIES, 
	 avgdepths/MAXTRIES, (int)total_min/MAXTRIES, (int)total_last/MAXTRIES);
  fp_time = fopen("result-table", "a");
  fprintf(fp_time, 
	  "g2wsat2005-%d-%d-%d-%d %s %5.3f %5.2lf %d %d %d %d %5.3lf %d %d\n", 
	  NOISE, LNOISE, NB_VAR, INIT_NB_CLAUSE,
	  INPUT_FILE, ((double)(endtime-begintime)/CLK_TCK), 
	  ((double)(nb_suc*100))/(double)MAXTRIES, MAXTRIES, 
	  ((nb_suc>0) ? (int)(total_nb_flip/nb_suc) : 0), MAXSTEPS, 
	  (int)(total_nbwalk/MAXTRIES), 
	  avgdepths/MAXTRIES, (int)total_min/MAXTRIES, (int)total_last/MAXTRIES);
  fclose(fp_time);
  printf ("Program terminated in %5.3f seconds.\n",
	  ((double)(endtime-begintime)/CLK_TCK));
}

void scanone(int argc, char *argv[], int i, int *varptr) {
  if (i>=argc || sscanf(argv[i],"%i",varptr)!=1){
    fprintf(stderr, "Bad argument %s\n", i<argc ? argv[i] : argv[argc-1]);
    exit(-1);
  }
}

int HELP_FLAG=FALSE;

void parse_parameters(int argc,char *argv[]) {
  int i, temp, j;
  if (argc<2)
    HELP_FLAG=TRUE;
  else 
    for (i=1;i < argc;i++) {
      if (strcmp(argv[i],"-seed") == 0) {
	scanone(argc,argv,++i,&SEED);
	SEED_FLAG=TRUE; 
      }
      else if (strcmp(argv[i],"-cutoff") == 0)
	scanone(argc,argv,++i,&MAXSTEPS);
      else if (strcmp(argv[i],"-tries") == 0 || strcmp(argv[i],"-restart") == 0) 
	scanone(argc,argv,++i,&MAXTRIES);
      else if (strcmp(argv[i], "-s")==0)
	BUILD_FLAG=FALSE;
      else if (strcmp(argv[i], "-noise")==0)
	scanone(argc, argv, ++i,&NOISE);
      else if (strcmp(argv[i], "-lnoise")==0)
	scanone(argc, argv, ++i,&LNOISE);
      else if (strcmp(argv[i], "-dp")==0)
	scanone(argc, argv, ++i,&LNOISE);
      else if (strcmp(argv[i], "-help")==0)
	HELP_FLAG=TRUE;
      else   
	for (j=0; j<WORD_LENGTH; j++) {
	  INPUT_FILE=argv[i];
	  saved_input_file[j]=INPUT_FILE[j];
	}
    }
}

main(int argc, char *argv[]) {
  int i,  var; 

  parse_parameters(argc,argv);
  if (HELP_FLAG==TRUE) {
    printf("using the following parameters (the order does not matter)\n\n");
    printf("your input file\n");
    printf("-cutoff N: N is the maxmum flips before restart\n");
    printf("-restart N, -tries N: N is the number of restarts\n");
    printf("-noises P: P is the noise (the propability will be P/100)\n");
    printf("-dp DP: DP is the Diversification Probability(=DP/100)\n");
    printf("-help: the current help message\n");
  }
  else 
    switch (build(BUILD_FLAG, INPUT_FILE)) {
    case FALSE: printf("Input file error\n"); return FALSE;
    case SATISFIABLE:     
      VARIABLE_STACK_fill_pointer=0;
      CLAUSE_STACK_fill_pointer = 0;
      MANAGEDCLAUSE_STACK_fill_pointer = 0;
      NB_CLAUSE=0;
      break;
    case TRUE:
      VARIABLE_STACK_fill_pointer=0;
      CLAUSE_STACK_fill_pointer = 0;
      MANAGEDCLAUSE_STACK_fill_pointer = 0;
      T_SEUIL= 0; 
      search(INPUT_FILE);
      break;
    case NONE: printf("An empty resolvant is found!\n"); break;
    }
  return TRUE;
}