/****************************************************************************/
/* based on eqsatz19.c, suppressing the stacks "pbete_node->dself...        */
/*                                                                          */
/*                                                                          */
/*                                                                          */
/*                    Author: Chu Min LI (cli@laria.u-picardie.fr)          */
/*                    Copyright LaRIA, Universite de Picardie Jules Verne   */
/*                    September 1996                                        */
/****************************************************************************/

/* integrating equivalent class size treatment    */

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

typedef signed int my_type;
typedef unsigned int my_unsigned_type;

#define DYNAMIQUE_SIZE 256
#define WORD_LENGTH 200
#define TRUE 1
#define FALSE 0
#define NONE -1

#define WEIGTH 5
#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  200000
#define tab_variable_size_plus_1 tab_variable_size+1
#define tab_clause_size 900000
#define tab_clause_size_plus_1 tab_clause_size+1
#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 get_var_from_lit1(negative_literal) lit_var[negative_literal]

#define RESOLVANT_LENGTH 3
#define RESOLVANT_SEARCH_THRESHOLD 5000
#define complement(lit1, lit2) \
((lit1<lit2) ? lit2-lit1==NB_VAR : lit1-lit2==NB_VAR)

#define pop(stack) stack[--stack ## _fill_pointer]
#define push(item, stack) stack[stack ## _fill_pointer++] = item
#define unit_clause(clause) clause_length[clause] == 1

#define dolist(ppointer, pend, begin, end)                                  \
          for(ppointer = begin, pend = end; ppointer != pend; ppointer++)


#define empty_vector(pstack) pstack ## _fill_pointer == 0

#define satisfiable() CLAUSE_STACK_fill_pointer == NB_CLAUSE

#define NEGATIVE 0
#define POSITIVE 1
#define PASSIVE 0
#define ACTIVE 1
#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];
/* my_unsigned_type neg_nb[tab_variable_size];
my_unsigned_type 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];

int reduce_if_negative_nb[tab_variable_size];
int reduce_if_positive_nb[tab_variable_size];

int *sat[tab_clause_size];
my_type clause_state[tab_clause_size];
my_unsigned_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 IMPLIED_LITS_fill_pointer=0;

int VARIABLE_STACK[tab_variable_size];
int CLAUSE_STACK[tab_clause_size];
int UNITCLAUSE_STACK[tab_clause_size];
int MANAGEDCLAUSE_STACK[double_tab_clause_size];
int IMPLIED_LITS[tab_variable_size];
/*
int MY_VARIABLE_STACK[tab_variable_size];
int MY_CLAUSE_STACK[tab_clause_size];
int MY_UNITCLAUSE_STACK[tab_clause_size];
int MY_MANAGEDCLAUSE_STACK[double_tab_clause_size];
*/
int TESTED_VAR_STACK[tab_variable_size];
int TESTED_VAR_STACK_fill_pointer=0;

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

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

my_type MAYBE_SATISFIABLE = TRUE;
/*
int MY_VARIABLE_STACK_fill_pointer = 0;
int MY_CLAUSE_STACK_fill_pointer = 0;
int MY_UNITCLAUSE_STACK_fill_pointer = 0;
int MY_MANAGEDCLAUSE_STACK_fill_pointer = 0;
*/
/* int CLASS_VAR_STACK[tab_variable_size];
int CLASS_VAR_STACK_fill_pointer=0; */

#define double_tab_literal_size 5*tab_literal_size
#define tab_bete_size tab_clause_size/4
#define tab_pair_size ((tab_bete_size/2<1000) ? 1000 : tab_bete_size/2)
#define BACK_POINT -2

int VALUE_STACK[double_tab_literal_size];
int VALUE_STACK_fill_pointer=0;
int BETE_STACK[tab_bete_size];
int BETE_STACK_fill_pointer=0;
int EQUI_STACK[tab_pair_size][2];
int EQUI_STACK_fill_pointer=0;
int saved_value_stack[tab_variable_size];
int saved_bete_stack[tab_variable_size];
/* int class_flag[tab_literal_size];
 */
int lit_var[tab_literal_size];
int lit_com[tab_literal_size];

int saved_previous_managedclause_stack[tab_variable_size];
int saved_previous_bete_stack[tab_variable_size];

int TREATING_CLASS_STACK_fill_pointer=0;
int TREATING_CLASS_STACK[tab_pair_size];
int grey[tab_literal_size];

/*
#define my_get_lit_class_var(lit)\
((lit_class[lit]==NONE) ? lit : lit_var[get_lit_class1(lit)])
*/

#define my_get_lit_class(lit)\
((lit_class[lit]==NONE) ? lit : get_lit_class1(lit))

int BACK= TRUE;

struct bete_node {
  int mate1;
  int mate2;
  int self;
  int bete;
  struct bete_node *next;
};

struct bete_node *in_bete[tab_variable_size];

int class_of[tab_literal_size];
int lit_class[tab_literal_size];
int class_size[tab_literal_size];

int betes[tab_bete_size][3];
int bete_state[tab_bete_size];
int bete_sign[tab_bete_size];
int bete_clauses[tab_bete_size][4];
int NB_BETE=0;
long STATIC_NB_BETE=0;
long TOTAL_NB_BETE=0;
int PREVIOUS_MANAGEDCLAUSE_STACK_fill_pointer = 0;
int PREVIOUS_BETE_STACK_fill_pointer=0;
int saved_nb_bete[tab_variable_size];
int nb_bete[tab_variable_size];

int EQ1[tab_pair_size][2];
int EQ2[tab_pair_size][2];
int EQ1_fill_pointer=0;
int EQ2_fill_pointer=0;
int BETE_TO_ADD[tab_pair_size][3];
int BETE_TO_ADD_fill_pointer=0;
int LIT_IMPLIED[tab_literal_size];
int bete_involving[tab_bete_size];
int bete_tab1[tab_bete_size];
int bete_tab1_fill_pointer=0;

struct bete_node *involved_in_bete[tab_variable_size];
/* int bete_involved[tab_bete_size];
 int bete_tab[tab_bete_size]; */
int var_tab[tab_variable_size];
/* int bete_tab_fill_pointer=0; */
int var_tab_fill_pointer=0;
/*
int MY_VALUE_STACK[double_tab_literal_size];
int MY_VALUE_STACK_fill_pointer=0;
int MY_BETE_STACK[tab_bete_size];
int MY_BETE_STACK_fill_pointer=0;
*/
int get_lit_class(int lit) {
  for(; lit_class[lit]!=NONE; lit=lit_class[lit]);
  return lit;
}

int get_lit_class1(int lit) {
  for(lit=lit_class[lit]; lit_class[lit]!=NONE; lit=lit_class[lit]);
  return lit;
}

int get_first_lit_of_class(int class) {
  for(; class_of[class]!=NONE; class=class_of[class]);
  return class;
}

void remove_clauses(int *clauses) {
   int clause;
   for(clause=*clauses; clause!=NONE; clause=*(++clauses)) {
     if (clause_state[clause] == ACTIVE) {
        clause_state[clause] = PASSIVE;
        push(clause, CLAUSE_STACK);
     }
  }
}

int manage_clauses(register int *clauses) {
   int clause;
   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(register int *clauses) {
   int clause;
   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 print_values(int nb_var, char *input_file) {
    FILE* fp_out; char output_file_name[WORD_LENGTH];
    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, class1, opp_class1, i;
      
   UNITCLAUSE_STACK_fill_pointer = 0; NB_BACK++; BACK=TRUE;
   do {
     var = pop(VARIABLE_STACK);
     if (var==NONE) return FALSE;
     switch(var_rest_value[var]) {
     case NONE: var_state[var] = ACTIVE; break;
     case BACK_POINT: var_state[var] = ACTIVE; break;
     default:
          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_length[MANAGEDCLAUSE_STACK[index]]++;
	  }
          MANAGEDCLAUSE_STACK_fill_pointer = saved_managedclause_stack[var];

          for ( i=VALUE_STACK_fill_pointer;
		i>saved_value_stack[var];) {
	    class_of[VALUE_STACK[--i]]=NONE;
	    class_of[VALUE_STACK[--i]]=NONE;
	    opp_class1=VALUE_STACK[--i];
	    class1=VALUE_STACK[--i];
	    class_size[lit_class[opp_class1]]-=class_size[opp_class1];
	    class_size[lit_class[class1]]-=class_size[class1];
	    
	    lit_class[opp_class1]=NONE;
	    lit_class[class1]=NONE;
	  }
	  VALUE_STACK_fill_pointer=saved_value_stack[var];

	  for (index = saved_bete_stack[var]; 
               index < BETE_STACK_fill_pointer;
               index++)
             bete_state[BETE_STACK[index]] = ACTIVE;
          BETE_STACK_fill_pointer = saved_bete_stack[var];

	  for (index = saved_nb_bete[var];
	       index<NB_BETE;
	       index++) 
	    remove_link_for_bete(index);
	  NB_BETE=saved_nb_bete[var];

    
    PREVIOUS_MANAGEDCLAUSE_STACK_fill_pointer=
      saved_previous_managedclause_stack[var];
    PREVIOUS_BETE_STACK_fill_pointer=saved_previous_bete_stack[var];

	  var_state[var]=ACTIVE;

	  if (var_rest_value[var]==TRUE) {
	    if (satisfy_var_and_simplify_clauses_for_class(var, 
                                BACK_POINT)==NONE) 
	      var_state[var]=ACTIVE;
	    else return TRUE;
	  }
	  else {
	    if (falsify_var_and_simplify_clauses_for_class(var, 
                                BACK_POINT)==NONE) 
	      var_state[var]=ACTIVE;
	    else 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
/*
#define smaller_than(lit1, lit2) lit_var[lit1]<lit_var[lit2]
*/
int smaller_than(int lit1, int lit2) {
    return ((lit1<NB_VAR) ? lit1 : lit1-NB_VAR) < 
      ((lit2<NB_VAR) ? lit2 : lit2-NB_VAR);
}

#define get_complement(lit) lit_com[lit]

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

my_type get_resolvant(int *clause1, int *clause2, int *resolvant) {
    int lit1, lit2, nb_diff1=0,  nb_diff2=0,
      nb_iden=0, nb_opps=0, j1=0, j2=0, j, limited_length;

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

       if (nb_diff1 + nb_diff2 + nb_iden <= limited_length) {
          j1=0; j2=0; j=0;
          while (((lit1 = clause1[j1])!=NONE) && 
		 ((lit2 = clause2[j2]) != NONE)) {
             if (lit1 == lit2) {
                resolvant[j] = lit1; j1++; j2++; j++;
             }
             else 
             if (smaller_than(lit1, lit2)) {
                resolvant[j] = lit1; j1++; j++;
             }
             else
             if (smaller_than(lit2, lit1)) {
                resolvant[j] = lit2; j2++; j++;
             }
             else {
                j1++; j2++;
             }
          }
          if (clause1[j1] ==NONE) 
	    while ((resolvant[j++] = clause2[j2++]) != NONE);
          else while ((resolvant[j++] = clause1[j1++]) != NONE);
          if (j==0) return NONE;
          if (nb_diff2==0) return 2; /* clause1 is redundant */
          return TRUE;
       }
    }
    return FALSE;
}

void remove_link(int clause) {
   int lit;
   int *lits;
   struct node *pnode1, *pnode2, *pnode;

   lits = sat[clause];

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

void set_link(int clause) {
   int lit;
   int *lits;
   struct node *pnode1, *pnode2, *pnode;

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

void set_link_for_resolv(int resolv) {
   int lit, *lits;
   struct node *pnode;
   lits=sat[resolv];
   for (lit=*lits; lit != NONE; lit=*(++lits)) { 
       pnode = allocate_node();
       pnode->clause = resolv;
	   pnode->next=in_resolv[lit];
	   in_resolv[lit]=pnode;
   }
}

void remove_link_for_resolv(int resolv) {
	int lit, *lits;
   struct node *pnode1, *pnode2, *pnode;

   lits = sat[resolv];
   for (lit=*lits; lit != NONE; lit=*(++lits)) { 
       pnode = in_resolv[lit];
       if (pnode == NULL) return;
       if (pnode->clause == resolv) 
		  in_resolv[lit] = pnode->next;
       else
       for (pnode1 = pnode, pnode2 = pnode->next;
            pnode2 != NULL; pnode2=pnode2->next) {
         if (pnode2->clause == resolv) {
            pnode1->next = pnode2->next;
            break;
         }
         else
            pnode1 = pnode2;
       }
   }
}

int *INVOLVED_CLAUSE_STACK;
int INVOLVED_CLAUSE_STACK_fill_pointer=0;
int *CLAUSE_INVOLVED;

int already_present(int *resolvant) {
	int lit, *lits, clause, length=0, i;
	struct node *pnode, *pnode1;
	lits=resolvant;
	for (lit=*lits; lit != NONE; lit=*(++lits)) {
		length++;
		for (pnode=in_resolv[lit]; pnode != NULL; pnode=pnode->next) {
			clause=pnode->clause;
			CLAUSE_INVOLVED[clause]++;
			if (CLAUSE_INVOLVED[clause]==1)
				push(clause, INVOLVED_CLAUSE_STACK);
			if (clause_length[clause]==CLAUSE_INVOLVED[clause]) {
				for(i=0; i<INVOLVED_CLAUSE_STACK_fill_pointer; i++) 
					CLAUSE_INVOLVED[INVOLVED_CLAUSE_STACK[i]]=0;
				INVOLVED_CLAUSE_STACK_fill_pointer=0;
				return NEW_CLAUSE_REDUNDANT;
			}
		}
	}
	for(i=0; i<INVOLVED_CLAUSE_STACK_fill_pointer; i++) {
		clause=INVOLVED_CLAUSE_STACK[i];
		if ((length==CLAUSE_INVOLVED[clause]) && (length<clause_length[clause])){
			clause_state[clause] = PASSIVE;
			remove_link(clause);
			remove_link_for_resolv(clause);
		}
		CLAUSE_INVOLVED[clause]=0;
	}
	INVOLVED_CLAUSE_STACK_fill_pointer=0;
	return FALSE;
}

int search_redundence(int *lits) {
   int lit, is_red;
   int *old_lits, *new_lits;
   struct node *pnode, *pnode1;

   /* if lits is unit, all clauses in the pnode list become redundant and
   will be deleted, so that pnode=pnode->next is not good */
   new_lits = lits;
   for (lit=*lits; lit != NONE; lit=*(++lits)) { 
     for (pnode = (positive(lit) ? node_pos_in[lit] : 
                                   node_neg_in[get_var_from_lit(lit)]);
          pnode != NULL; pnode = pnode1) {
       pnode1=pnode->next;
       old_lits = sat[pnode->clause];
       is_red = redundant(new_lits, old_lits);
       if (is_red == OLD_CLAUSE_REDUNDANT) {
/*          printf("old clause %d is redundant\n", 
                 pnode->clause);
*/
          clause_state[pnode->clause] = PASSIVE;
          remove_link(pnode->clause);
       }
       else
       if (is_red == NEW_CLAUSE_REDUNDANT) {
          return NEW_CLAUSE_REDUNDANT;
       }
     }
  }
  return FALSE;  
}

int add_resolvant(int *lits) {
   int j, lit, is_red, resolvant[RESOLVANT_LENGTH+1];
   my_type is_res;
   int *old_lits, *new_lits, *res;
   struct node *pnode, *pnode1;

   /* if lits is unit, all clauses in the pnode list become redundant and
      will be deleted, so that pnode=pnode->next is not good */
   new_lits = lits;
   for (lit=*lits; lit != NONE; lit=*(++lits))
     for (pnode = (positive(lit) ?
                  node_neg_in[lit] :
                  node_pos_in[get_var_from_lit(lit)]);
          pnode != NULL; pnode = pnode1) {
        pnode1=pnode->next;
        old_lits = sat[pnode->clause];
        is_res = get_resolvant(new_lits, old_lits, resolvant);
        if (is_res == NONE) return NONE;
        if (is_res != FALSE) {
          is_red=search_redundence(resolvant);
          if (is_red != NEW_CLAUSE_REDUNDANT) {
			 if (already_present(resolvant) == FALSE) { 
				 res=(int *)malloc((RESOLVANT_LENGTH+1)*sizeof(int));
				 clause_state[NB_CLAUSE]=ACTIVE;      
				 j=0;
				 while ((res[j]=resolvant[j]) != NONE) ++j;
				 if (j==0) return NONE;
				 sat[NB_CLAUSE] = res; 
				 set_link_for_resolv(NB_CLAUSE);
				 clause_length[NB_CLAUSE++]=j;
			 }
			 /* new_lits is redundant by resolvant */
			 if (is_res == 2) return 2;
          }
        }
      }
   return TRUE;
}

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

    pnode=node_in;
    while (pnode != NULL) {
      if (clause_state[pnode->clause]==ACTIVE) j++; 
      pnode = pnode->next;
    }
    in = (int *)malloc((j+1)*sizeof(int));
    j=0; pnode=node_in; 
    while (pnode != NULL) {
      if (clause_state[pnode->clause]==ACTIVE) {
        in[j] = pnode->clause; j++; 
      }
      pnode = pnode->next; 
    }
    in[j] = NONE;
    return in;
}
   
my_type build_sat_instance(char *input_file) {
   FILE* fp_in=fopen(input_file, "r");
   char ch, tautologie, word1[WORD_LENGTH], word2[WORD_LENGTH];
   int endln, germe, i, j, index, length, ii, jj, lit1, is_red,
       lits[tab_variable_size], *plit, *lits1, lit, var, *clause,
       NB_CLAUSE1, is_res;

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

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

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

   INIT_NB_CLAUSE= NB_CLAUSE;
   
     for(i=0; i<NB_CLAUSE; i++) 
	   set_link_for_resolv(i);

   CLAUSE_INVOLVED=(int *)malloc((tab_clause_size)*sizeof(int));
   INVOLVED_CLAUSE_STACK=(int *)malloc((tab_clause_size)*sizeof(int));
   for(i=0; i<tab_clause_size; i++) 
	   CLAUSE_INVOLVED[INVOLVED_CLAUSE_STACK[i]]=0;
   INVOLVED_CLAUSE_STACK_fill_pointer=0;
  
   for(i=0; i<NB_CLAUSE; i++) {
      plit = sat[i];
      length = clause_length[i];          
      if (length==1) push(i, UNITCLAUSE_STACK);
      if (search_redundence(plit) != NEW_CLAUSE_REDUNDANT) {
         is_res = add_resolvant(plit);
         if (is_res  == NONE) return NONE;
	 else 
         if (is_res == 2) clause_state[i] = PASSIVE;
	 else {
	   set_link(i);
	 }
      }
      else clause_state[i] = PASSIVE;
   }
   NB_CLAUSE1 = 0; TOTAL_NB_CLAUSE=NB_CLAUSE;
   for (i=0; i<NB_CLAUSE; i++) {
     if (clause_state[i] == ACTIVE) NB_CLAUSE1++;
   }
   NB_CLAUSE = NB_CLAUSE1;

   for(i=0; i<NB_VAR; i++) {
      neg_in[i]=copy_clauses(node_neg_in[i]);
      pos_in[i]=copy_clauses(node_pos_in[i]);
   }
   free_ressources();
   free(CLAUSE_INVOLVED);
   free(INVOLVED_CLAUSE_STACK);
   return TRUE;
}

my_type build_simple_sat_instance(char *input_file) {
   FILE* fp_in=fopen(input_file, "r");
   char ch, word1[WORD_LENGTH], word2[WORD_LENGTH];
   int endln, i, j, ii, jj, index, length, tautologie,
       lits[tab_variable_size], *lits1, lit, lit1, var;

   if (fp_in == NULL) return FALSE;

   fscanf(fp_in, "%c", &ch);
  while (ch!='p') {
    while (ch!='\n') fscanf(fp_in, "%c", &ch);  
    fscanf(fp_in, "%c", &ch);
  }
  
   fscanf(fp_in, "%s%d%d", word2, &NB_VAR, &NB_CLAUSE);
   INIT_NB_CLAUSE = NB_CLAUSE;
      
   for (i=0; i<NB_VAR; i++) {
       nb_neg_clause_of_length3[i] = 0;
       nb_pos_clause_of_length3[i] = 0;
       nb_neg_clause_of_length2[i] = 0;
       nb_pos_clause_of_length2[i] = 0;
   }
   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]; lits[length] = 0;
               printf("literal %d is redundant in clause %d\n", lit, i);
            }
            else
            if (abs(lit) == 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) {
	    var=abs(lits[j]) - 1;
	    nb_neg_clause_of_length3[var]++;
            if (length==1) push(i, UNITCLAUSE_STACK);
	    sat[i][j] = var + NB_VAR ;
	  }
	  else {
	    var= lits[j]-1;
	    sat[i][j] = var;
	    nb_pos_clause_of_length3[var]++;
	    if (length==1) push(i, UNITCLAUSE_STACK);
	  }
	}
	if (length==2) push(i, MANAGEDCLAUSE_STACK);
	clause_length[i]=length;
	clause_state[i] = ACTIVE;
	sat[i][length]=NONE;
      }
   }
   fclose(fp_in);
 
   for (i=0; i<NB_VAR; i++) { 

      neg_in[i] = (int *)
	          malloc((nb_neg_clause_of_length3[i]+1) * sizeof(int));
      pos_in[i] = (int *)
	          malloc((nb_pos_clause_of_length3[i]+1) * sizeof(int));
      neg_in[i][nb_neg_clause_of_length3[i]]=NONE;
      pos_in[i][nb_pos_clause_of_length3[i]]=NONE;
      nb_neg_clause_of_length3[i] = 0;
      nb_pos_clause_of_length3[i] = 0;
      var_state[i] = ACTIVE;
   }   
   for (i=0; i<NB_CLAUSE; i++) {
      lits1 = sat[i];
      for(lit=*lits1; lit!=NONE; lit=*(++lits1)) {
	 if (positive(lit)) 
            pos_in[lit][nb_pos_clause_of_length3[lit]++] = i;
	 else
            neg_in[get_var_from_lit(lit)]
                  [nb_neg_clause_of_length3[get_var_from_lit(lit)]++] = i;
      }
   }
   return TRUE;
}

int verify_solution() {
   int i, j, lit, *lits, clause_truth;

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

   return TRUE;
}

int reset_unitclauses(int begin) {
  int i;
  for (i=begin; i<UNITCLAUSE_STACK_fill_pointer; i++) 
     clause_length[UNITCLAUSE_STACK[i]]++;
}

long NB_SEARCH = 0; long NB_FIXED = 0;
  
int unitclause_process() {
  int var, i, j, unitclause, clause, lit, *lits, unitclause_position, class;
  
  for (unitclause_position = 0; 
       unitclause_position < UNITCLAUSE_STACK_fill_pointer;
       unitclause_position++) {
    unitclause = UNITCLAUSE_STACK[unitclause_position];
    if (clause_state[unitclause] == ACTIVE) {
      NB_UNIT++; 
      lits = sat[unitclause];
      for(lit=*lits; lit!=NONE; lit=*(++lits)) {
        if (positive(lit)) var=lit; else var=get_var_from_lit(lit);
        if (var_state[var]==ACTIVE) {
          class=get_lit_class(lit);
          if (positive(class)) {
	    if (satisfy_var_and_simplify_clauses_for_class(class, NONE)==NONE){
	      return NONE;
            } 
            else
	      break;
	  }
          else {
            if (falsify_var_and_simplify_clauses_for_class(
get_var_from_lit(class), NONE)==NONE) {
              return NONE;
            }
            else
	      break;
          }
        }
      }
    }
  }
  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 clause) {
  int *lits;
  int lit, var, i, resolvant_nb=0;
       
  lits = sat[clause];
  for(lit=*lits; lit!=NONE; lit=*(++lits)) {
     if (positive(lit)) {
        var = lit;
        if (var_state[var] == ACTIVE)
          resolvant_nb += (nb_neg_clause_of_length2[var] * WEIGTH)+ 
                           nb_neg_clause_of_length3[var];
     }
     else {
        var = get_var_from_lit(lit);
        if (var_state[var] == ACTIVE) 
           resolvant_nb += (nb_pos_clause_of_length2[var] * WEIGTH)+ 
                           nb_pos_clause_of_length3[var];
     }
  }
  return resolvant_nb;
}

void reset_context(int saved_variable_stack_fill_pointer,
		   int saved_clause_stack_fill_pointer,
		   int saved_managedclause_stack_fill_pointer,
		   int saved_value_stack_fill_pointer,
		   int saved_bete_stack_fill_pointer) {
   int i, tested_var, class1, opp_class1;

   UNITCLAUSE_STACK_fill_pointer = 0;

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

   for (i=saved_clause_stack_fill_pointer; 
	i<CLAUSE_STACK_fill_pointer; i++)
       clause_state[CLAUSE_STACK[i]] = ACTIVE;
   CLAUSE_STACK_fill_pointer = saved_clause_stack_fill_pointer;

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

   for (i=VALUE_STACK_fill_pointer;
	i>saved_value_stack_fill_pointer; ) {
    class_of[VALUE_STACK[--i]]=NONE;
    class_of[VALUE_STACK[--i]]=NONE;
    opp_class1=VALUE_STACK[--i];
    class1=VALUE_STACK[--i];
    class_size[lit_class[opp_class1]]-=class_size[opp_class1];
    class_size[lit_class[class1]]-=class_size[class1];

    lit_class[opp_class1]=NONE;
    lit_class[class1]=NONE;
  }
  VALUE_STACK_fill_pointer=saved_value_stack_fill_pointer;
  
  for (i = saved_bete_stack_fill_pointer; 
       i < BETE_STACK_fill_pointer;
       i++)
    bete_state[BETE_STACK[i]] = ACTIVE;
  BETE_STACK_fill_pointer = saved_bete_stack_fill_pointer;
}

int examine1(int tested_var) {
  int i, generating_if_positif = 0, generating_if_negatif = 0, var, mesure,
    nb_reduced_betes, nb_managed_clauses, nb_fixed_var, nb_removed_clauses,
    saved_variable_stack_fill_pointer, saved_clause_stack_fill_pointer,
    saved_managedclause_stack_fill_pointer, saved_value_stack_fill_pointer,
    saved_bete_stack_fill_pointer;

  saved_variable_stack_fill_pointer=VARIABLE_STACK_fill_pointer;
  saved_clause_stack_fill_pointer=CLAUSE_STACK_fill_pointer;
  saved_managedclause_stack_fill_pointer=MANAGEDCLAUSE_STACK_fill_pointer;
  saved_value_stack_fill_pointer=VALUE_STACK_fill_pointer;
  saved_bete_stack_fill_pointer=BETE_STACK_fill_pointer;
  
  init_for_preprocess();
 PREVIOUS_MANAGEDCLAUSE_STACK_fill_pointer=MANAGEDCLAUSE_STACK_fill_pointer;
  generating_if_positif=
    my_satisfy_var_and_simplify_clauses_for_class(tested_var);
  if (generating_if_positif != NONE) {
    generating_if_positif = branch();
    if (generating_if_positif !=NONE) {
      nb_managed_clauses=MANAGEDCLAUSE_STACK_fill_pointer-
	                 saved_managedclause_stack_fill_pointer;
      nb_reduced_betes=BETE_STACK_fill_pointer-
	               saved_bete_stack_fill_pointer;
      nb_fixed_var=VARIABLE_STACK_fill_pointer-
	           saved_variable_stack_fill_pointer;
      nb_removed_clauses=CLAUSE_STACK_fill_pointer-
	                 saved_clause_stack_fill_pointer;
      generating_if_positif=
	get_mesure1(saved_managedclause_stack_fill_pointer,
		    saved_variable_stack_fill_pointer,
		    saved_value_stack_fill_pointer,
		    saved_bete_stack_fill_pointer);
      if (generating_if_positif !=NONE) {
	reduce_if_positive_nb[tested_var]=generating_if_positif;
      }
    }
  }
  reset_context(saved_variable_stack_fill_pointer, 
		saved_clause_stack_fill_pointer,
		saved_managedclause_stack_fill_pointer, 
		saved_value_stack_fill_pointer,
		saved_bete_stack_fill_pointer);
  if (generating_if_positif == NONE) {
    if (falsify_var_and_simplify_clauses_for_class(tested_var, NONE)==NONE)
      return NONE;
    else  
    if (unitclause_process()==NONE) return NONE;
    else
    if (set_equivalencies()==NONE) return NONE;
    else return FALSE;
  }
  if ((EQ2_fill_pointer==0) &&
      (nb_fixed_var==class_size[tested_var]) &&
      (nb_removed_clauses==nb_managed_clauses)) {
    reduce_if_negative_nb[tested_var]=reduce_if_positive_nb[tested_var];
  }
  else {
    for(i=0; i<EQ2_fill_pointer; i++) {
      EQ1[i][0]=EQ2[i][0]; EQ1[i][1]=EQ2[i][1];
    }
    EQ1_fill_pointer=EQ2_fill_pointer; EQ2_fill_pointer=0;

    generating_if_negatif=
      my_falsify_var_and_simplify_clauses_for_class(tested_var);
    if (generating_if_negatif != NONE) {
      generating_if_negatif = branch();
      if (generating_if_negatif !=NONE) {
	generating_if_negatif=
	  get_mesure1(saved_managedclause_stack_fill_pointer,
		      saved_variable_stack_fill_pointer,
		      saved_value_stack_fill_pointer,
		      saved_bete_stack_fill_pointer);
	if (generating_if_negatif !=NONE) {
	  reduce_if_negative_nb[tested_var]=generating_if_negatif;
	}
      }
    }
    reset_context(saved_variable_stack_fill_pointer, 
		  saved_clause_stack_fill_pointer,
		  saved_managedclause_stack_fill_pointer, 
		  saved_value_stack_fill_pointer,
		  saved_bete_stack_fill_pointer);
    if (generating_if_negatif == NONE) {
      if (satisfy_var_and_simplify_clauses_for_class(tested_var, NONE)==NONE) 
	return NONE;
      else
	if (unitclause_process()==NONE) return NONE;
	else
	  if (set_equivalencies()==NONE) return NONE;
	  else return FALSE;
    }
    if (treat_implied_lits(tested_var)==NONE) 
      return NONE;
    if (treat_implied_betes(tested_var)==NONE) 
      return NONE;
    if (PREVIOUS_MANAGEDCLAUSE_STACK_fill_pointer<
	MANAGEDCLAUSE_STACK_fill_pointer) {
      if (set_equivalencies()==NONE) return NONE;
      PREVIOUS_MANAGEDCLAUSE_STACK_fill_pointer=
	MANAGEDCLAUSE_STACK_fill_pointer;
    }
  }
  push(tested_var, TESTED_VAR_STACK);
  return TRUE;
}

int my_falsify_var_and_simplify_clauses(int var) {
  if (manage_clauses(pos_in[var])==TRUE) {
    var_current_value[var] = FALSE;
    var_state[var] = PASSIVE;
    push(var, VARIABLE_STACK);
    remove_bete_for_var(var);
    remove_clauses(neg_in[var]);
    return TRUE;
  }
  else return NONE;
}

int my_satisfy_var_and_simplify_clauses(int var) {
  if (manage_clauses(neg_in[var])==TRUE) {
    var_current_value[var] = TRUE;
    var_state[var] = PASSIVE;
    push(var, VARIABLE_STACK);
    remove_bete_for_var(var);
    remove_clauses(pos_in[var]);
    return TRUE;
  }
  else return NONE;
}

int my_falsify_var_and_simplify_clauses_for_class(int var) {
  int lit;

  if (my_falsify_var_and_simplify_clauses(var)==NONE)
    return NONE;
  for(lit=class_of[var]; lit != NONE; lit=class_of[lit]) {
    if (positive(lit)) {
      var=lit;
      if (my_falsify_var_and_simplify_clauses(var)==NONE)
	return NONE;
    }
    else {
      var=get_var_from_lit(lit);
      if (my_satisfy_var_and_simplify_clauses(var)==NONE)
	return NONE;
    }
  }
  return TRUE;
}

int my_satisfy_var_and_simplify_clauses_for_class(int var) {
  int lit;

  if (my_satisfy_var_and_simplify_clauses(var)==NONE)
    return NONE;
  for(lit=class_of[var]; lit != NONE; lit=class_of[lit]) {
    if (positive(lit)) {
      var=lit;
      if (my_satisfy_var_and_simplify_clauses(var)==NONE)
	return NONE;
    }
    else {
      var=get_var_from_lit(lit);
      if (my_falsify_var_and_simplify_clauses(var)==NONE)
	return NONE;
    }
  }
  return TRUE;
}

int branch() {
   int var, lit, *lits, unitclause, clause, unitclause_position, i, class;
  
   NB_SEARCH++;
  
   for (unitclause_position = 0;
        unitclause_position != UNITCLAUSE_STACK_fill_pointer;
        unitclause_position++) {
      unitclause = UNITCLAUSE_STACK[unitclause_position];
      if (clause_state[unitclause] == ACTIVE) {
	lits = sat[unitclause];
	for(lit=*lits; lit!=NONE; lit=*(++lits)) {
	  if (positive(lit)) var=lit; else var=get_var_from_lit(lit);
	  if (var_state[var]==ACTIVE) {
	    class=get_lit_class(lit);
	    if (positive(class)) {
	      if (my_satisfy_var_and_simplify_clauses_for_class(class)==NONE){
		NB_FIXED++;
		return NONE;
	      }
	      else break;
	    }
	    else {
	      if (my_falsify_var_and_simplify_clauses_for_class(
                     get_var_from_lit(class))==NONE) {
                NB_FIXED++;
                return NONE;
             }
             else break;
          }
        }
      }
    }
   }
   return MANAGEDCLAUSE_STACK_fill_pointer;
}

int get_neg_clause_nb(int* clauses, int class_var) {
  my_type neg_clause3_nb = 0, neg_clause2_nb = 0;
  int clause;

  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[class_var] += neg_clause2_nb;
  nb_neg_clause_of_length3[class_var] += neg_clause3_nb;
  return neg_clause2_nb;
}

int get_neg_clause_nb_for_class(int class_var) {
    int var, lit; 

    nb_neg_clause_of_length2[class_var]=0;
    nb_neg_clause_of_length3[class_var]=0;
    
    for(lit=class_var; lit != NONE; lit=class_of[lit]) {
      if (positive(lit)) {
        var=lit;
        get_neg_clause_nb(neg_in[var], class_var);
      }
      else {
        var=get_var_from_lit(lit);
        get_neg_clause_nb(pos_in[var], class_var);
      }
    }
   return nb_neg_clause_of_length2[class_var] +  
          nb_neg_clause_of_length3[class_var];
}

int get_pos_clause_nb(int* clauses, int class_var) {
  my_type pos_clause3_nb = 0, pos_clause2_nb = 0;
  int clause;

  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[class_var] += pos_clause2_nb;
  nb_pos_clause_of_length3[class_var] += pos_clause3_nb;
  return pos_clause2_nb;
}

int get_pos_clause_nb_for_class(int class_var) {
  int var, lit;

    nb_pos_clause_of_length2[class_var]=0;
    nb_pos_clause_of_length3[class_var]=0;

    for(lit=class_var; lit != NONE; lit=class_of[lit]) {
      if (positive(lit)) {
        var=lit;
        get_pos_clause_nb(pos_in[var], class_var);
      }
      else {
        var=get_var_from_lit(lit);
        get_pos_clause_nb(neg_in[var], class_var);
      }
    }
   return nb_pos_clause_of_length2[class_var] +  
          nb_pos_clause_of_length3[class_var];
}

int falsify_var_and_simplify_clauses(int var, int rest_value) {
  if (manage_clauses(pos_in[var])==TRUE) {
    var_current_value[var] = FALSE;
    var_rest_value[var] = rest_value;
    var_state[var] = PASSIVE;
    push(var, VARIABLE_STACK);
    remove_bete_for_var(var);
    remove_clauses(neg_in[var]);
    return TRUE;
  }
  else return NONE;
}

int satisfy_var_and_simplify_clauses(int var, int rest_value) {
  if (manage_clauses(neg_in[var])==TRUE) {
    var_current_value[var] = TRUE;
    var_rest_value[var] = rest_value;
    var_state[var] = PASSIVE;
    push(var, VARIABLE_STACK);
    remove_bete_for_var(var);
    remove_clauses(pos_in[var]);
    return TRUE;
  }
  else return NONE;
}

int falsify_var_and_simplify_clauses_for_class(int var, int rest_value) {
  int lit;

  if (falsify_var_and_simplify_clauses(var, rest_value)==NONE)
    return NONE;
  for(lit=class_of[var]; lit != NONE; lit=class_of[lit]) {
    if (positive(lit)) {
      var=lit;
      if (falsify_var_and_simplify_clauses(var, NONE)==NONE)
	return NONE;
    }
    else {
      var=get_var_from_lit(lit);
      if (satisfy_var_and_simplify_clauses(var, NONE)==NONE)
	return NONE;
    }
  }
  return TRUE;
}

int satisfy_var_and_simplify_clauses_for_class(int var, int rest_value) {
  int lit;

  if (satisfy_var_and_simplify_clauses(var, rest_value)==NONE)
    return NONE;
  for(lit=class_of[var]; lit != NONE; lit=class_of[lit]) {
    if (positive(lit)) {
      var=lit;
      if (satisfy_var_and_simplify_clauses(var, NONE)==NONE)
	return NONE;
    }
    else {
      var=get_var_from_lit(lit);
      if (falsify_var_and_simplify_clauses(var, NONE)==NONE)
	return NONE;
    }
  }
  return TRUE;
}

int search_clauses(int lit1, int lit2) {
  /* lit1 is smaller than lit2 */
  int clause;
  if (positive(lit2)) {
    clause=search_clause(lit1, pos_in[lit2]);
    if (clause != NONE) return clause;
  }
  else {
    clause=search_clause(lit1, neg_in[get_var_from_lit(lit2)]);
    if (clause != NONE) return clause;
  }
  return NONE;
}

int search_clause(int lit1, int* clauses) {
  int *lits, lit, clause, var;
  for(clause=*clauses; clause!=NONE; clause=*(++clauses)) {
    if ((clause_state[clause] == ACTIVE) && (clause_length[clause] == 2)) {
      lits=sat[clause];
      for(lit=*lits; lit!=NONE; lit=*(++lits)) {
        if (positive(lit)) var=lit; else var=get_var_from_lit(lit);
	if ((var_state[var] == ACTIVE) && (lit==lit1))
	  return clause;
      }
    }
  }
  return NONE;
}

void tri3(int *lit1, int *lit2, int *lit3) {
  int temp;
  
  if (smaller_than(*lit1, *lit2)) {
    if (smaller_than(*lit3, *lit2)) {
      temp=*lit3; *lit3=*lit2; *lit2=temp;
      if (smaller_than(*lit2, *lit1)) {
	temp=*lit1; *lit1=*lit2; *lit2=temp;
      }
    }
  }
  else 
  if (smaller_than(*lit2, *lit3)) {
    temp=*lit1; *lit1=*lit2; *lit2=temp;
    if (smaller_than(*lit3, *lit2)) {
      temp=*lit3; *lit3=*lit2; *lit2=temp;
    }
  }
  else {
    temp=*lit1; *lit1=*lit3; *lit3=temp;
  }
}

int same_var(int lit1, int lit2) {
  if (negative(lit1)) lit1=get_var_from_lit1(lit1);
  if (negative(lit2)) lit2=get_var_from_lit1(lit2);
  return (lit1==lit2);
}

int same_var1(int lit1, int var2) {
  if (negative(lit1)) lit1=get_var_from_lit1(lit1);
  return (lit1==var2);
}

int satisfy_class(int class) {
  if (positive(class)) {
    if (satisfy_var_and_simplify_clauses_for_class(class, NONE)==NONE)
      return NONE;
    else if (unitclause_process() == NONE) return NONE;
  }
  else {
    if (falsify_var_and_simplify_clauses_for_class(
	get_var_from_lit(class), NONE)==NONE)
      return NONE;
    else if (unitclause_process() == NONE) return NONE;
  }
  return TRUE;
}

int falsify_class(int class) {
  if (positive(class)) {
    if (falsify_var_and_simplify_clauses_for_class(class, NONE)==NONE)
      return NONE;
    else if (unitclause_process() == NONE) return NONE;
  }
  else {
    if (satisfy_var_and_simplify_clauses_for_class(
	get_var_from_lit(class), NONE)==NONE)
      return NONE;
    else if (unitclause_process() == NONE) return NONE;
  }
  return TRUE;
}

int set_equivalences_by_betes() {
  int i, nb=0, bete, class1, class2, result;
  int var1, var2, var3, *bete_vars, pp, twovars[3], fixed_var;

  for(i=0; i<TREATING_CLASS_STACK_fill_pointer; i++) 
    grey[TREATING_CLASS_STACK[i]]=FALSE;

  EQUI_STACK_fill_pointer=0; TREATING_CLASS_STACK_fill_pointer=0; 
  i=PREVIOUS_BETE_STACK_fill_pointer;
  do {
    for (; i < BETE_STACK_fill_pointer; i++) {
      bete=BETE_STACK[i]; bete_vars=betes[bete]; pp=0;
      var1=bete_vars[0]; var2=bete_vars[1]; var3=bete_vars[2];
      if (var_state[var1]==ACTIVE) twovars[pp++]=var1; else fixed_var=var1;
      if (var_state[var2]==ACTIVE) twovars[pp++]=var2; else fixed_var=var2;
      if (var_state[var3]==ACTIVE) twovars[pp++]=var3; else fixed_var=var3;
      
      if (pp==2) {
	nb+=2;
	class1=get_lit_class(twovars[0]); class2=get_lit_class(twovars[1]);
	if (((var_current_value[fixed_var]==TRUE) && 
	     (bete_sign[bete]==NEGATIVE)) ||
	    ((var_current_value[fixed_var]==FALSE) && 
	     (bete_sign[bete]==POSITIVE))) {
	  if (class1==class2) 
	    return NONE;
	  class2=get_complement(class2);
	}
	else 
	  if (class1==get_complement(class2))
	    return NONE;
	if (class1 != class2) {
	  if (positive(class1)) var1=class1; 
	  else var1=get_var_from_lit(class1);
	  if (positive(class2)) var2=class2; 
	  else var2=get_var_from_lit(class2);
	  if ((nb_bete[var1]>1) && (nb_bete[var2]>1))
	    push(class_union(class1, class2), TREATING_CLASS_STACK);
	  else class_union(class1, class2);
	}
      }
      else
	if ((pp==1) && (propage_unit_bete(bete)==NONE))
	  return NONE;
	else
	  if ((pp==0) && (test_empty_bete(bete)==NONE))
	    return NONE;
    }
    result=bete_reasoning();
    if (result==NONE) 
      return NONE;
  } while (i<BETE_STACK_fill_pointer);
  return nb;
}

int propage_unit_bete(int bete) {
  int var1, var2, var3, *bete_vars, pp, twovars[3], active_var, nb;
  
  bete_vars=betes[bete]; pp=0; nb=0;
  var1=bete_vars[0]; var2=bete_vars[1]; var3=bete_vars[2];

  if (var_state[var1]==PASSIVE) twovars[pp++]=var1;
  else active_var=var1;
  if (var_state[var2]==PASSIVE) twovars[pp++]=var2;
  else active_var=var2;
  if (var_state[var3]==PASSIVE) twovars[pp++]=var3;
  else active_var=var3;

  if (var_current_value[twovars[0]] != var_current_value[twovars[1]])
    nb++;
  if (bete_sign[bete]==NEGATIVE) nb++;

  if (nb==1) 
    return falsify_class(get_lit_class(active_var));
  else 
    return satisfy_class(get_lit_class(active_var));
}

int test_empty_bete(int bete) {
  int var1, var2, var3, *bete_vars, pp, twovars[3], active_var, nb;
  
  bete_vars=betes[bete]; nb=0;
  var1=bete_vars[0]; var2=bete_vars[1]; var3=bete_vars[2];

  if (var_current_value[var1] != var_current_value[var2])
    nb++;
  if (bete_sign[bete]==NEGATIVE) nb++;
  if (var_current_value[var3]==FALSE) nb++;

  if ((nb==1) || (nb==3))
    return NONE;
  else return TRUE;
}

int set_equivalencies() { 
  int i, clause;
  if (set_equivalences_by_betes()==NONE) return NONE;
  for(i= PREVIOUS_MANAGEDCLAUSE_STACK_fill_pointer;
	  i<MANAGEDCLAUSE_STACK_fill_pointer; i++) {
    clause=MANAGEDCLAUSE_STACK[i];
    if ((clause_state[clause]==ACTIVE) && (clause_length[clause]==2)) {
      if (set_equivalence_for_clause(clause)==NONE)
	return NONE;
    }
  }
  return TRUE;
}

int set_equivalence_for_clause(int clause1) {
  int *lits, pp, twolits[3], var, lit, lit1, lit2, opp_lit1, opp_lit2,
    class1, class2, opp_class1, opp_class2, var1, var2,
    first_lit, opp_first_lit, clause2, *equi_pair;

  lits = sat[clause1]; pp=0;
  for(lit=*lits; lit!=NONE; lit=*(++lits)) {
    if (positive(lit)) var=lit; else var=get_var_from_lit(lit);
    if (var_state[var]==ACTIVE) {
      twolits[pp++]=lit;
      if (pp>2) return FALSE;
    }
  }
  lit1=twolits[0]; lit2=twolits[1]; 
  opp_lit1=get_complement(lit1); opp_lit2=get_complement(lit2);
  class1=get_lit_class(lit1); class2=get_lit_class(lit2);
  if (class1==class2) {
    clause_state[clause1]=PASSIVE; push(clause1, CLAUSE_STACK);
    if (satisfy_class(class1)==NONE) return NONE;
  }
  else
  if (complement(class1, class2)) {
    clause_state[clause1]=PASSIVE;
    push(clause1, CLAUSE_STACK);
  }
  else {
    /* un jour travailler pour opp_class1 et opp_class2 */
    clause2=search_clauses(opp_lit1, opp_lit2); 
    if (clause2 != NONE) {
      clause_state[clause2]=PASSIVE; push(clause2, CLAUSE_STACK);
      clause_state[clause1]=PASSIVE; push(clause1, CLAUSE_STACK);
      EQUI_STACK_fill_pointer=0;
      store_equi_pair(class1, get_complement(class2));
      if (bete_reasoning()==NONE) return NONE;
    }
  }
  return TRUE;
}

int store_equi_pair(int class1, int class2) {
  int *equi_pair;

  equi_pair=EQUI_STACK[EQUI_STACK_fill_pointer++];
  equi_pair[0]=class1; equi_pair[1]=class2;
}

int fix_class_by_bete(int class_to_fix, int bete, int lit1, int lit2) {
  int nb_com=0;
  if (lit1!=lit2) nb_com++;
  if (bete_sign[bete] == NEGATIVE) nb_com++;
  if (nb_com==1) {
    if (falsify_class(class_to_fix)==NONE)
      return NONE;
    else return FALSE;
  }
  else {
    if (satisfy_class(class_to_fix)==NONE)
      return NONE;
    else return FALSE;
  }
}

int pass_value(int var, int class1, int class2) {
  if (((var_current_value[var] == TRUE) && (positive(class1))) ||
      ((var_current_value[var] == FALSE) && (negative(class1)))) {
    if (satisfy_class(class2)==NONE)
      return NONE;
    else return FALSE;
  }
  else { 
    if (falsify_class(class2)==NONE)
      return NONE;
    else return FALSE;
  }
}

int examine_classes(int *class1, int *class2, int i) {
  int temp_class1, temp_class2, *equi_pair, var1, var2;
  equi_pair=EQUI_STACK[i]; 
  temp_class1=get_lit_class(equi_pair[0]); 
  temp_class2=get_lit_class(equi_pair[1]);
  if (temp_class1==temp_class2) return FALSE;
  else
  if (complement(temp_class1, temp_class2)) return NONE;

  if (positive(temp_class1)) var1=temp_class1; 
  else var1=get_var_from_lit(temp_class1);
  if (positive(temp_class2)) var2=temp_class2; 
  else var2=get_var_from_lit(temp_class2);

  if ((var_state[var1] == ACTIVE) && (var_state[var2] == ACTIVE)) {
    *class1=temp_class1; *class2=temp_class2;
  }
  else {
    if ((var_state[var1] == PASSIVE) && (var_state[var2] == PASSIVE)) {
      if ((var_current_value[var1] == var_current_value[var2]) &&
	  (((positive(temp_class1)) && (negative(temp_class2))) ||
	   ((negative(temp_class1)) && (positive(temp_class2)))))
	return NONE;
      else 
	if ((var_current_value[var1] != var_current_value[var2]) &&
	    (((positive(temp_class1)) && (positive(temp_class2))) ||
	     ((negative(temp_class1)) && (negative(temp_class2)))))
	  return NONE;
	else return FALSE;
    }
    else
      if (var_state[var1] == PASSIVE) 
	return pass_value(var1, temp_class1, temp_class2);
      else
	if (var_state[var2] == PASSIVE) 
	  return pass_value(var2, temp_class2, temp_class1);
  }

  return TRUE;
}

int class_union(int class1, int class2) {
  int opp_class1, opp_class2, first_lit, opp_first_lit, class;

  if (class_size[class1] > class_size[class2]) {
    class=class1; class1=class2; class2=class;
  }

  opp_class1=get_complement(class1); 
  opp_class2=get_complement(class2);

  lit_class[class1]=class2; 
  class_size[class2]+=class_size[class1];

  lit_class[opp_class1]=opp_class2;
  class_size[opp_class2]+=class_size[opp_class1];

  first_lit=get_first_lit_of_class(class2);
  opp_first_lit=get_first_lit_of_class(opp_class2);
  class_of[first_lit]=class1;
  class_of[opp_first_lit]=opp_class1;
  push(class1, VALUE_STACK); push(opp_class1, VALUE_STACK);
  push(first_lit, VALUE_STACK); 
  push(opp_first_lit, VALUE_STACK);
  grey[class2]=TRUE;
  return class2;
}

#define REDONDANT -2
long NB_UNIFY=0, EFFECTIVE_NB_UNIFY=0, EFFECTIVE;

int remove_bete1(int bete) {
  bete_state[bete] = PASSIVE; push(bete, BETE_STACK);
}

int examine_bete(int bete) {
  int *bete_vars, lit1, lit2, lit3;

  bete_vars=betes[bete];
  lit1=get_lit_class(bete_vars[0]);
  lit2=get_lit_class(bete_vars[1]);  
  lit3=get_lit_class(bete_vars[2]);

  if (same_var(lit1, lit2)) 
    return fix_class_by_bete(lit3, bete, lit1, lit2);
  else 
    if (same_var(lit1, lit3)) 
      return fix_class_by_bete(lit2, bete, lit1, lit3);
    else
      if (same_var(lit2, lit3)) 
	return fix_class_by_bete(lit1, bete, lit2, lit3);
  return TRUE;
}

int reset_bete_and_var() {
  int i;
  for(i=0; i<var_tab_fill_pointer; i++)
    involved_in_bete[var_tab[i]]=NULL;
  var_tab_fill_pointer=0;
}

int compare_bete(struct bete_node *p1, struct bete_node *p2, 
		 int same_mate, int diff_mate, int var) {
  int equ_in_bete1, mate1_in_bete2, bete1, bete2, mate2_in_bete2, 
    diff_in_bete2, same_in_bete2, equ_in_bete2, nb_com=0,
    diff_in_bete1, same_in_bete1;

  bete1=p1->bete; bete2=p2->bete;
  if ((bete1<STATIC_NB_BETE) && (bete2<STATIC_NB_BETE))
    remove_bete(bete1);
  else remove_bete1(bete1);
  same_in_bete1=my_get_lit_class(same_mate);
  diff_in_bete1=my_get_lit_class(diff_mate);
  equ_in_bete1=my_get_lit_class(p1->self);

  equ_in_bete2=my_get_lit_class(p2->self);

  mate1_in_bete2=my_get_lit_class(p2->mate1); 
  mate2_in_bete2=my_get_lit_class(p2->mate2);

  if (same_var1(mate1_in_bete2, var)) {
    same_in_bete2=mate1_in_bete2; diff_in_bete2=mate2_in_bete2;
  }
  else {
    same_in_bete2=mate2_in_bete2; diff_in_bete2=mate1_in_bete2;
  }
  if (same_var(diff_in_bete1, diff_in_bete2)) {
    if (equ_in_bete1 != equ_in_bete2) nb_com++;
    if (diff_in_bete1 != diff_in_bete2) nb_com++;
    if (same_in_bete1 != same_in_bete2) nb_com++;
    if (bete_sign[bete1]==NEGATIVE) nb_com++;
    if (bete_sign[bete2]==NEGATIVE) nb_com++;
    if ((nb_com==1) || (nb_com==3) || (nb_com==5)) 
      return NONE;
    else
      return REDONDANT;
  }
  else {
    if (equ_in_bete1 != equ_in_bete2) nb_com++;
    if (same_in_bete1 != same_in_bete2) nb_com++;
    if (bete_sign[bete1]==NEGATIVE) nb_com++;
    if (bete_sign[bete2]==NEGATIVE) nb_com++;
    if ((nb_com==1) || (nb_com==3)) 
      store_equi_pair(diff_in_bete1, get_complement(diff_in_bete2));
    else 
      store_equi_pair(diff_in_bete1, diff_in_bete2);
    return REDONDANT;
  }
}

int reasoning_on_class(int class) {
  int lit, var, bete, class_var, lit1, lit2, var1, var2, mate1, mate2;
  struct bete_node *pbete_node;
  reset_bete_and_var();
  if (positive(class)) class_var=class; 
  else class_var=get_var_from_lit1(class);
  for(lit=class; lit != NONE; lit=class_of[lit]) {
    if (positive(lit)) var=lit; else var=get_var_from_lit1(lit);
    for(pbete_node=in_bete[var]; pbete_node != NULL;
	pbete_node=pbete_node->next) {
      bete=pbete_node->bete;
      if (bete_state[bete]==ACTIVE) {
	mate1=pbete_node->mate1; mate2=pbete_node->mate2;
	var1=((lit_class[mate1]==NONE) ? mate1 : 
	      lit_var[get_lit_class1(mate1)]);
	/* my_get_lit_class_var(mate1); */
	var2=((lit_class[mate2]==NONE) ? mate2 : 
	      lit_var[get_lit_class1(mate2)]);
	/* my_get_lit_class_var(mate2); */
	if ((var1==var2) || (class_var==var1) || (class_var==var2)) {
	  if (examine_bete(bete)==NONE) 
	    return NONE;
	}
	else {
	  if (involved_in_bete[var1] != NULL) {
	    if (compare_bete(pbete_node, involved_in_bete[var1], 
			     mate1, mate2, var1)==NONE)
	      return NONE;
	  }
	  else {
	    involved_in_bete[var1] = pbete_node; push(var1, var_tab);
	    if (involved_in_bete[var2] != NULL) {
	      if (compare_bete(pbete_node, involved_in_bete[var2], 
			       mate2, mate1, var2)==NONE)
		return NONE;
	    }
	    else {
	      involved_in_bete[var2] = pbete_node; push(var2, var_tab);
	    }
	  }
	}
      }
    }
  }
  return TRUE;
}

int bete_reasoning() {
  int i, class, class1, class2;
  do {
    for(i=0; i<TREATING_CLASS_STACK_fill_pointer; i++) {
      class=get_lit_class(TREATING_CLASS_STACK[i]);
      if (grey[class] == TRUE) {
	grey[get_complement(class)]=FALSE; grey[class]=FALSE;
	if (reasoning_on_class(class)==NONE)
	  return NONE;
      }
    }
    TREATING_CLASS_STACK_fill_pointer=0;
    for (i=0;  i<EQUI_STACK_fill_pointer; i++) {
      switch(examine_classes(&class1, &class2, i)) {
      case NONE: return NONE;
      case TRUE: 
	  push(class_union(class1, class2), TREATING_CLASS_STACK);
	  break;
      }
    } 
    EQUI_STACK_fill_pointer=0;
  } while (TREATING_CLASS_STACK_fill_pointer>0);
  return TRUE;
}

int remove_bete(int bete) {
  int i, *clauses, clause;

  bete_state[bete] = PASSIVE; push(bete, BETE_STACK);
  if (bete>=STATIC_NB_BETE) return FALSE;
  
  clauses=bete_clauses[bete];
  for (i=0; i<4; i++) {
    clause=clauses[i];
    clause_state[clause]=PASSIVE; push(clause, CLAUSE_STACK);
  }
  
  return TRUE;
}
/*
#define get_var(lit) ((positive(lit)) ? lit : lit_var[lit])
*/
#define get_var(lit) lit_var[lit]

int get_element(int *diff, int *same, int *equ_class, 
		 int bete, int var, int treating_class_var) {
  int *bete_vars, class1, class2, class3, 
    class_var1, class_var2, class_var3;
  bete_vars=betes[bete]; class1=get_lit_class(bete_vars[0]);
  class2=get_lit_class(bete_vars[1]); class3=get_lit_class(bete_vars[2]);
  class_var1=get_var(class1);  class_var2=get_var(class2);
  class_var3=get_var(class3);
  if (class_var1==treating_class_var) {
    *equ_class=class1;
    if (class_var2==var) {
      *same=class2; *diff=class3;
    }
    else {
      *same=class3; *diff=class2;
    }
  }
  else 
    if (class_var1==var) {
      *same=class1;
      if (class_var2==treating_class_var) {
	*equ_class=class2; *diff=class3;
      }
      else {
	*equ_class=class3; *diff=class2;
      }
    }
    else {
      if (class_var2==treating_class_var) {
	*equ_class=class2; *same=class3; 
      }
      else {
	*same=class2; *equ_class=class3;
      }
      *diff=class1;
    }
}

int remove_bete_for_var(int var) {
  int bete;
  struct bete_node *pbete_node;

  for(pbete_node=in_bete[var]; pbete_node != NULL;
      pbete_node=pbete_node->next) {
    bete=pbete_node->bete;
    if (bete_state[bete] == ACTIVE) {
      bete_state[bete]=PASSIVE;
      push(bete, BETE_STACK);
    }
  }
}

int get_bete_nb(int class_var) {
  int lit, var, bete, *bete_vars, i, twovars[3], pp, nb=0;
  struct bete_node *pbete_node;

  for(lit=class_var; lit != NONE; lit=class_of[lit]) {
    if (positive(lit)) var=lit; else var=get_var_from_lit(lit);
    for(pbete_node=in_bete[var]; pbete_node != NULL;
	pbete_node=pbete_node->next) {
      bete=pbete_node->bete; 
      if (bete_state[bete]==ACTIVE) {
	nb++;
      }
    }
  }
  nb_bete[class_var]=nb;
  return nb;
}

int choose_and_instantiate_variable() {
  int var, chosen_var=NONE, i, j, posi, nega, class_lit, class_var,
      posi1, nega1, nb_clauses1, max_nb_clauses1 = -1, nb,
      nb_clauses, max_nb_clauses = -1, saved_ma;
  my_type pos2, neg2;
  struct var_node *pvar_node;
  
  NB_BRANCHE++;
  TESTED_VAR_STACK_fill_pointer=0;
  if (set_equivalencies()==NONE) return NONE;
  PREVIOUS_MANAGEDCLAUSE_STACK_fill_pointer=MANAGEDCLAUSE_STACK_fill_pointer;
  PREVIOUS_BETE_STACK_fill_pointer=BETE_STACK_fill_pointer;

  for (class_var = 0; class_var < NB_VAR; class_var++) 
    if ((var_state[class_var] == ACTIVE) && (lit_class[class_var]==NONE)) 
      get_bete_nb(class_var);

  for (class_var = 0; class_var < NB_VAR; class_var++) {
    if ((var_state[class_var] == ACTIVE) && (lit_class[class_var]==NONE)) {
      nb_neg_clause_of_length2[class_var]=0;
      nb_pos_clause_of_length2[class_var]=0;
      if (((neg2=get_neg_clause_nb(neg_in[class_var], class_var))>1) &&
	  ((pos2=get_pos_clause_nb(pos_in[class_var], class_var))>1))
	if (examine1(class_var) == NONE)
	  return NONE;
    }
  }
  if (TESTED_VAR_STACK_fill_pointer < 40) {
    TESTED_VAR_STACK_fill_pointer=0;
    for (class_var = 0; class_var < NB_VAR; class_var++) {
      if ((var_state[class_var] == ACTIVE) && (lit_class[class_var]==NONE)) {
	if (examine1(class_var) == NONE)
	  return NONE;
      }
    }
  }
  
  for (i=0; i<TESTED_VAR_STACK_fill_pointer; i++) {
    var=TESTED_VAR_STACK[i];
    if (var_state[var] == ACTIVE) {
      if (lit_class[var] != NONE) {
	class_lit=get_lit_class(var);
	if (positive(class_lit)) {
	  class_var=class_lit;
	  reduce_if_positive_nb[class_var]+=reduce_if_positive_nb[var];
	  reduce_if_negative_nb[class_var]+=reduce_if_negative_nb[var];
	}
	else {
	  class_var=get_var_from_lit(class_lit);
	  reduce_if_positive_nb[class_var]+=reduce_if_negative_nb[var];
	  reduce_if_negative_nb[class_var]+=reduce_if_positive_nb[var];
	}
      }
    }
  }
  for (i=0; i<TESTED_VAR_STACK_fill_pointer; i++) {
    var=TESTED_VAR_STACK[i];
    if ((var_state[var] == ACTIVE) && (lit_class[var] == NONE)) {
      posi=reduce_if_positive_nb[var];
      nega=reduce_if_negative_nb[var];
      nb_clauses = posi*nega + posi + nega +1;
      if (nb_clauses > max_nb_clauses) {
	chosen_var = var;
	max_nb_clauses = nb_clauses;
      }
    }
  } 
  
  if (chosen_var == NONE) return FALSE;
  saved_clause_stack[chosen_var] = CLAUSE_STACK_fill_pointer;
  saved_managedclause_stack[chosen_var] = MANAGEDCLAUSE_STACK_fill_pointer;
  saved_value_stack[chosen_var]=VALUE_STACK_fill_pointer;
  saved_bete_stack[chosen_var]=BETE_STACK_fill_pointer;
  saved_nb_bete[chosen_var]=NB_BETE;
  saved_previous_managedclause_stack[chosen_var]=
    PREVIOUS_MANAGEDCLAUSE_STACK_fill_pointer;
  saved_previous_bete_stack[chosen_var]=PREVIOUS_BETE_STACK_fill_pointer;

  if (satisfy_var_and_simplify_clauses_for_class(chosen_var, FALSE)==NONE) 
    return NONE;
  return TRUE;
}

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

#define MAX_BETE_NODE_NUMBER 3*tab_bete_size

struct bete_node BETE_NODES[MAX_BETE_NODE_NUMBER];
struct bete_node *BETE_NODE_POINTER=NULL;

int prepare_bete_ressources() {
  int i;

  for(i=0; i<MAX_BETE_NODE_NUMBER; i++) {
    BETE_NODES[i].next=BETE_NODE_POINTER;
    BETE_NODE_POINTER=&BETE_NODES[i];
  }
}

struct bete_node *allocate_bete_node() {
  struct bete_node *pbete_node;
  pbete_node=BETE_NODE_POINTER;
  BETE_NODE_POINTER=BETE_NODE_POINTER->next;
  return pbete_node;
}

void deallocate_bete_node(struct bete_node *pbete_node) {
  pbete_node->next=BETE_NODE_POINTER;
  BETE_NODE_POINTER=pbete_node;
}

void init() {
  int i, var;
  /*
  for (var = 0; var < NB_VAR; var++) 
	  if (var_state[var] == ACTIVE) {
	  class_flag[var]=FALSE;
  }
  */
  for (i=0; i<2*NB_VAR; i++) {
    lit_class[i]=NONE;
    class_of[i]=NONE;
    class_size[i]=1;
  }
  for(i=0; i<NB_VAR; i++)
    involved_in_bete[i]=NULL;

  for(i=0; i<NB_VAR; i++) {
    lit_var[i]=i;
    lit_com[i]=i+NB_VAR;
  }
  for (i=NB_VAR; i<2*NB_VAR; i++) {
    lit_var[i]=i-NB_VAR;
    lit_com[i]=i-NB_VAR;
  }

  prepare_bete_ressources();
}

int set_betes() {
  int clause, lit1, lit2, lit3, *lits, clausebis, clause_list[2], i,
    saved_clause_stack_fill_pointer;

  for(i=0; i<NB_VAR; i++) {
    in_bete[i]=NULL;
  }

  saved_clause_stack_fill_pointer=CLAUSE_STACK_fill_pointer;
  
  for(clause=0; clause<INIT_NB_CLAUSE; clause++) {
    if ((clause_state[clause]==ACTIVE) && (clause_length[clause]==3)) {
      lits=sat[clause]; lit1=lits[0]; lit2=lits[1]; lit3=lits[2];
      clausebis=matching1(lit1, lit2, lit3);
      if ((clausebis!=NONE) && 
	  (matching2(lit1, lit2, lit3, clause_list)==TRUE)) {
	clause_state[clausebis]=PASSIVE; clause_state[clause]=PASSIVE;
	clause_state[clause_list[0]]=PASSIVE;
	clause_state[clause_list[1]]=PASSIVE;
	push(clausebis, CLAUSE_STACK); push(clause, CLAUSE_STACK);
	push(clause_list[0],  CLAUSE_STACK);
	push(clause_list[1],  CLAUSE_STACK);
	bete_clauses[NB_BETE][0]=clause; 
	bete_clauses[NB_BETE][1]=clausebis;
	bete_clauses[NB_BETE][2]=clause_list[0];
	bete_clauses[NB_BETE][3]=clause_list[1];
	set_bete(lit1, lit2, lit3);
      }
    }
  }
  for(i=saved_clause_stack_fill_pointer; i<CLAUSE_STACK_fill_pointer; i++) {
    clause_state[CLAUSE_STACK[i]]=ACTIVE;
  }
  CLAUSE_STACK_fill_pointer=saved_clause_stack_fill_pointer;
  STATIC_NB_BETE=NB_BETE;
}

void set_link_for_bete(int bete_no) {
  int i, var1, var2, var3, *bete_vars;
  struct bete_node *pbete_node;

  bete_vars=betes[bete_no]; var1=bete_vars[0];
  var2=bete_vars[1]; var3=bete_vars[2];

  pbete_node=allocate_bete_node(); 
  pbete_node->bete=bete_no;
  pbete_node->mate1=var2;   pbete_node->mate2=var3;
  pbete_node->self=var1; 
  pbete_node->next=in_bete[var1]; 
  in_bete[var1]=pbete_node;

  pbete_node=allocate_bete_node(); 
  pbete_node->bete=bete_no;
  pbete_node->mate1=var1;   pbete_node->mate2=var3;
  pbete_node->self=var2; 
  pbete_node->next=in_bete[var2]; 
  in_bete[var2]=pbete_node;

  pbete_node=allocate_bete_node(); 
  pbete_node->bete=bete_no;
  pbete_node->mate1=var1;   pbete_node->mate2=var2;
  pbete_node->self=var3; 
  pbete_node->next=in_bete[var3]; 
  in_bete[var3]=pbete_node;
}

int remove_link_for_bete(int bete_no) {
  int i, var, *bete_vars;
  struct bete_node *pbete_node, *pbete_node1, *pbete_node_to_remove;

  bete_vars=betes[bete_no];
  for (i=0; i<3; i++) {
    var=bete_vars[i];
    if (in_bete[var]->bete==bete_no) {
      pbete_node_to_remove= in_bete[var];
      in_bete[var]= pbete_node_to_remove->next;
      deallocate_bete_node(pbete_node_to_remove); 
    }
    else {
      for(pbete_node1=in_bete[var], pbete_node=pbete_node1->next;
	  pbete_node != NULL;
	  pbete_node1=pbete_node, pbete_node=pbete_node->next) {
	if (pbete_node->bete==bete_no) {
	  pbete_node1->next=pbete_node->next;
	  deallocate_bete_node(pbete_node); 
	  break;
	}
      }
    }
  }
}

int set_bete(int lit1, int lit2, int lit3) {
  int nb=0, var1, var2, var3, sign;

  if (positive(lit1)) {
    var1=lit1; nb++;
  }
  else var1=get_var_from_lit1(lit1);

  if (positive(lit2)) {
    var2=lit2; nb++;
  }
  else var2=get_var_from_lit1(lit2);

  if (positive(lit3)) {
    var3=lit3; nb++;
  }
  else var3=get_var_from_lit1(lit3);
  if ((nb==1) || (nb==3)) sign=POSITIVE;
  else sign=NEGATIVE;

  insert_new_bete(var1, var2, var3, sign);
}

int insert_new_bete(int var1, int var2, int var3, int sign) {
  int  *bete_vars;
  tri3(&var1,&var2, &var3);
  
  bete_vars=betes[NB_BETE]; 
  bete_vars[0]=var1;  bete_vars[1]=var2; bete_vars[2]=var3;
  bete_sign[NB_BETE]=sign; 
  bete_state[NB_BETE]=ACTIVE; bete_involving[NB_BETE]=NONE;
  set_link_for_bete(NB_BETE);
  NB_BETE++; TOTAL_NB_BETE++;
  return TRUE;
}

int matching1(int lit1, int lit2, int lit3) {
  int clause;
  
  if (positive(lit1))  
    return matching1_clause(pos_in[lit1], lit1, lit2, lit3);
  else 
    return matching1_clause(neg_in[get_var_from_lit(lit1)], lit1, lit2, lit3);
}

int matching1_clause(int* clauses, int lit1, int lit2, int lit3) {
  int clause, *lits;
  for(clause=*clauses; clause!=NONE; clause=*(++clauses)) {
    if ((clause_state[clause]==ACTIVE) && (clause_length[clause]==3)) {
      lits=sat[clause];
      if ((lit1==lits[0]) && (complement(lit2, lits[1])) &&
	  (complement(lit3, lits[2])))
	return clause;
    }
  }
  return NONE;
}

int matching2(int lit1, int lit2, int lit3, int *clause_list) {
  int clause;
  if (positive(lit1))
    return matching2_clause(neg_in[lit1], lit1, lit2, lit3, clause_list);
  else 
    return matching2_clause(pos_in[get_var_from_lit(lit1)], lit1, lit2, lit3, 
							clause_list);
}

int matching2_clause(int* clauses, int lit1, int lit2, int lit3, 
		     int *clause_list) {
  int clause, *lits, pp=0;
  for(clause=*clauses; clause!=NONE; clause=*(++clauses)) {
    if ((clause_state[clause]==ACTIVE) && (clause_length[clause]==3)) {
      lits=sat[clause];
      if (complement(lit1,lits[0])) {
	if (((complement(lit2, lits[1])) && (lit3==lits[2])) ||
	    ((complement(lit3, lits[2])) && (lit2==lits[1]))) {
	  clause_list[pp]=clause; pp++;
	}
      }
    }
  }
  if (pp==2) return TRUE; else return FALSE;
}

int init_set_equivalencies() {
  int clause;

  for (clause=0; clause<TOTAL_NB_CLAUSE; clause++) {
    if ((clause_state[clause]==ACTIVE) && (clause_length[clause]==2))
      if (set_equivalence_for_clause(clause)==NONE)
	return NONE;
  }
  return TRUE;
}

int my_satisfy_class(int class) {
  if (positive(class)) {
    if (my_satisfy_var_and_simplify_clauses_for_class(class)==NONE)
      return NONE;
    else if (branch() == NONE) return NONE;
  }
  else {
    if (my_falsify_var_and_simplify_clauses_for_class(
	get_var_from_lit(class))==NONE)
      return NONE;
    else if (branch() == NONE) return NONE;
  }
  return TRUE;
}

int my_falsify_class(int class) {
  if (positive(class)) {
    if (my_falsify_var_and_simplify_clauses_for_class(class)==NONE)
      return NONE;
    else if (branch() == NONE) return NONE;
  }
  else {
    if (my_satisfy_var_and_simplify_clauses_for_class(
	get_var_from_lit(class))==NONE)
      return NONE;
    else if (branch() == NONE) return NONE;
  }
  return TRUE;
}

int my_propage_unit_bete(int bete) {
  int var1, var2, var3, *bete_vars, pp, twovars[3], active_var, nb;
  
  bete_vars=betes[bete]; pp=0; nb=0;
  var1=bete_vars[0]; var2=bete_vars[1]; var3=bete_vars[2];

  if (var_state[var1]==PASSIVE) twovars[pp++]=var1;
  else active_var=var1;
  if (var_state[var2]==PASSIVE) twovars[pp++]=var2;
  else active_var=var2;
  if (var_state[var3]==PASSIVE) twovars[pp++]=var3;
  else active_var=var3;

  if (var_current_value[twovars[0]] != var_current_value[twovars[1]])
    nb++;
  if (bete_sign[bete]==NEGATIVE) nb++;

  if (nb==1) 
    return my_falsify_class(get_lit_class(active_var));
  else 
    return my_satisfy_class(get_lit_class(active_var));
}

int get_mesure(int saved_managedclause_fill_pointer,
	       int saved_variable_stack_fill_pointer) {
  int i, clause, nb=0;

  for(i=saved_managedclause_fill_pointer; 
      i<MANAGEDCLAUSE_STACK_fill_pointer; i++) {
   clause = MANAGEDCLAUSE_STACK[i];
   if (clause_state[clause] == ACTIVE)
     nb++;
 }
  return VARIABLE_STACK_fill_pointer+(nb/2)-saved_variable_stack_fill_pointer;
}

int my_set_equivalence_for_clause(int clause1) {
  int *lits, pp, twolits[3], var, lit, lit1, lit2, opp_lit1, opp_lit2,
    class1, class2, opp_class1, opp_class2, var1, var2,
    first_lit, opp_first_lit, clause2, *equi_pair;

  lits = sat[clause1]; pp=0;
  for(lit=*lits; lit!=NONE; lit=*(++lits)) {
    if (positive(lit)) var=lit; else var=get_var_from_lit(lit);
    if (var_state[var]==ACTIVE) {
      twolits[pp++]=lit;
      if (pp>3) return FALSE;
    }
  }
  lit1=twolits[0]; lit2=twolits[1]; 
  opp_lit1=get_complement(lit1); opp_lit2=get_complement(lit2);
  class1=get_lit_class(lit1); class2=get_lit_class(lit2);
  if (class1==class2) {
    clause_state[clause1]=PASSIVE; push(clause1, CLAUSE_STACK);
    if (my_satisfy_class(class1)==NONE) return NONE;
  }
  else
  if (complement(class1, class2)) {
    clause_state[clause1]=PASSIVE;
    push(clause1, CLAUSE_STACK);
  }
  else {
    /* un jour travailler pour opp_class1 et opp_class2 */
    clause2=search_clauses(opp_lit1, opp_lit2); 
    if (clause2 != NONE) {
      clause_state[clause2]=PASSIVE; push(clause2, CLAUSE_STACK);
      clause_state[clause1]=PASSIVE; push(clause1, CLAUSE_STACK);
      EQUI_STACK_fill_pointer=0;
      store_equi_pair(class1, get_complement(class2));
      if (my_bete_reasoning1()==NONE) return NONE;
    }
  }
  return TRUE;
}

int my_set_equivalences1(int saved_bete_stack_fill_pointer) {
  int i, bete, class1, class2, result;
  int var1, var2, var3, *bete_vars, pp, twovars[3], fixed_var;
  for(i=0; i<TREATING_CLASS_STACK_fill_pointer; i++) 
    grey[TREATING_CLASS_STACK[i]]=FALSE;

  EQUI_STACK_fill_pointer=0; TREATING_CLASS_STACK_fill_pointer=0; 
  i=saved_bete_stack_fill_pointer;
  do {
    for (; i < BETE_STACK_fill_pointer; i++) {
      bete=BETE_STACK[i]; bete_vars=betes[bete]; pp=0;
      var1=bete_vars[0]; var2=bete_vars[1]; var3=bete_vars[2];
      if (var_state[var1]==ACTIVE) twovars[pp++]=var1; else fixed_var=var1;
      if (var_state[var2]==ACTIVE) twovars[pp++]=var2; else fixed_var=var2;
      if (var_state[var3]==ACTIVE) twovars[pp++]=var3; else fixed_var=var3;
      
      if (pp==2) {
	class1=get_lit_class(twovars[0]); class2=get_lit_class(twovars[1]);
	if (((var_current_value[fixed_var]==TRUE) && 
	     (bete_sign[bete]==NEGATIVE)) ||
	    ((var_current_value[fixed_var]==FALSE) && 
	     (bete_sign[bete]==POSITIVE))) {
	  if (class1==class2) 
	    return NONE;
	  class2=get_complement(class2);
	}
	else 
	  if (class1==get_complement(class2))
	    return NONE;
	if (class1 != class2) {
	  var1=get_var(class1); var2=get_var(class2);
	  if ((nb_bete[var1]>1) && (nb_bete[var2]>1))
	    /*    && ((nb_bete[var1]-1)*(nb_bete[var2]-1)>5)) */
	  {
	    push(class_union(class1, class2), TREATING_CLASS_STACK);
	  }
	  else class_union(class1, class2);
	}
      }
      else
	if ((pp==1) && (my_propage_unit_bete(bete)==NONE))
	  return NONE;
	else
	  if ((pp==0) && (test_empty_bete(bete)==NONE))
	    return NONE;
    }
    result=my_bete_reasoning1();
    if (result==NONE) 
      return NONE;
  } while (i<BETE_STACK_fill_pointer);
  return TRUE;
}

int get_nb(int saved_managedclause_stack_fill_pointer) {
  int i, clause, *lits, lit, var, class, class_var, nb=0;
  
  for(i=saved_managedclause_stack_fill_pointer; 
      i<MANAGEDCLAUSE_STACK_fill_pointer; i++) {
    clause=MANAGEDCLAUSE_STACK[i];
    if ((clause_state[clause] == ACTIVE) && 
	(clause_length[clause] == 2)) {
      lits = sat[clause];
      for(lit=*lits; lit!=NONE; lit=*(++lits)) {
	var=get_var_from_lit1(lit);
	if (var_state[var] == ACTIVE) {
	  class=get_lit_class(lit);
	  class_var=get_var_from_lit1(class);
	  if (negative(class)) 
	    nb+=nb_pos_clause_of_length2[class_var];
	  else 
	    nb+=nb_neg_clause_of_length2[class_var];
	}
      }
    }
  }
  return nb;
}

int get_mesure1(int saved_managedclause_stack_fill_pointer,
		int saved_variable_stack_fill_pointer,
		int saved_value_stack_fill_pointer,
		int saved_bete_stack_fill_pointer) {
  int i, clause, nb, nb1=0, nb2=0;

  nb=my_set_equivalences1(saved_bete_stack_fill_pointer);
  if (nb == NONE) 
    return NONE;
  else {
    for(i= saved_managedclause_stack_fill_pointer; 
	i<MANAGEDCLAUSE_STACK_fill_pointer; i++) {
      clause=MANAGEDCLAUSE_STACK[i];
      if ((clause_state[clause]==ACTIVE) && (clause_length[clause]==2)) {
	if (my_set_equivalence_for_clause(clause)==NONE)
	  return NONE;
      }
    }
    nb1=get_nb(saved_managedclause_stack_fill_pointer);

    for(i=saved_variable_stack_fill_pointer; 
	i<VARIABLE_STACK_fill_pointer; i++) 
      if (lit_class[VARIABLE_STACK[i]]==NONE) nb2++;
    return nb1/2+
      ((VALUE_STACK_fill_pointer-saved_value_stack_fill_pointer)/4)+nb2;
  }
}

long MY_NB_UNIFY=0, MY_EFFECTIVE_NB_UNIFY=0;

int init_for_preprocess() {
  int i;
  EQ1_fill_pointer=0; EQ2_fill_pointer=0;
  BETE_TO_ADD_fill_pointer=0;
  for(i=0; i<IMPLIED_LITS_fill_pointer; i++) 
    LIT_IMPLIED[IMPLIED_LITS[i]]=0;
  IMPLIED_LITS_fill_pointer=0;
}

int preprocess() {
  int var, i;
  
  for(i=0; i<NB_BETE; i++) 
    bete_involving[i]=NONE;
  for(i=0; i<2*NB_VAR; i++)
    grey[i]=FALSE;

  for (var = 0; var < NB_VAR; var++) 
    if ((var_state[var] == ACTIVE) && (lit_class[var]==NONE)) 
      get_bete_nb(var);
  for (var = 0; var < NB_VAR; var++) {
    if ((var_state[var] == ACTIVE) && (lit_class[var]==NONE)) {
      if (examine1(var) == NONE)
	return NONE;
    }
  }
  for (i=0; i<NB_BETE; i++) {
    if (bete_state[i]==PASSIVE) 
      remove_link_for_bete(i);
  }
  return TRUE;
}

int treat_implied_lits(int var) {
  int i, lit, lits[3], *plit, var1;
  for (i=0; i<IMPLIED_LITS_fill_pointer; i++) {
    if (var_state[var]==PASSIVE) return TRUE;
    lit=IMPLIED_LITS[i];
    switch(LIT_IMPLIED[lit]) {
    case 0: break;
    case 1: 
      if (positive(lit)) var1=lit; else var1=get_var_from_lit(lit);
      LIT_IMPLIED[lit]=0;
      if (LIT_IMPLIED[get_complement(lit)] != 0) {
	LIT_IMPLIED[get_complement(lit)]=0;
	if (var_state[var1] == ACTIVE) {
	  if (insert_eq(get_lit_class(var), get_lit_class(lit))==NONE)
	    return NONE;
	}
	else {
	  if (positive(lit)) 
	    return satisfy_class(get_lit_class(var));
	  else return falsify_class(get_lit_class(var));
	}
      }
      break;
    case 2:
      if (positive(lit)) var1=lit; else var1=get_var_from_lit(lit);
      LIT_IMPLIED[lit]=0;
      if ((var_state[var1]==ACTIVE) &&
	  (satisfy_class(get_lit_class(lit))==NONE))
	return NONE;
      break;
    }
  }
  return TRUE;
}

int treat_implied_betes(int var) {
  int i, j, lit11, lit12, lit21, lit22;
  for(i=0; i<EQ1_fill_pointer; i++) {
    lit11=EQ1[i][0]; lit12=EQ1[i][1];
    for(j=0; j<EQ2_fill_pointer; j++) {
      lit21=EQ2[j][0]; lit22=EQ2[j][1];
      if ((same_var(lit11, lit21)) && (same_var(lit12, lit22))) {
	if (same_eq(lit11, lit21, lit12, lit22)) {
	  if (insert_eq(lit11, lit12)==NONE) 
	    return NONE;
	  if (var_state[var] == PASSIVE) return FALSE;
	}
	else
	  prepare_bete_to_add(lit11, lit12);
      }
    }
  }
  return insert_betes(var);
}

int prepare_bete_to_add(int lit1, int lit2) {
  int *lits;
  lits=BETE_TO_ADD[BETE_TO_ADD_fill_pointer++];
  lits[0]=lit1; lits[1]=lit2;
  return TRUE;
}

int same_eq(int lit11, int lit21, int lit12, int lit22) {
  int nb_com=0;

  if (complement(lit11, lit21)) nb_com++;
  if (complement(lit12, lit22)) nb_com++;
  if ((nb_com==0) || (nb_com==2)) return TRUE;
  else return FALSE;
}

int insert_eq(int class1, int class2) {
  EQUI_STACK_fill_pointer=0;
  store_equi_pair(class1, class2);
  if (bete_reasoning()==NONE) return NONE;
  return TRUE;
}

int instantiate_by_bete(int var1, int var2, int var3, int sign) {
  if (((var_current_value[var2]==var_current_value[var3]) &&
       (sign==POSITIVE)) ||
      ((var_current_value[var2]!=var_current_value[var3]) &&
       (sign==NEGATIVE))) {
    if ((satisfy_class(get_lit_class(var1)))==NONE) return NONE;
  }
  else {
    if ((falsify_class(get_lit_class(var1)))==NONE) return NONE;
  }
  return FALSE;
}

int insert_eq_by_bete(int var1, int var2, int var3, int sign) {
  if (((var_current_value[var3]==TRUE) && (sign==POSITIVE)) ||
      ((var_current_value[var3]==FALSE) && (sign==NEGATIVE)))
    return insert_eq(var1, var2);
  else return insert_eq(var1, get_complement(var2));
}

int instantiate_by_eq(int class1, int class2, int class3) {
  int nb=0;
  if (same_var(class1, class2)) {
    if (negative(class1)) nb++;
    if (negative(class2)) nb++;
    if (negative(class3)) nb++;
    if ((nb==1) || (nb==3)) return NONE;
    else return FALSE;
  }
  if (class2==class3)
    return satisfy_class(class1);
  else
    return falsify_class(class1);
}

int search_and_set_bete(int class1, int class2, int class3) {
  int var1, var2, var3, nb=0, new_sign, i;

  if (positive(class1)) var1=class1;
  else {nb++; var1=get_var_from_lit(class1);}
  if (positive(class2)) var2=class2;
  else {nb++; var2=get_var_from_lit(class2);}
  if (positive(class3)) var3=class3;
  else {nb++; var3=get_var_from_lit(class3);}

  if ((nb==0) || (nb==2)) new_sign=POSITIVE;
  else new_sign=NEGATIVE;
  
  for(i=0; i<bete_tab1_fill_pointer; i++)
    bete_involving[bete_tab1[i]]=NONE;
  bete_tab1_fill_pointer=0;

  EQUI_STACK_fill_pointer=0; simple_parcour_bete_for_var(var1);
  switch (parcour_bete_for_var(var2, var1, var3, new_sign)) {
  case FALSE: return FALSE;
  case NONE: return NONE;
  }
  switch (parcour_bete_for_var(var3, var1, var2, new_sign)) {
  case FALSE: return FALSE;
  case NONE: return NONE;
  }
  insert_new_bete(var1, var2, var3, new_sign);
  return TRUE;
}

int simple_parcour_bete_for_var(int var1) {
  int var, lit, bete;
  struct bete_node *pbete_node;
  for(lit=var1; lit != NONE; lit=class_of[lit]) {
    if (positive(lit)) var=lit; else var=get_var_from_lit1(lit);
    for(pbete_node=in_bete[var]; pbete_node != NULL;
	pbete_node=pbete_node->next) {
      bete=pbete_node->bete;
      if (bete_state[bete]==ACTIVE) {
	bete_involving[bete]=var1; push(bete, bete_tab1);
      }
    }
  }
}

int parcour_bete_for_var(int var1, int var2, int var3, int new_sign) {
  int lit, var, diff1, same12, same11, diff2, same21, same22, bete, nb_com=0;
  struct bete_node *pbete_node;
  for(lit=var1; lit != NONE; lit=class_of[lit]) {
    if (positive(lit)) var=lit; else var=get_var_from_lit(lit);
    for(pbete_node=in_bete[var]; pbete_node != NULL;
	pbete_node=pbete_node->next) {
      bete=pbete_node->bete;
      if (bete_state[bete]==ACTIVE) {
	if (bete_involving[bete]==NONE) {
	  bete_involving[bete]=var1; push(bete, bete_tab1);
	}
	else {
	  same11=var1; same12=bete_involving[bete];
	  if (var2==same12) diff1=var3; else diff1=var2;
	  get_element(&diff2, &same21, &same22, bete, same11, same12);
	  if (negative(same21)) nb_com++; 
	  if (negative(same22)) nb_com++;
	  if (bete_sign[bete]==NEGATIVE) nb_com++;
	  if (new_sign==NEGATIVE) nb_com++;
	  if (same_var(diff1, diff2)) {
	    if (negative(diff2)) nb_com++;
	    if ((nb_com==1) || (nb_com==3) || (nb_com==5))
	      return NONE;
	    else return FALSE;
	  }
	  else {
	    if ((nb_com==1) || (nb_com==3))
	      store_equi_pair(diff1, get_complement(diff2));
	    else 
	      store_equi_pair(diff1, diff2);
	    if (bete_reasoning() == NONE) return NONE;
	    else return FALSE;
	  }
	}
      }
    }
  }
  return TRUE;
}

int insert_bete(int var1, int lit2, int lit3) {
  int class1, class2, class3, var2, var3, sign;
  if (((positive(lit2)) && (positive(lit3))) || 
      ((negative(lit2)) && (negative(lit3))))
    sign=POSITIVE;
  else sign=NEGATIVE;

  if (positive(lit2)) var2=lit2; else var2=get_var_from_lit(lit2);
  if (positive(lit3)) var3=lit3; else var3=get_var_from_lit(lit3);

  if ((var_state[var2]==PASSIVE) && (var_state[var3]==PASSIVE)) {
    return instantiate_by_bete(var1, var2, var3, sign);
  }
  else 
    if (var_state[var2]==PASSIVE) 
      return insert_eq_by_bete(var1, var3, var2, sign);
    else
      if (var_state[var3]==PASSIVE) 
	return insert_eq_by_bete(var1, var2, var3, sign);
      else {
	class1=get_lit_class(var1); class2=get_lit_class(lit2);
	class3=get_lit_class(lit3);
	if (same_var(class1, class2)) 
	  return instantiate_by_eq(class3, class1, class2);
	else
	  if (same_var(class1, class3)) 
	    return instantiate_by_eq(class2, class1, class3);
	else
	  if (same_var(class2, class3)) 
	    return instantiate_by_eq(class1, class2, class3);
	  else {
	    if (search_and_set_bete(class1, class2, class3)==NONE)
	      return NONE;
	    return TRUE;
	  }
      }
}

int insert_betes(int var) {
  int i, *lits;

  for(i=0; i<BETE_TO_ADD_fill_pointer; i++) {
    if (var_state[var]==PASSIVE) return TRUE;
    lits=BETE_TO_ADD[i];
    if (insert_bete(var, lits[0], lits[1])==NONE)
      return NONE;
  }
  return TRUE;
}

int my_fix_class_by_bete1(int class_to_fix, int bete, int lit1, int lit2) {
  int nb_com=0, opp_lit;
  if (lit1!=lit2) nb_com++;
  if (bete_sign[bete] == NEGATIVE) nb_com++;
  if (nb_com==1) {
    opp_lit=get_complement(class_to_fix);
    if (LIT_IMPLIED[opp_lit]==0)
      push(opp_lit, IMPLIED_LITS);
    LIT_IMPLIED[opp_lit]++;
    return my_falsify_class(class_to_fix);
  }
  else {
    if (LIT_IMPLIED[class_to_fix]==0)
      push(class_to_fix, IMPLIED_LITS);
    LIT_IMPLIED[class_to_fix]++;
    return my_satisfy_class(class_to_fix);
  }
}

int my_examine_bete1(int bete) {
  int *bete_vars, lit1, lit2, lit3;

  bete_vars=betes[bete];
  lit1=get_lit_class(bete_vars[0]);
  lit2=get_lit_class(bete_vars[1]);  
  lit3=get_lit_class(bete_vars[2]);

  if (same_var(lit1, lit2)) {
    if (my_fix_class_by_bete1(lit3, bete, lit1, lit2)==NONE)
      return NONE;
    else return FALSE;
  }
  else 
    if (same_var(lit1, lit3)) {
      if (my_fix_class_by_bete1(lit2, bete, lit1, lit3)==NONE)
	return NONE;
      else return FALSE;
    }
    else
      if (same_var(lit2, lit3)) {
	if (my_fix_class_by_bete1(lit1, bete, lit2, lit3)==NONE)
	  return NONE;
	else return FALSE;
      }
  return TRUE;
}

int my_reasoning_on_class(int class) {
  int lit, var, bete, class_var, lit1, lit2, var1, var2, mate1, mate2;
  struct bete_node *pbete_node;
  reset_bete_and_var();
  if (positive(class)) class_var=class; 
  else class_var=get_var_from_lit1(class);
  for(lit=class; lit != NONE; lit=class_of[lit]) {
    if (positive(lit)) var=lit; else var=get_var_from_lit1(lit);
    for(pbete_node=in_bete[var]; pbete_node != NULL;
	pbete_node=pbete_node->next) {
      bete=pbete_node->bete;
      if (bete_state[bete]==ACTIVE) {
	mate1=pbete_node->mate1; mate2=pbete_node->mate2;
	if (lit_class[mate1]==NONE) var1=mate1;
	else var1=lit_var[get_lit_class1(mate1)];
	if (lit_class[mate2]==NONE) var2=mate2;
	else var2=lit_var[get_lit_class1(mate2)];
	if ((var1==var2) || (class_var==var1) || (class_var==var2)) {
	  if (my_examine_bete1(bete)==NONE) 
	    return NONE;
	}
	else {
	  if (involved_in_bete[var1] != NULL) {
	    if (compare_bete(pbete_node, involved_in_bete[var1], 
				mate1, mate2, var1)==NONE)
	      return NONE;
	  }
	  else {
	    involved_in_bete[var1] = pbete_node; push(var1, var_tab);
	    if (involved_in_bete[var2] != NULL) {
	      if (compare_bete(pbete_node, involved_in_bete[var2],
				  mate2, mate1, var2)==NONE)
		return NONE;
	    }
	    else {
	      involved_in_bete[var2] = pbete_node; push(var2, var_tab);
	    }
	  }
	}
      }
    }
  }
  return TRUE;
}

int my_pass_value1(int var, int class1, int class2) {
	int opp_lit;
  if (((var_current_value[var] == TRUE) && (positive(class1))) ||
      ((var_current_value[var] == FALSE) && (negative(class1)))) {
    if (my_satisfy_class(class2)==NONE)
      return NONE;
    else {
      if (LIT_IMPLIED[class2]==0)
	push(class2, IMPLIED_LITS);
      LIT_IMPLIED[class2]++;
      return FALSE;
    }
  }
  else  {
    if (my_falsify_class(class2)==NONE)
      return NONE;
    else {
      opp_lit=get_complement(class2);
      if (LIT_IMPLIED[opp_lit]==0)
	push(opp_lit, IMPLIED_LITS);
      LIT_IMPLIED[opp_lit]++;
      return FALSE;
    }
  }
}

int my_examine_classes1(int *class1, int *class2, int i) {
  int temp_class1, temp_class2, *equi_pair, var1, var2;
  equi_pair=EQUI_STACK[i]; 
  temp_class1=get_lit_class(equi_pair[0]); 
  temp_class2=get_lit_class(equi_pair[1]);
  if (temp_class1==temp_class2) return FALSE;
  else
  if (complement(temp_class1, temp_class2)) return NONE;

  if (positive(temp_class1)) var1=temp_class1; 
  else var1=get_var_from_lit(temp_class1);
  if (positive(temp_class2)) var2=temp_class2; 
  else var2=get_var_from_lit(temp_class2);

  if ((var_state[var1] == ACTIVE) && (var_state[var2] == ACTIVE)) {
    *class1=temp_class1; *class2=temp_class2; return TRUE;
  }
  else {
    if ((var_state[var1] == PASSIVE) && (var_state[var2] == PASSIVE)) {
      if ((var_current_value[var1] == var_current_value[var2]) &&
	  (((positive(temp_class1)) && (negative(temp_class2))) ||
	   ((negative(temp_class1)) && (positive(temp_class2)))))
	return NONE;
      else 
	if ((var_current_value[var1] != var_current_value[var2]) &&
	    (((positive(temp_class1)) && (positive(temp_class2))) ||
	     ((negative(temp_class1)) && (negative(temp_class2)))))
	  return NONE;
	else return FALSE;
    }
    else
      if (var_state[var1] == PASSIVE) 
	return my_pass_value1(var1, temp_class1, temp_class2);
      else
	if (var_state[var2] == PASSIVE) 
	  return my_pass_value1(var2, temp_class2, temp_class1);
  }
}

int my_bete_reasoning1() {
  int i, class, *pair, class1, class2;
  do {
    for(i=0; i<TREATING_CLASS_STACK_fill_pointer; i++) {
      class=get_lit_class(TREATING_CLASS_STACK[i]);
      if (grey[class] == TRUE) {
	grey[get_complement(class)]=FALSE; grey[class]=FALSE;
	if (my_reasoning_on_class(class)==NONE)
	  return NONE;
      }
    }
    TREATING_CLASS_STACK_fill_pointer=0;
    for (i=0;  i<EQUI_STACK_fill_pointer; i++) {
      switch(my_examine_classes1(&class1, &class2, i)) {
      case NONE: return NONE;
      case TRUE: 
	  pair=EQ2[EQ2_fill_pointer]; pair[0]=class1; pair[1]=class2;
	  EQ2_fill_pointer++;
	  push(class_union(class1, class2), TREATING_CLASS_STACK); break;
      }
    } 
    EQUI_STACK_fill_pointer=0;
  } while (TREATING_CLASS_STACK_fill_pointer>0);
  return TRUE;
}

int my_union(int class1, int class2) {
  int opp_class1, opp_class2, first_lit, opp_first_lit, class;
  
  if (class_size[class1] > class_size[class2]) {
    class=class1; class1=class2; class2=class;
  }
  
  opp_class1=get_complement(class1); 
  opp_class2=get_complement(class2);

  lit_class[class1]=class2; 
  class_size[class2]+=class_size[class1];

  lit_class[opp_class1]=opp_class2;
  class_size[opp_class2]+=class_size[opp_class1];

  first_lit=get_first_lit_of_class(class2);
  opp_first_lit=get_first_lit_of_class(opp_class2);
  class_of[first_lit]=class1;
  class_of[opp_first_lit]=opp_class1;
  push(class1, VALUE_STACK); push(opp_class1, VALUE_STACK);
  push(first_lit, VALUE_STACK); 
  push(opp_first_lit, VALUE_STACK);
  grey[class2]=TRUE;
  return class2;
}

main(int argc, char *argv[]) {
   char input_file[WORD_LENGTH], saved_input_file[WORD_LENGTH];
   int i, choice, var, value;
   int saved_clause_stack_fill_pointer,
     saved_managedclause_stack_fill_pointer,
     saved_variable_stack_fill_pointer, saved_nb_back,
     saved_value_stack_fill_pointer,
     saved_bete_stack_fill_pointer;
   long begintime, endtime;
   struct tms *a_tms;
   FILE *fp_time;

   if ((argc!=2) && (argc !=3)) {
      printf("Using format: satz input_instance [-s]\n");
      return;
   }

   for (i=0; i<WORD_LENGTH; i++) saved_input_file[i]=argv[1][i];
   
     begintime = clock();
   a_tms = ( struct tms *) malloc( sizeof (struct tms));

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

   switch (build(argc, argv)) {
      case FALSE: printf("Input file error\n"); return;
      case TRUE:
	 init();
	 set_betes();
	 if (init_set_equivalencies()==NONE) 
	   printf("an inequivalence is found at top\n");
	 else {
	   if (preprocess()==NONE) {
	     printf("a contradiction is found at top\n");
	   }
	   else
	   do {
	     if (UNITCLAUSE_STACK_fill_pointer==0) {
	       if (choose_and_instantiate_variable()==NONE) 
		 backtracking();
	     }
	     if (unitclause_process()==NONE) backtracking();
	   }  while ((VARIABLE_STACK_fill_pointer > 0)
		     && (!(satisfiable())));
         }
	 break;
      case NONE: printf("An empty resolvant is found!\n"); break;
   }
   
   endtime=clock();
   times(a_tms); endtime = a_tms->tms_utime;

   if (satisfiable()) {
     printf ("****the instance is satisfiable *****\n");
     if (verify_solution()) {
        printf ("****verification of solution is OK****\n");
        print_values(NB_VAR, saved_input_file);
     }
     else
        printf ("****I'm sorry, your program is wrong****\n");
   }
  else {
     printf ("****the instance is unsatisfiable *****\n");
  }
  printf("eqsatz20 %s %5.3f %ld %ld %ld %ld %ld %d %d %d %d\n", 
	  saved_input_file, ((double)(endtime-begintime)/CLK_TCK), 
	  STATIC_NB_BETE, TOTAL_NB_BETE, NB_UNIT, NB_BRANCHE, NB_BACK,  
          satisfiable(), NB_VAR, INIT_NB_CLAUSE, NB_CLAUSE-INIT_NB_CLAUSE);

  fp_time = fopen("timetable", "a");
  fprintf(fp_time, "eqsatz20 %s %5.3f %ld %ld %ld %ld %ld %d %d %d %d\n", 
	  saved_input_file, ((double)(endtime-begintime)/CLK_TCK), 
	  STATIC_NB_BETE, TOTAL_NB_BETE, NB_UNIT, NB_BRANCHE, NB_BACK,  
          satisfiable(), NB_VAR, INIT_NB_CLAUSE, NB_CLAUSE-INIT_NB_CLAUSE);
  fclose(fp_time);
}