/**CFile***********************************************************************

  FileName    [ varelim.c ]

  PackageName [ sat ]

  Synopsis    [ Routines for variable elimination ]

  Author      [ Hyojung Han ]

  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado

  All rights reserved.

  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions
  are met:

  Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

  Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

  Neither the name of the University of Colorado nor the names of its
  contributors may be used to endorse or promote products derived from
  this software without specific prior written permission.

  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  POSSIBILITY OF SUCH DAMAGE.]
 
******************************************************************************/
#include <setjmp.h>
#include <signal.h>
#include <string.h>
#include <stdlib.h>
#include "sat.h"
#include "util.h"

#define VERIFY_ON

/* #define __DEBUG */
/* #define DEBUG  */
#define CLENGTH_LIMIT 5

/** Duplicated from util.c **/
#define heap_left(i)	((i<<1)+1)
#define heap_right(i)	((i+1)<<1)
#define heap_parent(i)	((i-1)>>1)
  
/******************************************************************************
 * FUNCTION DECLARATIONS
 ******************************************************************************/
#ifndef CUR_DATE
#define CUR_DATE        "<compile date not supplied>"
#endif

#ifndef CUR_VER
#define CUR_VER         "U of Colorado/Boulder, CirCUs Release 2.0"
#endif

static int vel_compare_scores(satManager_t *m, long x, long y);

/******************************************************************************
 * FUNCTION DESCRIPTIONS
 ******************************************************************************/

/**Function********************************************************************

  Synopsis    [ Initialize options for preprocessing ] 

  Description [ Initialize options for preprocessing ]

  SideEffects [ This function allows external application to initialize
                the options to use variable elimination. ]

  SeeAlso     [ sat_init_options_for_distill ]

******************************************************************************/
void
sat_init_options_for_varelim(satManager_t *m) 
{

  if (m == 0) 
    fprintf(stderr, "ERROR : SAT manager is not initialized!\n");
 
  m->simplify = 1;
  m->grow = 0;
  m->nIteratePreprocess = 3;
}

/**Function********************************************************************

  Synopsis    [ Main function of variable elimination ] 

  Description [ Main function of variable elimination ]

  SideEffects [ Set m->marks[v] = 1 for a variable v eliminated.
                Reset m->marks[v] for all variables v before exiting function. 
	      ]

  SeeAlso     [ ]

******************************************************************************/
int
sat_eliminate_var_main(satManager_t *m) 
{
long i, v;
int verbosity, simplified, eliminable;
int iterations, progress, progress_n;
long cnt, nCandidates;
double btime, etime;
satHeap_t *h;
satQueue_t *subsumption_queue;

  iterations = m->nIteratePreprocess;
  btime = (double)util_cpu_time(); 

  verbosity = m->verbosity;
  subsumption_queue = m->satQueue;

  m->nInputVars = m->nVars;
  m->nInputClauses = m->clauses->size + m->learned->size;
  m->nInputLiterals = m->nCurClauseLits; 

#ifdef DEBUG
  fprintf(stdout, "CHECK : all clauses sorted before VARELIM Unit \n");
  sat_check_all_clauses_sorted(m);
#endif

  /** Initialize varElimHeap of the number 
   * of unassigned variables, and insert
   * the variables into the varElimHeap.
   **/
  h = m->varElimHeap;
  simplified = 1; 
  if (sat_implication_on_all_watched_literals(m) != 0) {
    simplified = 0;
    goto endVarElim;
  }

  if (sat_check_clauses_high_density(m) == 1) {
    if (!sat_backward_subsumption_check(m))
      simplified = 0;
    else {
      sat_init_clauses_statistics(m);
      sat_reset_all_watched_lists(m);
      sat_recover_clauses_DB(m);
      sat_remove_marked_clauses(m, m->clauses); 
      sat_remove_marked_clauses(m, m->learned); 
    }
    goto endVarElim;
  }

  if (verbosity >= 2 ) {
    fprintf(stdout, "Variable Elimiation Procedure\n");

    fprintf(stdout, "===============================[ VarElim Statistics ]=============================\n");
    fprintf(stdout, " TRIAL |          ORIGINAL         |        RESOLVENT              |    REJECT   |\n");
    fprintf(stdout, "       |    Vars  Clauses Literals |    Clauses  Literals  Lit/Cl  |   Bnd  Self |\n");
    fprintf(stdout, "==================================================================================\n");
    fprintf(stdout, "| %4ld | %7ld %8ld %8.f | %10ld %9ld %7s  | %5ld %5ld |\n", 
    	              m->nVarElimTry, h->size, m->clauses->size, m->nCurClauseLits, 
		      m->nResolvents, m->nResolventLits, "N/A", m->nVarElimReject, m->nSelfsubsume); 
    fflush(stdout);
  }
  
  progress = 0;
  nCandidates = h->size;

beginVarElim:;

  if (!sat_backward_subsumption_check(m)) {
    simplified = 0;
    goto endVarElim;
  }
  m->nSubsumeTry++;

  v = 0;
  for (cnt = 0; h->size > 0; cnt++) {
    if (m->nResolventLits > 0 && verbosity >= 2 && cnt%100 == 0) {
      fprintf(stdout, "| %4ld | %7ld %8ld %8.f | %10ld %9ld %7.2f  | %5ld %5ld |\n", 
  	      m->nVarElimTry, nCandidates - m->nEliminatedVars, m->clauses->size - m->nEliminatedCls, 
	      (m->nCurClauseLits + m->nResolventLits) - m->nEliminatedLits, 
	      m->nResolvents, m->nResolventLits, (double)m->nResolventLits/(double)m->nResolvents, 
	      m->nVarElimReject, m->nSelfsubsume); 
      fflush(stdout);
    }
 
    v = vel_heap_remove_min(m);
    if (m->values[v] != 2)   continue;

    m->nVarElimTry++;
    eliminable = sat_eliminate_var(m, v);
    if (eliminable == 1) {  
      /*  add the resolvents generated */
      m->values[v] = 3;
      sat_mark_clauses_of_var_deleted(m, v);
      sat_add_resolvents_from_lit_pool(m, m->redundant);

      /*  store eliminated variable to find its value 
       *  if problem is satisfiable 
       */  
      m->elimtable = sat_array_insert(m->elimtable, v);
      m->nEliminatedVars++;
    }
    else if (eliminable == 0)
      m->nVarElimReject++;
    else sat_implication_on_all_watched_literals(m); 

    if (!sat_backward_subsumption_check(m) || m->clauses->size == 0 || m->status < 2) {
      fprintf(stdout, "Solved in preprocessing level!\n");
      simplified = 0;
      if (m->clauses->size == 0)  
        m->status = 1; 

      goto endVarElim;
    }
  }

  if (!m->eliminateVar) {
    sat_gather_touched_clauses(m);
    if (subsumption_queue->size > 0 || h->size > 0) {
      if (sat_implication_on_all_watched_literals(m) != 0) {
        simplified = 0;
        goto endVarElim;
      }
      goto beginVarElim;
    }  
   
    progress_n = sat_elimination_progress(m);
    if (iterations > 0 && (progress_n - progress) > 10) {
      progress = progress_n;
      sat_insert_clauses_into_subsumption_check_queue(m, m->clauses);
      if (sat_implication_on_all_watched_literals(m) != 0) {
        simplified = 0;
        goto endVarElim;
      }
      if (subsumption_queue->size > 0) {
        iterations--;
        goto beginVarElim;
      }
    }
  }

  if (verbosity >= 2) {
    fprintf(stdout, "| %4ld | %7ld %8ld %8.f | %10ld %9ld %7.2f  | %5ld %5ld |\n", 
  	      m->nVarElimTry, nCandidates - m->nEliminatedVars, m->clauses->size - m->nEliminatedCls, 
	      (m->nCurClauseLits + m->nResolventLits)-m->nEliminatedLits, m->nResolvents, m->nResolventLits, 
	      (double)m->nResolventLits/(double)m->nResolvents, m->nVarElimReject, 
	      m->nSelfsubsume); 
    fflush(stdout);
    fprintf(stdout, "==================================================================================\n");
  }

  sat_init_clauses_statistics(m);
  sat_reset_all_watched_lists(m);
  sat_recover_clauses_DB(m);
  sat_remove_marked_clauses(m, m->clauses); 
  sat_remove_marked_clauses(m, m->learned); 

  if (verbosity >= 2)
    sat_print_clauses_histogram(m);

  /* remove pure literals */
  if (!m->allSat) {
    for(i=1; i<=m->nVars; i++) {
      if (m->values[i] == 2) {
        if(m->pure[i] == 1) {
          sat_enqueue_check(m, i<<1, 0);
        }
        else if(m->pure[i] == 2) {
          sat_enqueue_check(m, (i<<1)+1, 0);
        }
      }	
    }
  } 

endVarElim:;
  etime = (double)util_cpu_time();
  m->elimTime = (etime - btime) / 1000.0;
  sat_report_result_for_var_elim(m);
  fflush(stdout);
  
  return simplified;
}

/**Function********************************************************************

  Synopsis    [ Calculate progress in elimination ] 

  Description [ Calculate progress in elimination ]

  SideEffects [ retrun 0 if progress is negligible, otherwise return progress ]

  SeeAlso     [ ]

******************************************************************************/
int
sat_elimination_progress(satManager_t *m)
{
double progress;

  progress = 0;
  progress = 100 * (double)m->nEliminatedLits / (double)m->nLits;

  return (int)progress;
}

/**Function********************************************************************

  Synopsis    [ Write eliminated data base into a file] 

  Description [ Write eliminated data base into a file.
                Note that it doesn't write them in DIMACS. ]

  SideEffects [  ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_write_eliminated_DB(satManager_t *m, int turnOffClauses)
{
long i, j, size, csize;
long v, lit;
char filename[1024];
FILE *fp;
satArray_t *arr;
satClause_t *c;

  sprintf(filename, "cnf.elim");
  fp = fopen(filename, "w");
  fprintf(fp, "===========\n");
  fprintf(fp, " variables \n");
  fprintf(fp, "===========\n");

  arr = m->elimtable;
  size = arr->size; 
  for (i = 0; i < size; i++) {
    v = arr->space[i];     
    fprintf(fp, "%ld ", v);

    if ((i % 15) == 1) 
      fprintf(fp, "\n");
  }
  fprintf(fp, "\n");

  if (!turnOffClauses) {
    fprintf(fp, "===========\n");
    fprintf(fp, " clauses   \n");
    fprintf(fp, "===========\n");

    arr = m->deleted; 
    for (i = 0; i < arr->size; i++) {
      c = (satClause_t*)arr->space[i];
      csize = SATSizeClause(c);
      fprintf(fp, "%d %f (", (int) c->size & SATCTypeMask, c->info.activity);
      for (j = 0; j < csize; j++) {
        lit = c->lits[j];
	v = lit >> 1;
	fprintf(fp, "%c%ld ", lit & 1 ? '-' : ' ', v);
      }
      fprintf(fp, ")\n");
    }
  }
  
  fclose(fp);
}

/**Function********************************************************************

  Synopsis    [ Apply variable elimination ] 

  Description [ Apply variable elimination ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
int
sat_eliminate_var(satManager_t *m, long v)
{
int eliminable, first;
long lit;
long cnt, i, j, cntLits;
satClause_t *posc, *negc;
satArray_t *pos, *neg;

  m->temp->size = 0;
  cntLits = 0;
  first = 0;
  
  /** Get the positive and 
   *  negative  occurrence list
   **/
  lit = v << 1;
  pos = m->wls[lit^1];
  neg = m->wls[lit];

  if (!pos || pos->size == 0) 
    return 1; 

  else if (!neg || neg->size == 0) 
    return 1;
  
  /** Apply resolution operation for each pair
   *  of postive and negative occurrence clauses
   **/
  cnt = 0;
  for (i = 0; i < pos->size; i++) {
    posc = (satClause_t*)pos->space[i];
    if (SATClauseVisited(posc)) {
      pos->space[i] = pos->space[--pos->size];
      i--;
      continue;
    }
    first++;

    /** continue only if the clauses of both
     *  sign currently exist 
     **/
    cntLits += posc->size;

    for (j = 0; j < neg->size; j++) {
      negc = (satClause_t*)neg->space[j];
      if (SATClauseVisited(negc)) {
        neg->space[j] = neg->space[--neg->size];
        j--;
        continue;
      }
      if (first == 1)  
        cntLits += negc->size;
	   
       eliminable = sat_merge_sort_literals(m, posc, negc, i, j, v);
           
       if (eliminable == 1) {

         /** Two criterions to limit the size of database : 
	  *  	1. the number of clauses to be added 
	  *  	2. the average number of literals to be added
	  **/
         if ((++cnt > ((m->scores[lit] + m->scores[lit|1]) + m->grow))  || 
#ifdef VERIFY_ON
	      (((double)(m->redundant->size - (cnt<<1)) /cnt) > (CLENGTH_LIMIT * 2*((double)m->nCurClauseLits/m->nClauses)))) {
#else
	      (m->redundant->size - cnt) /cnt > (CLENGTH_LIMIT *(m->nCurClauseLits/m->nClauses))) {
#endif
          m->redundant->size = 0;
          return  0;
        }
      } 
      else if (eliminable == 2) {
        /* Skip to next i due to posc selfsubsubsumed */
        m->nSelfsubsume++;
	i--;
        break;
      }
      else if (eliminable == 3) {
        /* Break j loop due to negc selfsubsumed */
        m->nSelfsubsume++;
        j--;
      }
      else if (eliminable == 4) {
        i--;
	break; 
      }
        else if (eliminable == 5) {
        j--;
      }
      else 
	continue;
    }
  }

  return 1;
}

/**Function********************************************************************

  Synopsis    [ Build occurency lists with watched lists ]

  Description [ Build occurency lists with watched lists ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_build_occurrence_list(satManager_t *m)
{
long i, size;
satClause_t *c;
satArray_t *cls;

  cls = m->clauses;
  size = cls->size;
  for (i=0; i<size; i++) {
    c = (satClause_t*)cls->space[i];
    if (SATClauseVisited(c)) {
      c->size -= SATCVisited;
    }
    else if (SATSizeClause(c) > 1) { 
      sat_add_all_watched_literal(m, c);
      sat_queue_insert(m->satQueue, (long)c);
    }  
  }

  cls = m->learned;
  size = cls->size;
  for (i=0; i<size; i++) {
    c = (satClause_t*)cls->space[i];
    if (SATClauseVisited(c)) {
      c->size -= SATCVisited;
    }
    else if (SATSizeClause(c) > 1) { 
      sat_add_all_watched_literal(m, c);
      sat_queue_insert(m->satQueue, (long)c);
    }
  }
}

/**Function********************************************************************

  Synopsis    [ Insert clauses into subsumption check queue ]

  Description [ Insert clauses into subsumption check queue ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_insert_clauses_into_subsumption_check_queue(satManager_t *m, satArray_t *clauses)
{
long i, j, size, csize;
long v, lit;
satClause_t *c;

  size = clauses->size;
  for (i = 0; i < size; i++) {
    c = (satClause_t*)clauses->space[i];
    if (SATClauseVisited(c))	continue;
    
    csize = SATSizeClause(c);
    if (csize == 1) {
      sat_enqueue_check(m, c->lits[0], c);
    }
    else {
      if (!sat_squeeze_clause(m, c) || 
          ((double)SATSizeClause(c)) > CLENGTH_LIMIT * ((double)m->nCurClauseLits/(double)m->nClauses)) 
        continue; 

      for(j = 0; j < csize; j++) {
        lit = c->lits[j];
        v = lit >> 1;
	if ((m->scores[lit] > 10 && m->scores[lit|1] > 10) || (m->scores[lit] + m->scores[lit|1] > 40)) 
	  continue;  
	
        if (m->values[v] == 2) {
          if(m->varElimHeap->indices[v] >= 0)
            vel_heap_down(m, m->varElimHeap->indices[v]);
          else  
            vel_heap_insert(m, v);
        }	  
      }
      sat_queue_insert(m->satQueue, (long)c);
    }
  }
}

/**Function********************************************************************

  Synopsis    [ Merge and sort literals ]

  Description [ Merge and sort literals 
                  
		Encoding eliminable : 
		  0 -> tautology 
		  1 -> eliminable and addable the resolvent 
		  2 -> eliminable and selfsubsuming p
		  3 -> eliminable and selfsubsuming q
		  4 -> eliminable and selfsubsumming both P & q
              ]

  SideEffects [ Precondition : each set of literals of a cluase is
   		suppose to be sorted when it is instantiated. ]

  SeeAlso     [ ]

******************************************************************************/
int
sat_merge_sort_literals(
	satManager_t *m,
	satClause_t *cp,
	satClause_t *cq,
	long cpindex,
	long cqindex,
	long v)
{
int eliminable, beginLit;
long i, j, nCommon;
long cpsize, cqsize, crsize;
long wlpindex, wlqindex, vpindex, vqindex;
long vp, vq, litp, litq, value;
satArray_t *rcarray;

  rcarray = m->redundant;
  /* Use the first literal position
   * as a flag for deletion
   */
  beginLit = rcarray->size;
  rcarray = sat_array_insert(rcarray, 0);
  eliminable = 1;

#ifdef __DEBUG
    fprintf(stdout, "  ----------------------------------------------\n");  
    fprintf(stdout, "  * Resolve on VAR %d\n", v);  
    fprintf(stdout, "            (");  
    sat_print_clause_simple(m, cp);  
    fprintf(stdout, ") \n            (");  
    sat_print_clause_simple(m, cq);  
    fprintf(stdout, ") \n");  
    fprintf(stdout, "  ----------------------------------------------\n");  
#endif

  vp = vq = litp = litq = 0;
  vpindex = vqindex = 0;
  i = j = 0;
  crsize = 0;
  cpsize = SATSizeClause(cp);
  cqsize = SATSizeClause(cq);
  nCommon = 0;
  wlpindex = (v<<1)^1; 
  wlqindex = (v<<1);
  while (i<cpsize || j<cqsize) {
    if (i < cpsize) {
      litp = cp->lits[i];
      vp = SATVar(litp);
      value = m->values[vp];

      /* skip the false literals of p */
      if (value < 2) { 
        if (value^(litp&1)) {
          cp->size |= SATCVisited;         
          sat_delete_clause_from_watched_list(m, cp, wlpindex, cpindex); 
          rcarray->size = beginLit;
	  m->redundant = rcarray;
#ifdef __DEBUG
	  fprintf(stdout, "Satisfied clause on positive literal %ld = %d\n", vp, (int)value);
#endif 
          return 4;
        }
        else {
          i++;
          continue;
        }
      }	

      /* skip the pivot variable and 
       * storing its wl index in p
       */
      if (vp == v) {
	vpindex = i++;
        continue;
      }
    }
    
    if (j < cqsize) {
      litq = cq->lits[j];
      vq = SATVar(litq);
      value = m->values[vq];
      /* skip the false literals of q */
      if (value < 2) {
        if (value^(litq&1)) {
          cq->size |= SATCVisited;         
          sat_delete_clause_from_watched_list(m, cq, wlqindex, cqindex); 
          rcarray->size = beginLit;
	  m->redundant = rcarray;
#ifdef __DEBUG
	  fprintf(stdout, "Satisfied clause on negative literal %ld = %d\n", vq, (int)value);
#endif
          return 5;
        }
        else {
          j++;
          continue;
       }
     }	
      /* skip the pivot variable and
       * store its wl index in q
       */
      if (vq == v) {
	vqindex = j++;
        continue;
      }
    }

    /* check common literals  
     */
    if (vp == vq) {
      /* return "eliminable" 
       * for tautology case 
       */
      if (litp == (litq^1)) {
        /* remove the current resolvent */
        rcarray->size = beginLit;
	m->redundant = rcarray;
        return 0;
      }

      
      nCommon++;
      rcarray = sat_array_insert(rcarray, litp);
      j++;
      i++;
    }
    /* insert q's literal because of no p's literal left */ 
    else if (i >= cpsize) { 
      rcarray = sat_array_insert(rcarray, litq);
      j++;
    }
    /* insert p's literal because of no q's literal left */ 
    else if (j >= cqsize) {
      rcarray = sat_array_insert(rcarray, litp);
      i++;
    }
    /* insert the literal with smaller index */ 
    else if (vp < vq) {
      rcarray = sat_array_insert(rcarray, litp);
      i++;
    }
    else { 
      rcarray = sat_array_insert(rcarray, litq);
      j++;
    }

    crsize++;
  }
  
  if (m->coreGeneration) {
    rcarray = sat_array_insert(rcarray, (long)cp);
    rcarray = sat_array_insert(rcarray, (long)cq);
  }
  rcarray->space[beginLit] = -crsize;
  m->redundant = rcarray;

#ifdef __DEBUG
  sat_check_clause_after_merge_sort(m, rcarray, beginLit);
#endif
  
#if 1 /* to enable self-subsumption check */
  
  /** part for checking selfsubsumption **/

  /* p is subsumed by the resolvent */
  if (nCommon == cqsize-1) {
    if (!sat_strengthen_clause(m, cp, vpindex)) 
      m->nNewUnitLits++; 

#ifdef __DEBUG
    fprintf(stdout, "  [ Strengthened ] (");  
    sat_print_clause_simple(m, cp);  
    fprintf(stdout, ")\n");  
#endif

    /* discard the current resolvent */
    rcarray->size = beginLit;
 
    /** TODO : Disable the following function to speed up **/
    sat_delete_redundant_resolvents(m, cp);
    sat_delete_clause_from_watched_list(m, cp, wlpindex, cpindex); 
    eliminable = 2;
  }

  /* q is subsumed by the resolvent */
  if (nCommon == cpsize-1) {
    /* avoid clause duplication in strengthening */
    if (eliminable < 2) {
      eliminable = 3;
      if (!sat_strengthen_clause(m, cq, vqindex)) 
        m->nNewUnitLits++; 

#ifdef __DEBUG
        fprintf(stdout, "  [ Strengthened ] (");  
        sat_print_clause_simple(m, cq);  
        fprintf(stdout, ")\n");  
#endif

    }
    /* discard the current resolvent */
    rcarray->size = beginLit;
    sat_delete_redundant_resolvents(m, cq);
    sat_delete_clause_from_watched_list(m, cq, wlqindex, cqindex); 
  }

#endif /* #if 0 to disable self-subsumption check */

#ifdef __DEBUG
  if (rcarray->size) {
    fprintf(stdout, "  [ Resolvent ] ");  
    sat_print_clause_array_part(m, rcarray, beginLit+1, rcarray->size);
    fprintf(stdout, "\n");  
  }
#endif 
  return eliminable;
}

/**Function********************************************************************

  Synopsis    [ Merge the literals of two clauses ] 

  Description [ Merge the literals of two clauses ]

  SideEffects [ cp and cq must be compared by the
                size when this function is called.
		Thus _cq is always smaller one.]

  SeeAlso     [ ]

******************************************************************************/
int
sat_merge_literals(
	satManager_t *m,
	satClause_t *cp, 
	satClause_t *cq, 
	satArray_t *rcarray,
	long cpindex,
	long cqindex,
	long v) 
{
int cp_smaller;
long i, j, index, common, flag;
long cpsize, cqsize;
long _cpindex, wlpindex;
long vp, vq, litp, litq;
satClause_t *_cp, *_cq;

  rcarray->size = 0;

  cpsize = SATSizeClause(cp);
  cqsize = SATSizeClause(cq);

#ifdef __DEBUG
    fprintf(stdout, "  * Resolve ");  
    sat_print_clause_simple(m, cp);  
    fprintf(stdout, "  (x) ");  
    sat_print_clause_simple(m, cq);  
    fprintf(stdout, "\n");  
#endif

  cp_smaller = cpsize < cqsize;
  _cp = cp_smaller ? cq : cp;
  _cq = cp_smaller ? cp : cq;
  _cpindex = cp_smaller ? cqindex : cpindex;
  wlpindex = v<<1;
  index = 0; 
  common = 0;		
  flag = 0;
  cpsize = SATSizeClause(_cp);
  cqsize = SATSizeClause(_cq);
  for (i=0; i<cqsize; i++) {
    litq = _cq->lits[i];
    vq = SATVar(litq);
    if (m->values[vq] != 2) continue;

    if (SATVar(litq) != v) { 
      for (j = 0; j < cpsize; j++) {
        litp = _cp->lits[j];
        vp = SATVar(litp);
        if (m->values[vp] != 2) continue;
        flag = 0;

        if (vp == vq) {
	  /** 1. Check tautology :
	   *  Value 0 is returned. 
	   *  Out clause then can not be used.
	   **/
	  if (litp == (litq^1)) 
	    return 0;
	  else {
	    /** count the number of common literals 
	     * */
	    common++; 	    
	    flag = 1;
	  }
	}
      }
      if (flag == 0)
        rcarray = sat_array_insert(rcarray, litq);
    }
  }

  for (i=0; i<cpsize; i++) {
    litp = _cp->lits[i];
    vp = SATVar(litp);
    /** 2. Remember the position of the variable v
     *     to be eliminated. Doing so is a hand in
     *     strengthening clause for selfsubsumed case.
     **/
    if (vp == v) {
      index = i;
    }
    else 
     rcarray = sat_array_insert(rcarray, litp);
  }

  /** 3. Check selfsubsumption :
   *  The case when all the literals of 
   *  _cq but the literal v also occur
   *  in cp. Then value 1 is returned.
   *  Out clause must be cp strengthed.
   **/
  if (common == cqsize - 1) {
    /* don't remove this clause strengthened */
    m->nSelfsubsume++;

    /** TODO: Copy the clause before strengthening 
     *  for satisfying ussignment proof of elimination.
     **/
 
    if (!sat_strengthen_clause(m, _cp, index)) {
      m->nNewUnitLits++;    
    }
    
    /** Keep recording the clause _cp strengthened 
     *  as a dependent of _cq. This information may be
     *  used to delete _cq  when yet it is not deleted 
     *  by eliminating a variable, while it is also 
     *  subsumed by the _cq strengthened, and irredundant.
     **/

#ifdef __DEBUG
    fprintf(stdout, "    *Strengthened to ");  
    sat_print_clause_simple(m, _cp);  
    fprintf(stdout, "\n");  
#endif

    /** Remove all resolvents depend on 
     *  either the clauses _cp or _cq.
     *  Checking the resolvents associated 
     *  with _cq(shorter) is optional as commented 
     *  above, because not all of them are subsumed 
     *  by the strengthened clause, while the all 
     *  of resolvents for _cp(longer, strengthened) 
     *  is apparently redundant.
     **/
    /*sat_remove_dependent_resolvents(m, _cp);*/
    sat_delete_clause_from_watched_list(m, _cp, wlpindex, _cpindex);

    if (common == rcarray->size) {
 
#ifdef __DEBUG
      fprintf(stdout, "   * Remove the redundancy : ");  
      sat_print_clause_simple(m, _cq);  
      fprintf(stdout, "\n");
#endif
      
      _cq->size |= SATCVisited; /* set the clause to be deleted */ 
      return 4;
    }
    return (3 - cp_smaller);
  }

  m->clearned = rcarray;
  return 1;
}

/**Function********************************************************************

  Synopsis    [ Check backward subsumption and selfsubsumption ] 

  Description [ Check backward subsumption and selfsubsumption 
  		by resolution on CNF clauses ].

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
int 
sat_backward_subsumption_check(satManager_t *m)
{
int verbosity;
int cnt, subsumed, deleted_literals;
long i, j, csize, index;
long lit, v, best, bestLit, bestSize;
satQueue_t *subsumption_queue;
satClause_t *c, *ct;
/*satClause_t *cprime;*/
satArray_t *occur;
//#define DEBUG

int test;

  verbosity = m->verbosity;
  
  //m->clearned->size = 0;

  cnt = subsumed = deleted_literals = 0;
  subsumption_queue = m->satQueue;
  while (subsumption_queue->size > 0) {
    test = 0;
    /*if (m->status == 0) {
      fprintf(stdout, "conflict during bsubsumption check for CL(");
      sat_print_clause(m, c);
      fprintf(stdout, ") strengthened from CL");
      sat_print_array_as_clause(m, m->clearned);
    }
    m->clearned->size = 0; */

    c = (satClause_t*)sat_queue_pop(subsumption_queue);
   
    /*for (i = 0; i <SATSizeClause(c); i++) {
      m->clearned = sat_array_insert(m->clearned, c->lits[i]);
    }
    if (c->lits[0] == ((61935<<1)|1) && c->lits[1] == (75503<<1) &&
		    c->lits[2] == (75505<<1)) 
      test = 1;
    */

    if (SATClauseVisited(c))  continue;	
    
    if (verbosity >= 3 && cnt++ % 1000 == 0)
      fprintf(stdout, "subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", (int)subsumption_queue->size, subsumed, deleted_literals); 
    
    /** Find the best variable to scan **/
    csize = SATSizeClause(c);
    if (csize == 1)
      continue;

    bestLit = c->lits[0];
    best = SATVar(bestLit);
    for (i=1; i<csize; i++) {
      lit = c->lits[i];
      v = SATVar(lit);
      bestSize = m->scores[bestLit^1] + m->scores[bestLit];
      if ((m->scores[lit^1] + m->scores[lit]) < bestSize) {
        bestLit = lit; 
	best = v;
      }
    }
    
    /** Search all the candidates on the same sign **/
    occur = m->wls[bestLit^1]; 
    if (occur == 0)  continue;

    for (j = 0; j < occur->size; j++) {
      ct = (satClause_t*)occur->space[j];

      /*if (test) {
	fprintf(stdout, "CT(");
        sat_print_clause(m, ct);
	fprintf(stdout, ") %s%s\n", SATClauseVisited(ct)?
			"visited":"", ct == c? " duplicate":" ");
      }*/

      /*if (SATClauseVisited(c))  
        break;
      else*/ if (!SATClauseVisited(ct) && ct != c) {
        lit = sat_subsume_on_sorted_clauses(m, c, ct);

        /*if (test && lit > 0)  {
	  fprintf(stdout, "subsumed with lit = %d => C(", (int)lit);
          sat_print_clause_simple(m, c);
	  fprintf(stdout, ") X CT(");
	  sat_print_clause_simple(m, ct);
	  fprintf(stdout, ")\n");
        }*/

#if 0
	int check_subsume = (int)sat_subsume_on_clauses(m, c, ct);
        if (check_subsume == 0 && lit != -1) {
          fprintf(stdout, "ERROR : backwardsumption check failed!\n");
          fprintf(stdout, "(");
          sat_print_clause_simple(m, c);
          fprintf(stdout, ") & (");
          sat_print_clause_simple(m, ct);
          fprintf(stdout, ")\n");
	  fprintf(stdout, "%d but subsumption checked %d\n", check_subsume, (int)lit);
	  /*exit(0);*/
	}
#endif

	if (lit == 0) {
	  /** if redudnat clause is original and subsuming 
	   *  clause is conflict clause, the conflict clause
	   *  must not blong to conflict clauses.
	   *  Note that the conflict must be handled when 
	   *  the CNF data is simplified and recovered after
	   *  backward subsumption check.
	   **/
	  if (SATClauseLearned(c) && !SATClauseLearned(ct))
	     c->size -= SATCLearned;

          sat_set_clause_deleted(m, ct);
          subsumed++;
        } 
	else if (lit > 0) {
	 /** HHJ : storing clauses deledted by selfsubsumption
	  *        is unsure now. Proof of unsatisfiability 
	  *        without such cleauses are still valid.
	  **/
	 /* if (m->coreGeneration) {
	    m->deleted = sat_array_insert(m->deleted, (long)c);
            cprime = sat_copy_clause(m, c); 
	    sat_make_resolution_graph(c, cprime);
	    c->size |= SATCVisited;
	    c = cprime; 
          }
         */
	  m->nBackwardSelfsubsume++;
	  /** strengthen clause with lit **/ 
	  if (SATSizeClause(c) == SATSizeClause(ct)) {
	    if (SATClauseLearned(c) && !SATClauseLearned(ct))
	      c->size -= SATCLearned; 

            sat_set_clause_deleted(m, ct);
            subsumed++;
            index = sat_get_literal_index_of_clause(m, c, lit^1);
            if (!sat_strengthen_clause(m, c, index)) {
	      if (sat_implication_on_all_watched_literals(m) != 0) 
                return 0;
	    } 
	    else {
	      /* instead of sat_clean_all_watched_list_of_literal(m, lit^1);
	       */
              sat_delete_clause_from_watched_list(m,  c, lit, -1);
	    }
	  }
	  else {
            index = sat_get_literal_index_of_clause(m, ct, lit);
	    if (!sat_strengthen_clause(m, ct, index)) {
	      if (sat_implication_on_all_watched_literals(m) != 0)
                return 0;
	    } 
	    else {
	      /* instead of sat_clean_all_watched_list_of_literal(m, lit);
	       */
              sat_delete_clause_from_watched_list(m,  ct, lit^1, -1);
	      j--;
	      continue;
	    }
	  }
          occur = m->wls[bestLit^1]; 
	}
	else if (lit == -2) {
          sat_set_clause_deleted(m, c);
          subsumed++;
          break; 
	}
      }
    }

    if (SATClauseVisited(c))  
        continue;
    /** Search all the candidates on the opposite sign **/
    occur = m->wls[bestLit]; 
    if (occur == 0)  continue;

    for (j = 0; j < occur->size; j++) {
      ct = (satClause_t*)occur->space[j];

      /*if (test) {
	fprintf(stdout, "CT(");
        sat_print_clause(m, ct);
	fprintf(stdout, ") %s\n", SATClauseVisited(ct)?
			"visited":"", ct == c? " duplicate":" ");
      }*/

      /*if (SATClauseVisited(c))  
        break;
      else*/ if (!SATClauseVisited(ct) && ct != c) {
        lit = sat_subsume_on_sorted_clauses(m, c, ct);
        /*if (test)  fprintf(stdout, "lit = %d\n", lit);*/

#if 0 
	int check_subsume = (int)sat_subsume_on_clauses(m, c, ct);
        if (check_subsume == 0 && lit != -1) {
          fprintf(stdout, "ERROR : backwardsumption check failed on opposite, %ld!\n", lit);
          fprintf(stdout, "(");
          sat_print_clause_simple(m, c);
          fprintf(stdout, ") & (");
          sat_print_clause_simple(m, ct);
          fprintf(stdout, ")\n");
	  fprintf(stdout, "%d but subsumption checked %d\n", check_subsume, (int)lit);
	  exit(0);
	}
#endif

	if (lit == 0) {
	  if (SATClauseLearned(c) && !SATClauseLearned(ct))
	     c->size -= SATCLearned; 

          sat_set_clause_deleted(m, ct);
          subsumed++;
        } 
	else if (lit > 0) {
	 /** HHJ : storing clauses deledted by selfsubsumption
	  *        is unsure now. Proof of unsatisfiability 
	  *        without such cleauses are still valid.
	  **/
	  /*if (m->coreGeneration) {
	    m->deleted = sat_array_insert(m->deleted, (long)c);
            cprime = sat_copy_clause(m, c);
	    sat_make_resolution_graph(c, cprime);
	    c->size |= SATCVisited;
	    c = cprime;  
          }*/

	  m->nBackwardSelfsubsume++;
	  /** strengthen clause with lit **/ 
          if (SATSizeClause(c) == SATSizeClause(ct)) {
	    if (SATClauseLearned(c) && !SATClauseLearned(ct))
	      c->size -= SATCLearned; 

            subsumed++;
            sat_set_clause_deleted(m, ct);
            index = sat_get_literal_index_of_clause(m, c, lit^1);
            if (!sat_strengthen_clause(m, c, index)) {
	      if (sat_implication_on_all_watched_literals(m) != 0)
                return 0;
	    }
	    else { 
	      /* instead of sat_clean_all_watched_list_of_literal(m, lit);
	       * using following
	       */
              sat_delete_clause_from_watched_list(m,  c, lit, -1);
               
	    }
	  }
	  else { 
            index = sat_get_literal_index_of_clause(m, ct, lit);
	    if (!sat_strengthen_clause(m, ct, index)) {
	      if (sat_implication_on_all_watched_literals(m) != 0)
                return 0;
	    }
	    else { 
	      /* instead of sat_clean_all_watched_list_of_literal(m, lit);
	       * using following
	       */
              sat_delete_clause_from_watched_list(m,  ct, lit^1, -1);
	      j--;
	      continue;
	    }
          }
          occur = m->wls[bestLit]; 
	}
	else if (lit == -2) {
          sat_set_clause_deleted(m, c);
          subsumed++;
          break; 
	}
      }
    }
  }
  /*m->clearned->size = 0;*/

  return 1;
}



/**Function********************************************************************

  Synopsis    [ Get literal index of clause ] 

  Description [ Get literal index of clause ] 
  
  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
long 
sat_get_literal_index_of_clause(satManager_t *m, satClause_t *c, long lit)
{
long i, csize;

  csize = SATSizeClause(c);
  for (i=0; i<csize; i++) {
    if (c->lits[i] == lit)
      return i;
  }
  
  fprintf(stdout, "ERROR : literal %s%ld does not exist in CL(", lit&1 ? "-":"", lit>>1);
  sat_print_clause_simple(m, c);
  fprintf(stdout, ")\n");
  return -1;
}

/**Function********************************************************************

  Synopsis    [ Set clause to be deleted ] 

  Description [ Set clause to be deleted with updating some of sturctures : 
                
		m->scores : variable scores
		m->varElimHeap : variable elimination heap

  SideEffects [ Preconditions : All the literals of a clause are sorted. ]

  SeeAlso     [ sat_subsume_on_clauses]

******************************************************************************/
void 
sat_set_clause_deleted(satManager_t *m, satClause_t *c)
{
long i, csize;
long lit;
satHeap_t *h;
 
  h = m->varElimHeap;

  csize = SATSizeClause(c);
  for (i=0; i<csize; i++) {
    lit = c->lits[i];

    if (h->indices[lit>>1] >= 0) {
      m->nEliminatedLits++; 
      m->scores[lit]--;
      vel_heap_up(m, h->indices[lit>>1]);
    }
  }
  c->size |= SATCVisited;
  m->nEliminatedCls++;
}

/**Function********************************************************************

  Synopsis    [ Check if a clause selfsubsumes/subsumes the other clause ] 

  Description [ Check if a clause selfsubsumes/subsumes the other clause.
                Invariants:
		  cp subsumes cq -> sorted(cp) and sorted (cq) and 
		                   forall i, lit[i] \in cp \and lit[i] \in cq

  		Result:
		 -2  - cp is subsumed by level zero unit clauses 
		 -1  - No subsumption or simplification
		  0  - Clause cp subsumes Clause cq
		  p  - The literal p can be deleted from cq ]

  SideEffects [ Preconditions : the literals of a clause are sorted on 
  				the function call. ]

  SeeAlso     [ sat_subsume_on_clauses]

******************************************************************************/
DD_INLINE long 
sat_subsume_on_sorted_clauses(
	satManager_t *m, 
	satClause_t *cp, 
	satClause_t *cq)
{
char value;
int ret;
long i, j;
long cpsize, cqsize;
long litp, litq, vp, vq;

  cpsize = SATSizeClause(cp);
  cqsize = SATSizeClause(cq);

  /** check preliminary condition **/
  if (cqsize < cpsize || (cp->info.abstract & ~(cq->info.abstract)) != 0)
    return -1;

  ret = 0;
  i = j = 0;
  while (i < cpsize) {
    /** No subsumption found **/
    if (j >= cqsize) 
      return -1;

    /** skip satisfied clause or false literals **/ 
    litp = cp->lits[i];
    vp = SATVar(litp);
    value = m->values[vp];
    if (value < 2) {
      if ((value^(litp&1)) == 1) {
        return -2;
      }
      else {
        i++;
        goto ok;
      }
    }

    litq = cq->lits[j];
    vq = SATVar(litq);
    value = m->values[vq];
    if (value < 2) {
      if ((value^(litq&1)) == 1) {
      cq->size |= SATCVisited;
        return -1;
      }  
      else {
        j++;
        goto ok;
      }
    }

    /** check common literals **/ 
    if (litp == litq) {
      i++;
      j++;
    }
    /** check for selfsubsumption **/
    else if (ret == 0 && litp == (litq^1)) {
      ret = litq;
      i++;
      j++;
    }
    else if ((ret > 0 && vp == vq) || vp < vq)
      return -1; 
    else 
      j++;

  ok:;
  }

  return ret;
}

/**Function********************************************************************

  Synopsis    [ Check if a clause selfsubsumes/subsumes the other clause ] 

  Description [ Check if a clause selfsubsumes/subsumes the other clause.
  		This function does check subsumption relation of the two clauses
		with a conventional quadratic operation. In addition, one can 
		use this function to verify the function sat_subsume_on_sorted
		_clauses.

  SideEffects [ ]

  SeeAlso     [ sat_subsume_on_sorted_clauses ]

******************************************************************************/
DD_INLINE long 
sat_subsume_on_clauses(
	satManager_t *m, 
	satClause_t *cp, 
	satClause_t *cq) 
{
long i, j, cpsize, cqsize;
long ret;

  cpsize = SATSizeClause(cp);
  cqsize = SATSizeClause(cq);

  /** check preliminary condition **/
  if (cqsize < cpsize || (cp->info.abstract & ~(cq->info.abstract)) != 0)
    return -1;

  ret = 0;
  i = j = 0;

  for (i=0; i<cpsize; i++) {
    if ((m->values[SATVar(cp->lits[i])]^(cp->lits[i]&1)) == 1) 
      return -2;

    if ((m->values[SATVar(cp->lits[i])]^(cp->lits[i]&1)) == 0) 
      continue;

    for (j=0; j<cqsize; j++) {

      if ((m->values[SATVar(cq->lits[j])]^(cq->lits[j]&1)) == 1) 
        return -1;

      if ((m->values[SATVar(cq->lits[j])]^(cq->lits[j]&1)) == 0) 
        continue;


      if (cp->lits[i] == cq->lits[j])
        goto ok;
      else if (ret == 0 && cp->lits[i] == (cq->lits[j] ^ 1)) {
        ret = cq->lits[j];
	goto ok;
      }
    }
    return -1;

  ok:;
  }

  return ret;
}

/**Function********************************************************************

  Synopsis    [ Strengthen clause ] 

  Description [ Strengthen clause ]

  SideEffects [ 1. Copy the clause into the deleted clause list
		   before strenthening.
		2. Return 0 if it is pure, or return 1 otherwise.
	  	3. Do not insert the strengthen result into 
		   the list of resolvents.
	      ]

  SeeAlso     [ ]

******************************************************************************/
int
sat_strengthen_clause(
	satManager_t *m, 
	satClause_t *c,
	long index)
{
long i, csize, flags, lit, assigns;
satClause_t *ante;
satHeap_t *h;

  m->nEliminatedLits++; 
 
  /** Move the deleted clause to backup space, after
   *  duplicating it, and the deleted clause is stored
   *  as dependent clause to make resolution graph. 
   **/
  ante = 0;
  lit = c->lits[index];

  /** Maintain the order of the literals out of the 
   *  pivot variable, and recalculating the abstraction 
   *  of clause.
   **/
  csize = SATSizeClause(c) - 1;
  for (i=index; i<csize; i++) {
    c->lits[i] = c->lits[i+1];
  }
  
  /** Recompute clause size and flags **/
  flags = c->size & SATCMask;
  c->size = (csize << SATCsizeShift) | flags;

  h = m->varElimHeap;
  if (h->indices[lit>>1] >= 0) {
    m->scores[lit]--;
    vel_heap_up(m, h->indices[lit>>1]);
  } 

  /** Once the clause becomes unit 
   *  propagate at level zero. 
   **/
  if (csize == 1) {
    c->size |= SATCVisited;
    assigns = m->stackPos;
    sat_enqueue_check(m, c->lits[0], ante);
    return (m->stackPos - assigns ? 0 : 1);
  }

  if (!m->eliminateVar) {
    sat_queue_insert(m->satQueue, (long)c);
  }
  /** correct abstract value changed by 
   *  a literal removed 
   **/
  sat_calculate_clause_abs(c);

  return 1;
}

/**Function********************************************************************

  Synopsis    [ Gather touched clauses for backward subsumption ] 

  Description [ Gather touched clauses for backward subsumption ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void sat_gather_touched_clauses(satManager_t *m)
{
long i, j, nVars, lit;
satClause_t *c;
satQueue_t *queue;
satArray_t *pos, *neg;

  queue = m->satQueue;
  nVars = m->nVars;
  for (i=1; i<=nVars; i++) {
    if (m->marks[i] == 1) {
      lit = i << 1;
      /** get positive and 
       *  negative occurrences **/
      pos = m->wls[lit|1];
      neg = m->wls[lit];
      
      if (pos) {
        for (j=0; j<pos->size; j++) {
          c = (satClause_t*)pos->space[j];
          if (!SATClauseIrredundant(c) && !SATClauseVisited(c)) {
            sat_queue_insert(m->satQueue, (long)c);
            c->size |= SATCIrredundant;
	  }
        }
      }	
      if (neg) {
        for (j=0; j<neg->size; j++) {
          c = (satClause_t*)neg->space[j];
          if (!SATClauseIrredundant(c) && !SATClauseVisited(c)) {
            sat_queue_insert(queue, (long)c);
            c->size |= SATCIrredundant;
	  }
        }
      }
      m->marks[i] = 0; 
    }
  }

  for (i=queue->first; i != queue->last; ) {
    c = (satClause_t*)queue->elems[i++];
    i = i%(queue->max);
    c->size -= SATCIrredundant; 
  }
}


/**Function********************************************************************

  Synopsis    [ Check implications with all enqueued literals. ] 

  Description [ Check implications with all enqueued literals on ALL-watched
                literal clauses. 
	      ]

  SideEffects [ Preconditions : All clauses are sorted. 
                Postconditions: All clauses are sorted. And no satisfied clause
		                is left. ]

  SeeAlso     [ ]

******************************************************************************/
satClause_t *
sat_implication_on_all_watched_literals(satManager_t *m)
{
#ifdef DEBUG
long unit;
#endif

int nProps, nonUnit;
long i, index, lit;
satClause_t *conflicting, *c;
satArray_t *wl;

  nProps = 0;
  conflicting = 0;

  while (m->curPos < m->stackPos) {
    lit = m->decisionStack[m->curPos++];
   
    /** Set the satisfied occurrencies to be removed **/
    wl = m->wls[lit^1]; 
    if (wl == 0) continue;  
    
    for (i = 0; i < wl->size; i++) {
      c = (satClause_t*)wl->space[i];
      sat_set_clause_deleted(m, c); 
    }
    /** Propage the assignment over the other occurrences **/
    wl = m->wls[lit];
    if (wl == 0) continue;  
   
    for (i = 0; i < wl->size; i++) {
      nonUnit = 1;

      c = (satClause_t*)wl->space[i];
      if (c && SATClauseVisited(c))	continue;

#ifdef DEBUG      
      unit = sat_check_unit_clause(m, c);
#endif
      
      /** strengthen clause with lit **/ 
      index = sat_get_literal_index_of_clause(m, c, lit^1); 
      if (index < 0) 
        fprintf(stderr, "ERROR : cannot find strenthened literal \n");
      nonUnit = sat_strengthen_clause(m, c, index);

#ifdef DEBUG
      if (nonUnit == 0 && (unit != m->decisionStack[m->stackPos-1]))
        fprintf(stdout, "ERROR : check all-watched implication (lit %ld -- %ld)\n", unit, m->decisionStack[m->stackPos-1]); 
#endif

      if (!nonUnit && m->status == 2)
        nProps++; 
      if (!nonUnit && m->status == 0) {
        conflicting = c;
	goto foundConflict;
      }
    }
  }
foundConflict:;
  m->nImplications += nProps;
  return (conflicting);
}

/**Function********************************************************************

  Synopsis    [ Clean the all-watched lists of clause ] 

  Description [ Clean the all-watched lists of clause ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_clean_all_watched_lists_of_clause(
	satManager_t *m,
        satClause_t *c)
{
long i, csize, lit;

  csize = SATSizeClause(c);
  for (i=0; i<csize; i++) {
    lit = c->lits[i];
    sat_clean_all_watched_list_of_literal(m, lit);
  }
}

/**Function********************************************************************

  Synopsis    [ Clean the all-watched list of literal ] 

  Description [ Clean the all-watched list of literal ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void 
sat_clean_all_watched_list_of_literal(
	satManager_t *m,
	long lit)
{
long i;
satArray_t *arr;
satClause_t *c;

  arr = m->wls[lit^1];
  if (arr)
    for(i=0; i<arr->size; i++) {
      c = (satClause_t*)arr->space[i];
      if (SATClauseVisited(c)) {
        arr->size--;
        arr->space[i--] = arr->space[arr->size];
      }
    }
}


/**Function********************************************************************

  Synopsis    [ Clean the all-watched list of variable ] 

  Description [ Clean the all-watched list of variable ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void 
sat_clean_all_watched_list_of_variable(
	satManager_t *m,
	long v)
{

  sat_clean_all_watched_list_of_literal(m, v<<1);
  sat_clean_all_watched_list_of_literal(m, (v<<1)|1);
}

/**Function********************************************************************

  Synopsis    [ Delete the clause in the watched list ] 

  Description [ Delete the clause in the watched list ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
int
sat_delete_clause_from_watched_list(
	satManager_t *m, 
	satClause_t *c, 
	long wlindex,
	long cindex)
{
long i;
satClause_t *ct;
satArray_t *arr;

  arr = m->wls[wlindex];

  if (arr->size == 0) 	return 0;
  
  /** If index of the clause in watched list
   *  is not valid, manually find it. 
   **/
  i = 0;
  while (cindex < 0) {
    if (i && i >= arr->size) {
      fprintf(stdout, "ERROR : Cannot find clause in watched list!\n");
      fprintf(stdout, "(");
      sat_print_clause_simple(m, c);
      fprintf(stdout, ") : watched list of %c%ld\n", wlindex & 1 ? ' ':'-', wlindex>>1);
      return 0;
    }

    ct = (satClause_t*)arr->space[i++];
    if (ct == c) 
      cindex = i-1;       
  }

  arr->space[cindex] = arr->space[--arr->size];
  return 1;
}

/**Function********************************************************************

  Synopsis    [ Delete the redundant clause out of resolvent literal pool ] 

  Description [ Delete the redundant clause out of resolvent literal pool ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
long
sat_delete_redundant_resolvents(satManager_t *m, satClause_t *cp)
{
char *marks;
long i, j, size, cpsize, cqsize;
long lit, lit1, lit2, count, redundant;
satArray_t *resolvents; 
 
  /* mark the literals of 
   * the cluase subsuming 
   */
  marks = m->litMarks;
  cpsize = SATSizeClause(cp);
  for (i=0; i<cpsize; i++) {
    lit = cp->lits[i]; 
    marks[lit] = 1;
  }

  redundant = 0;
  resolvents = m->redundant;
  size = resolvents->size;
  for (i=0; i<size; ) {
    lit1 = resolvents->space[i];
    cqsize = -lit1;
    if (cqsize > cpsize) {
      lit2 = resolvents->space[i+1];
      
      /* resolvent is not valid if lit2 is 0. */
      if (lit2 != 0) {
        count = 0;
        j = i + 1;
        do {
          lit2 = resolvents->space[j++];
          if (marks[lit2])  count++;
        } while (j <= i+cqsize);

        /* set redundant clause as invalid */
        if (count == cpsize) {
          resolvents->space[i+1] = 0;  
          redundant++;
        }   
      }
    }
    i += (m->coreGeneration ? (cqsize+3) : (cqsize + 1)); 
  }

  /* unmark the literals of 
   * the cluase subsuming 
   */
  for (i=0; i<cpsize; i++) {
    lit = cp->lits[i]; 
    marks[lit] = 0;
  }

  return redundant; 
}

/**Function********************************************************************

  Synopsis    [ Remove the resolvents created depending on the clause given ] 

  Description [ Remove the resolvents created depending on the clause given ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_remove_dependent_resolvents(satManager_t *m, satClause_t *c)
{
long i, size;
satArray_t *dependents;
satClause_t *dpc;

  dependents = c->dependent;
  if (!dependents)	return;

  size = dependents->size;
  for (i=0; i<size; i++) {
    dpc= (satClause_t*)(dependents->space[i]);

    if (dpc) {
      if (!SATClauseVisited(dpc)) {
        m->nResolvents--;
        m->nResolventLits -= SATSizeClause(dpc);
        dpc->size |= SATCVisited;
      }
    }
  }
  dependents->size = 0;
}

/**Function********************************************************************

  Synopsis    [ Add resolvent clause ] 

  Description [ Add resolvent clause ]

  SideEffects [ Adding watched literals is put off after the end of 
		variable elimination. ]

  SeeAlso     [ ]

******************************************************************************/
satClause_t *
sat_add_resolvent_clause(satManager_t *m, satArray_t *resolvent, long learned)
{
satClause_t *c;

  c = sat_new_clause(resolvent, learned); /* original clause */
  m->resolvents = sat_array_insert(m->resolvents, (long)c);
  m->nResolventLits += SATSizeClause(c);
  m->nResolvents++;
  return(c);
}

/**Function********************************************************************

  Synopsis    [ Add the resolvents from the literal pool ] 

  Description [ Add the resolvents from the literal pool 
              
	        Precondition : All the literals of each resolvent are sorted. ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_add_resolvents_from_lit_pool(satManager_t *m, satArray_t *pool)
{
long i, j, k, size, csize;
long lit1, lit2, index;
long abstract;
satArray_t *arr;
satClause_t *c;
satHeap_t *h;

  h = m->varElimHeap;
  size = pool->size;
  for (i=0; i+1<size; ) {
    lit1 = pool->space[i];
    lit2 = pool->space[i+1];
    csize = -lit1;
     
    if (lit2 > 0) {
      /* create a new clause from the pool */
      c = (satClause_t *)malloc(sizeof(satClause_t) + (sizeof(long)*csize));
      c->size = csize << SATCsizeShift;

      /* add the literals into the new clause */
      j = i + 1;
      k = 0;
      c->info.activity = 0;
      abstract = 0;
      while (k < csize) {
        lit2 = pool->space[j++];
	assert(lit2 != 0);
	c->lits[k++] = lit2;

	index = lit2^1;
        arr = m->wls[index];
	m->wls[index] = sat_array_alloc_insert(arr, (long)c);
	abstract |= 1 << (SATVar(lit2) & 31);
         	
	/* update variable scores and then heap down the variable */
	if (h->indices[lit2>>1] >= 0) {
          if (!m->eliminateVar) 
	    m->marks[lit2>>1] = 1; 
	  m->scores[lit2]++;
          vel_heap_down(m, h->indices[lit2>>1]);
	}  
      } 
      c->info.abstract = abstract;
      c->dependent = 0;
      if (m->coreGeneration) {
        sat_make_resolution_graph((satClause_t*)pool->space[j++], c);
        sat_make_resolution_graph((satClause_t*)pool->space[j], c);
#ifdef DEBUG
        sat_check_resolvent_dependencies(m, (satClause_t*)pool->space[j-1], (satClause_t*)pool->space[j], c);
#endif
      }
      m->clauses = sat_array_insert(m->clauses, (long)c);
      if (!m->eliminateVar) {
        sat_queue_insert(m->satQueue, (long)c);
      }
      m->nResolventLits += csize;
      m->nResolvents++;
    }
    i += (m->coreGeneration ? (csize + 3) : (csize + 1));
  }
  pool->size = 0;
}

/**Function********************************************************************

  Synopsis    [ Add all literals as watched ] 

  Description [ Add all literals as watched ]

  SideEffects [ The array of indices of upper part for all variables: m->up.
                Watched lists must be reconstructed for two watched literal
		schemed being used in SAT solver. ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_add_all_watched_literal(satManager_t *m, satClause_t *c)
{
long index, i, csize;
satArray_t *arr;

  csize = SATSizeClause(c);
  m->scores[c->lits[0]]++;
  if (csize > 1)
    m->scores[c->lits[1]]++;
    
  for (i=2; i<csize; i++) {
    /** This list is used as occur list. 
     *  Don't use as two watched literal list.
     **/
    m->scores[c->lits[i]]++;
    index = (c->lits[i])^1;
    arr = m->wls[index];
    m->wls[index] = sat_array_alloc_insert(arr, (long)c);
  }
}

/**Function********************************************************************

  Synopsis    [ Add all literals as watched with no scoring ] 

  Description [ Add all literals as watched with no scoring ]

  SideEffects [ Only watched literals are updated ]

  SeeAlso     [ sat_add_all_watched_literal ]

******************************************************************************/
void
sat_add_all_watched_literal_without_scoring(satManager_t *m, satClause_t *c)
{
long index, i, csize;
satArray_t *arr;

  csize = SATSizeClause(c);
  for (i=2; i<csize; i++) {
    /** This list is used as occur list. 
     *  Don't use as two watched literal list.
     **/
    index = (c->lits[i])^1;
    arr = m->wls[index];
    m->wls[index] = sat_array_alloc_insert(arr, (long)c);
  }
}

/**Function********************************************************************

  Synopsis    [ Extend model with respect to the eliminated variables ] 

  Description [ Extend model with respect to the eliminated variables ]

  SideEffects [ Precondition : 
 
                1. All the survided variable are assigned.
                2. All watched lists of eliminated variables must point 
		   to the list of their clauses deleted by variable 
		   elimination procedure. 
		]

  SeeAlso     [ ]

******************************************************************************/
void
sat_extend_model(satManager_t *m)
{
long i, index;
long v, lit;
int dontCares;
satArray_t *elimVars, *deleted;

  /** Get eliminated variables **/
  elimVars = m->elimtable;  
 
  /** Find values of eliminated variables
   *  in the reverse order of elimination
   **/
  dontCares = 0;
  for (i = elimVars->size - 1; i >= 0; i--) {
    v = elimVars->space[i];
    lit = v << 1;

    /** 1. Scan posivive occurrence clauses **/
    index = lit | 1;
    deleted = m->wls[index];
    if (deleted)
      sat_find_value_of_eliminated_var_on_clauses(m, deleted, v);
    
    /** 2. Scan negative occurrence clauses **/
    index = lit;
    deleted = m->wls[index];
    if (deleted)
       sat_find_value_of_eliminated_var_on_clauses(m, deleted, v);
    
    if (m->values[v] >= 2) {
      /* don't care variable is found */
      m->values[v] = 1;  
      dontCares++;
    }  
  }
}

/**Function********************************************************************

  Synopsis    [ Find a value of an eliminated variable ] 

  Description [ Find a value of an eliminated variable ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_find_value_of_eliminated_var_on_clauses(satManager_t *m, satArray_t *clauses, long v)
{
long i, j, csize;
long otherV, otherLit;
int sign;
satClause_t *c;
#ifdef DEBUG
int error = 1;
#endif

  sign = 0;
  for (i = 0; i < clauses->size; i++) {
    c = (satClause_t*)clauses->space[i];
    csize = SATSizeClause(c);
    for (j = 0; j < csize; j++) { 
      otherLit = c->lits[j];
      otherV = SATVar(otherLit);
      if (otherV == v) {
        sign = otherLit & 1;

#ifdef DEBUG
        error = 0;  
#endif
      }
      else if ((m->values[otherV]^(otherLit&1)) != 0) {
        /* skip clause satisfied by other literal */
        goto nextClause;
      } 
    }
#ifdef DEBUG
    if (error) {
      fprintf(stdout, "ERROR : Invalid extension of eliminated Var %ld!\n", v);
      fprintf(stdout, "Check CL (");
      sat_print_clause_simple(m, c);
      fprintf(stdout, ") wrt %ld \n", v);
      break;
    }
#endif
    if (sign == 1) m->values[v] = 0;
    else m->values[v] = 1;
    /* m->values[v] = (sign==1 ? 0 : 1); HK*/
    break;

nextClause:;
  }
}

/**Function********************************************************************

  Synopsis    [ Check duplicates in clauses array ] 

  Description [ Check duplicates in clauses array ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_check_duplications_in_clauses(satArray_t *clauses)
{
long i, j, nDuplicates;
satClause_t *cp, *cq;

  nDuplicates = 0;

  for (i = 0; i < clauses->size; i++) {
    cp = (satClause_t*)clauses->space[i];
    cp->info.activity = 0;
  }
    
  for (i = 0; i < clauses->size; i++) {
    cp = (satClause_t*)clauses->space[i];
    for (j = i+1; j < clauses->size; j++) {
      cq = (satClause_t*)clauses->space[j];
      if (sat_check_clauses_duplicate(cp, cq)) { 
        cp->info.activity++;
        cq->info.activity++;
        nDuplicates++; 
      }
    }
  }
  fprintf(stdout, "******************************************\n");
  fprintf(stdout, " %ld Duplicates out of %ld clauses \n", nDuplicates, clauses->size);
  fprintf(stdout, "******************************************\n");

  for (i = 0; i < clauses->size; i++) {
    cp = (satClause_t*)clauses->space[i];
    fprintf(stdout, "Clause %ld : %ld duplicates\n", i, (long)cp->info.activity);
  }
}

/**Function********************************************************************

  Synopsis    [ Check duplicate clauses ] 

  Description [ Check duplicate clauses ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
int
sat_check_clauses_duplicate(satClause_t *cp, satClause_t *cq)
{
long i, j, cpsize, cqsize;
long lit;
int duplicate;

  cpsize = SATSizeClause(cp);
  cqsize = SATSizeClause(cq);

  if (cpsize != cqsize)  return 0;

  for (i = 0; i < cpsize; i++) {
    lit = cp->lits[i];
    duplicate = 0;
    for (j = 0; j < cqsize; j++) {
      if (cq->lits[j] == lit) {
        duplicate = 1;
        break;
      }
    }
    if (duplicate == 0)
      return 0;
  }
  return 1;
}


/******************************************************************************
 * 
 * Utilities
 *
*******************************************************************************/
void 
sat_report_result_for_var_elim(satManager_t *m) 
{
  if (m== 0) return;
 
  fprintf(stdout, "============[ Varelim Statistics ]============\n");
  fprintf(stdout, "Eliminated variables : %ld out of %ld\n", m->nEliminatedVars, m->nVars); 
  fprintf(stdout, "Eliminated clauses   : %ld out of %ld\n", m->nEliminatedCls, m->nClauses); 
  fprintf(stdout, "Eliminated literals  : %ld out of %ld\n", m->nEliminatedLits, m->nLits); 
  fprintf(stdout, "Resolvent clauses    : %ld\n", m->nResolvents);
  fprintf(stdout, "Resolvent literals   : %ld\n", m->nResolventLits);
  fprintf(stdout, "Selfsubsumption      : backward(%ld), resolution(%ld)\n", m->nBackwardSelfsubsume, m->nSelfsubsume);
  fprintf(stdout, "Elimination checks   : %ld with %ld iterations\n", m->nVarElimTry, m->nSubsumeTry-1); 
  if(m->status == 0) fprintf(stdout, "UNSATISFIABLE at level 0\n");
  else if (m->status == 1) fprintf(stdout, "SATISFIABLE at level 0\n");
  
  fprintf(stdout, "Eliminate time : %10g \n", m->elimTime);
  fprintf(stdout, "\n");
}

/**Function********************************************************************

  Synopsis    [ Heap ] 

  Description [ Heap ] 

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
static int
vel_compare_scores(satManager_t *m, long x, long y)
{
long xindex, yindex;
long xscore, yscore;

  xindex = x << 1;
  xscore = m->scores[xindex] * (m->scores[xindex|1]);
  xscore -= (m->scores[xindex] + m->scores[xindex|1]);

  yindex = y << 1;
  yscore = m->scores[yindex] * (m->scores[yindex|1]);
  yscore -= (m->scores[yindex] + m->scores[yindex|1]);
   
  return(xscore < yscore);
}

void
vel_heap_remove_var_eliminated(satManager_t *m)
{
long i, j;
satHeap_t *h;
 
  h = m->varElimHeap;
  for(i=j=0; i<h->size; i++) {
    if(m->levels[h->heap[i]]) {
      h->heap[j] = h->heap[i];
      h->indices[h->heap[i]] = j++;
    }
    else {
      h->indices[h->heap[i]] = -1;
    }
  }
  h->size -= (i-j);

  for(i=h->size/2-1; i>=0; i--) 
    vel_heap_down(m, i);
}

void 
vel_heap_up(satManager_t *m, long i)
{
satHeap_t *h;
long *heap;
long x;

  h = m->varElimHeap;
  heap = h->heap;
  x = heap[i];
  while(i!=0 && vel_compare_scores(m, x, heap[heap_parent(i)])) {
    heap[i] = heap[heap_parent(i)];
    h->indices[heap[i]] = i;
    i = heap_parent(i);
  }
  h->heap[i] = x;
  h->indices[x] = i;
}

void
vel_heap_down(satManager_t *m, long i)
{
satHeap_t *h;
long *heap;
long x, c;

  h = m->varElimHeap;
  heap = h->heap;
  x = heap[i];
  while(heap_left(i) < h->size) {
    c = (heap_right(i) < h->size && 
	vel_compare_scores(m, heap[heap_right(i)], heap[heap_left(i)])) ?
	heap_right(i) : heap_left(i);
    if(!vel_compare_scores(m, heap[c], x))	break;
    heap[i] = heap[c];
    h->indices[heap[i]] = i;
    i = c;
  }
  heap[i] = x;
  h->indices[x] = i;
}

long
vel_heap_remove_min(satManager_t *m)
{
long x;
satHeap_t *h;
 
  h = m->varElimHeap;
  x = h->heap[0];
  h->heap[0] = h->heap[h->size-1];
  h->indices[h->heap[0]] = 0;
  h->indices[x] = -1;
  h->size--;
  if(h->size > 1)	
    vel_heap_down(m, 0);

  return(x);
}

void
vel_heap_clear(satManager_t *m)
{
satHeap_t *h;
long i;
 
  h = m->varElimHeap;
  for(i=0; i<h->size; i++)
    h->indices[h->heap[i]] = -1;
  h->size = 0;
}

void
vel_heap_update(satManager_t *m, long n)
{
satHeap_t *h;
 
  h = m->varElimHeap;
  if(h->indices[n] < 0)
    vel_heap_insert(m, n);
  else {
    vel_heap_up(m, h->indices[n]);
    vel_heap_down(m, h->indices[n]);
  }
}

void
vel_heap_init(satManager_t *m, long size)
{
satHeap_t *h;
long i;
  

  h = (satHeap_t *)malloc(sizeof(satHeap_t));
  h->size = 0;

  size++;
  h->heap = (long *)malloc(sizeof(long)*size);
  h->indices = (long *)malloc(sizeof(long)*size);
  for(i=0; i<size; i++) h->indices[i] = -1;

  m->varElimHeap = h;
}

void
vel_heap_print(satManager_t *m)
{
satHeap_t *h;
int i;

  h = m->varElimHeap;
  for(i=0; i<=h->size; i++) {
    fprintf(stdout, "%d ", i);
    fprintf(stdout, "%ld ", h->heap[i]);
    fprintf(stdout, "\n");
  }
}

void
vel_heap_free(satManager_t *m)
{
satHeap_t *h;

  h = m->varElimHeap;
  if(h) {
    free(h->heap);
    free(h->indices);
    free(h);
    m->varElimHeap = 0;
  }
}

int
vel_heap_check(satManager_t *m, long i)
{
satHeap_t *h;

  h = m->varElimHeap;
  if(i >= h->size) return(1);

  if(i==0 || !vel_compare_scores(m, h->heap[i], h->heap[heap_parent(i)])) {
    return(vel_heap_check(m, heap_left(i)) && vel_heap_check(m, heap_right(i)));
  }
  return(0);
      
}

int
vel_heap_inHeap(satManager_t *m, long n)
{
satHeap_t *h;
  
  h = m->varElimHeap;
  return (h->indices[n] >= 0); 
}

void
vel_heap_insert(satManager_t *m, long n)
{
satHeap_t *h;

  h = m->varElimHeap;
  h->indices[n] = h->size;
  h->heap[h->size++] = n;
  vel_heap_up(m, h->indices[n]);
}

long
sat_get_num_assignments_of_a_level(satManager_t *m, long level) 
{
satArray_t *seperator;
long bi, ei;

  seperator = m->decisionStackSeperator;
  if (seperator->size < level) {
    fprintf(stdout, "ERROR : level %d has been assigned\n", (int)level);
    return (-1);
  }

  if (level == 0) bi = 0;
  else 		  bi = seperator->space[level-1];
  ei = (seperator->size == level) ? m->stackPos : seperator->space[level];

  return (ei - bi);
}

void 
sat_clean_resolvents_DB(satManager_t *m, long v, long begin)
{
long i, j, size, index;
satClause_t *c, *oc;
satArray_t *resolvents, *occurr;

  /** Remove associated dependent list **/
  index = v << 1;
  occurr = m->wls[index];
  if (occurr)
    for (i=0; i<occurr->size; i++) {
      oc = (satClause_t*)occurr->space[i];
      if (oc->dependent)
        oc->dependent->size = 0;
    }

  index += 1;
  occurr = m->wls[index];
  if (occurr)
    for (i=0; i<occurr->size; i++) {
      oc = (satClause_t*)occurr->space[i];
      if (oc->dependent)
        oc->dependent->size = 0;
    }

  resolvents = m->resolvents;
  for (i=j=begin; i<resolvents->size; i++) {
    c = (satClause_t*)resolvents->space[i];
    if (SATClauseVisited(c)) {
      if (c->dependent)
        free(c->dependent);
      free(c);
      m->nResolventLits -= SATSizeClause(c);
    }
    else {
      fprintf(stdout, "clause : address %p \n", c); 
      m->wls[c->lits[0]^1] = sat_array_alloc_insert(m->wls[c->lits[0]^1], (long)c);
      m->wls[c->lits[1]^1] = sat_array_alloc_insert(m->wls[c->lits[1]^1], (long)c);
      
      sat_add_all_watched_literal(m,c);
      
      resolvents->space[j++] = resolvents->space[i++];
      size = SATSizeClause(c);
      m->nCurClauseLits -= size;
      m->nTotalClauseLits -= size;
    }  
  }
  resolvents->size -= (i-j);
  m->nResolvents = resolvents->size;
}

void 
sat_delete_current_resolvents_DB(satManager_t *m, long v, long begin)
{
long i, j;
long *space, index;
satClause_t *c, *oc;
satArray_t *resolvents, *occurr;

  /** Remove associated dependent list **/
  index = v << 1;
  occurr = m->wls[index];
  for (i=0; i<occurr->size; i++) {
    oc = (satClause_t*)occurr->space[i];
    if (oc->dependent) {
      oc->dependent->size = 0;
    }
  }
  index ^= 1;
  occurr = m->wls[index];
  for (i=0; i<occurr->size; i++) {
    oc = (satClause_t*)occurr->space[i];
    if (oc->dependent) {
      oc->dependent->size = 0;
    }
  }

  resolvents = m->resolvents;
  space = resolvents->space;
  for (i=begin, j=resolvents->size; i<j; i++) {
    c = (satClause_t*)space[i];
    if (c) {
      if (c->dependent)
        free(c->dependent);
      m->nResolventLits -= SATSizeClause(c);
      free(c);
      space[i--] = space[--j];
    }
  }
  resolvents->size = j;
  m->nResolvents = j; 
}


/**Function********************************************************************

  Synopsis    [ Remove marked clauses in preprocessing ] 

  Description [ Remove marked clauses in preprocessing
                 
		Precondition : no literal in CNF DB is watched. All the watched
		               literals will be added after this procedure. ]

  SideEffects [ No clause is freed, but the clauses are moved to a backup 
                data base out of the original cnf clauses. ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_remove_marked_clauses(satManager_t *m, satArray_t *arr)
{
int learned;
long i, j, csize;
satClause_t *c;

  learned = (arr == m->learned) ? 1 : 0;

  for (i=j=0 ; i< arr->size; i++) {
    c = (satClause_t*)arr->space[i];
    csize = SATSizeClause(c);
    if (csize == 1) {
      arr->space[j++] = arr->space[i];
      continue;
    }
    
    if (SATClauseVisited(c)) {
#ifdef VERIFY_ON
      m->deleted = sat_array_insert(m->deleted, (long)c);
#else
      if (c->dependent)
        free(c->dependent);
      free(c); 
#endif
    }
    else {
      if (learned && !SATClauseLearned(c)) 
        m->clauses = sat_array_insert(m->clauses, (long)c);
      else 
        arr->space[j++] = arr->space[i];
    }
  }
  arr->size -= (i-j);
}

void
sat_mark_clauses_of_var_deleted(satManager_t *m, long v)
{
long lit;
  
  lit = v << 1;
  sat_mark_occur_list_to_be_deleted(m, lit);
  lit |= 1;
  sat_mark_occur_list_to_be_deleted(m, lit);
}

void
sat_mark_occur_list_to_be_deleted(satManager_t *m, long index)
{
long i, j, csize, lit, nCls, nLits;
satArray_t *occur;
satClause_t *c;
satHeap_t *h;

  h = m->varElimHeap;

  nCls = nLits = 0;
  /* take the occur list */
  occur = m->wls[index];
  if (occur) {
    for (i=0; i<occur->size; i++) {
      c = (satClause_t*) occur->space[i];
      if (c && !(SATClauseVisited(c))) {
        c->size |= SATCVisited; 
	csize = SATSizeClause(c);
	/* update variable heap */
	for (j=0; j<csize; j++) {
	  lit = c->lits[j]; 
	  if (index != lit && h->indices[lit>>1] >= 0) {
	    m->scores[lit]--;
	    vel_heap_update(m, lit>>1); 
	  }
	}
        nLits += csize;
        nCls++;
      }
    }
  }
  m->nEliminatedLits += nLits;
  m->nEliminatedCls += nCls;
}

void sat_reset_all_watched_lists(satManager_t *m)
{
long i, index, lit;
satArray_t *pwl, *nwl;

  for (i=1; i<=m->nVars; i++) {
    lit = i << 1;
    index = lit;
    pwl = m->wls[index|1];
    nwl = m->wls[index];
    
    if (m->values[i] <= 2) { 
      m->scores[index] = 0;
      if (pwl)   pwl->size = 0;

      m->scores[index|1] = 0;
      if (nwl)  nwl->size = 0;
      
      if (m->values[i] == 2)
        m->pure[i] = 0;
    }
  }  
  m->nCurClauseLits = 0;
  m->nTotalClauseLits = 0;
  m->nCurLearnedLits = 0;
  m->nCurLearnedClauses = 0;
}

int
sat_squeeze_clause(satManager_t *m, satClause_t *c)
{
long i, j, size;
long v, lit, flags;

  size = SATSizeClause(c);
  for (i=j=0; i<size; i++) {
    lit = c->lits[i];
    v = SATVar(lit);
    if (m->values[v] == 2)
      c->lits[j++] = c->lits[i];
    else if ((m->values[v] ^ (lit&1)) == 1 ) { 
      c->size |= SATCVisited;
      return 0;
    }
  }
  flags = c->size & SATCMask;
  size -= (i-j);
  c->size = (size << SATCsizeShift) | flags;

  return 1;
}

void sat_recover_clauses_DB(satManager_t *m)
{
long i, lit, *space;
satArray_t *clauses;
satClause_t *c;

  clauses = m->clauses;
  space = clauses->space;
  for (i=0; i<clauses->size; i++) {
    c = (satClause_t*)space[i]; 

    if (SATClauseVisited(c))
      continue;

    if(SATSizeClause(c) == 1) {
      lit = c->lits[0];
      sat_enqueue_check(m, lit, c); 
    }
    else { 
      if (c) {
        if (sat_squeeze_clause(m, c)) {
          sat_mark_for_pure_lits(m, c);
          sat_add_watched_literal(m, c);
	}
      }
    } 
  }

  clauses = m->learned;
  space = clauses->space;
  if (m->periodicDistill)
    m->n2LitClauses = 0;

  for (i=0; i<clauses->size; i++) {
    c = (satClause_t*)space[i]; 

    if (SATClauseVisited(c))
      continue;

    if(SATSizeClause(c) == 1) {
      lit = c->lits[0];
      sat_enqueue_check(m, lit, c); 
    }
    else { 
      if (c) {
        if (sat_squeeze_clause(m, c))
          sat_add_watched_literal(m, c);
	if (m->periodicDistill && SATSizeClause(c) == 2)
	  m->n2LitClauses++;
      }
    } 
  }
}

void 
sat_init_clauses_statistics(satManager_t *m)
{
int i;

  for (i = 0; i < 13; i++) {
    m->clausesHistogram[i] = 0;
  }
  m->majorityClauseLength = 0;
}

void
sat_update_clauses_statistics(satManager_t *m, satClause_t *c)
{
int index;
long csize;
  
  csize = SATSizeClause(c);
  index = (csize >= 12) ? 12 : csize;
  m->clausesHistogram[index]++;    

  if (m->clausesHistogram[index] > m->clausesHistogram[m->majorityClauseLength]) {
    m->minorityClauseLength = m->majorityClauseLength;
    m->majorityClauseLength = index;
  }
}

long
sat_check_clauses_high_density(satManager_t *m)
{
long index1, index2;
satArray_t *clauses;

  clauses = m->clauses;

  index1 = m->majorityClauseLength;
  index2 = m->minorityClauseLength;
  if ((double)m->clausesHistogram[index1]/clauses->size >= 0.95) 
    return (1);
  
  if ((double)m->clausesHistogram[index2]/clauses->size >= 0.95)
    return (1);

  return 0;
}

void 
sat_print_clauses_histogram(satManager_t *m)
{
int i;

  fprintf(stdout, "**********************************\n");
  fprintf(stdout, "* Histogram of clause lengths    *\n");
  fprintf(stdout, "**********************************\n");
  for (i = 0; i < 11; i++) {
    fprintf(stdout, " Num of claues [%d] : %ld\n", i, m->clausesHistogram[i]);
  }
  fprintf(stdout, " Num of claues [ >=%d ] : %ld\n", i, m->clausesHistogram[i]);
  fprintf(stdout, " Length %d is majority clause length.\n", (int)m->majorityClauseLength);
  fprintf(stdout, "**********************************\n");
}

/******************************************************************************
 * 
 * Functions for Debugging 
 *
 ******************************************************************************/

/**Function********************************************************************

  Synopsis    [ Check the clause after merging and sorting ]

  Description [ Check the clause after merging and sorting 
                
		Invariant : for all literal lit_i in the clause, lit_i <= lit_j,
		            where j > i.

		Return 1 if no error found.
		Return 0 Otherwise.
              ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
int
sat_check_clause_after_merge_sort(satManager_t *m, satArray_t *arr, long begin)
{
long i, j, lit;

  for (i=begin+1; i<arr->size; i++) {
    lit = arr->space[i];
    for (j=i+1; j<arr->size; j++) {
      if (lit > arr->space[j]) {
        fprintf(stdout, "ERROR in checking the clause after merging and sorting!\n");
	fprintf(stdout, "Caused in ");
	sat_print_array_as_clause(m, arr);
        return 0;
      }
    }
  }
  return 1;
}

/**Function********************************************************************

  Synopsis    [ Print a part of clause array ]

  Description [ Print a part of clause array ] 
                
  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_print_clause_array_part(satManager_t *m, satArray_t *arr, long begin, long end) 
{
long i, lit, v;
  
  fprintf(stdout, "(");
  for(i=begin; i<end; i++) {
    lit = arr->space[i];
    v = lit>>1;
    fprintf(stdout, "%c%d:%c", 
	         lit&1 ? '-' : ' ',
		 (int)v,
		 m->values[v]==1 ? '1' : (m->values[v]==0 ? '0' : 'x'));
    fprintf(stdout, " ");
  }
  fprintf(stdout, ")");
  fflush(stdout);
}

/**Function********************************************************************

  Synopsis    [ Print current database into CNF file ]

  Description [ Print current database into CNF file ] 
                
  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_print_current_DB_to_cnf(satManager_t *m, char *cnfFilename)
{
FILE *fp;
long i, j, lit, v;
long csize;
satClause_t *c;
satArray_t *clauses;

  if (!(fp = fopen(cnfFilename, "w"))) {
    fprintf(stderr, "ERROR : Can't open CNF file %s\n", cnfFilename);
    return;
  }
  
  clauses = m->clauses;
  fprintf(fp, "p cnf %d %d\n", (int)m->nVars, (int)clauses->size);
  for (i = 0; i < clauses->size; i++) {
    c = (satClause_t*)clauses->space[i];
    csize = SATSizeClause(c);
    for (j = 0; j< csize; j++) {
      lit = c->lits[j];
      v = SATVar(lit);
      if ((m->values[v]^(lit&1)) == 1) continue;
    }

    for (j = 0; j < csize; j++) {
      lit = c->lits[j];
      v = SATVar(lit);
      fprintf(fp, "%d ", lit&1 ? (int) -v : (int) v); 
    }
    fprintf(fp, "0\n");
  }

  fclose(fp);
}

/**Function********************************************************************

  Synopsis    [ Check clauses are sorted ]

  Description [ Check clauses are sorted ] 
                
  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
int
sat_check_all_clauses_sorted(satManager_t *m) 
{
long i, j, csize, passed; 
satClause_t *c;
satArray_t *clauses;

  passed = 1;
  clauses = m->clauses;
  for (i = 0; i < clauses->size; i++) {
    c = (satClause_t*)clauses->space[i];
    csize = SATSizeClause(c);
    if (csize == 1) continue;

    for (j = 0; j < csize - 1; j++) {
      if (SATClauseIrredundant(c))
        fprintf(stdout, "ERROR : Clause marked\n");
      if ((c->lits[j] >>1) > (c->lits[j+1] >>1)) {
        fprintf(stdout, "ERROR : found unsorted clause (");
	sat_print_clause_simple(m, c);
	fprintf(stdout, ") on %dth of %dth original clause of size %d\n", (int)j, (int)i, (int)csize);
	passed = 0;
	break;
      }
    }
  }

  clauses = m->learned;
  for (i = 0; i < clauses->size; i++) {
    c = (satClause_t*)clauses->space[i];
    csize = SATSizeClause(c);
    if (csize == 1) continue;

    for (j = 0; j < csize - 1; j++) {
      if (SATClauseIrredundant(c))
        fprintf(stdout, "ERROR : Clause marked\n");
      if ((c->lits[j] >>1) > (c->lits[j+1] >>1)) {
        fprintf(stdout, "ERROR : found unsorted clause (");
	sat_print_clause_simple(m, c);
	fprintf(stdout, ") on %dth of %dth conflict clause of size %d\n", (int)j, (int)i, (int)csize);
        sat_sort_clause_literal(c);
	passed = 0;
      }
    }
  }

  return passed;
}

/**Function********************************************************************

  Synopsis    [ Check resolvent dependencies ]

  Description [ Check resolvent dependencies ] 
                
  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_check_resolvent_dependencies(satManager_t *m, satClause_t *cp, satClause_t *cq, satClause_t *c)
{
long i, j, cpsize, cqsize, csize;
int error;
char *marks;

  error = 0;
  marks = m->litMarks;
  cpsize = SATSizeClause(cp);
  csize = SATSizeClause(c); 
  for (i = 0; i < cpsize; i++) 
    for (j = 0; j < csize; j++) 
      if (cp->lits[i] == c->lits[j]) 
        marks[c->lits[j]] = 1;
     
  cqsize = SATSizeClause(cq);
  for (i = 0; i < cqsize; i++) 
    for (j = 0; j < csize; j++) 
      if (cq->lits[i] == c->lits[j])
        if (marks[c->lits[j]] == 0)
          marks[c->lits[j]] = 1;

  for (j = 0; j < csize; j++)
    if (marks[c->lits[j]] == 0)
      error = 1; 

  if (error) {
    fprintf(stdout, "ERROR : Wrong in resolution! \n");
    fprintf(stdout, "Resolvent (");
    sat_print_clause_simple(m, c);
    fprintf(stdout, " ) <= (");
    sat_print_clause_simple(m, cp);
    fprintf(stdout, ") (x) (");
    sat_print_clause_simple(m, cq);
    fprintf(stdout, ")\n");

  }
}

/**Function********************************************************************

  Synopsis    [ Check unit of a clause ]

  Description [ Check unit of a clause ] 
                
  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
long
sat_check_unit_clause(satManager_t *m, satClause_t *c) 
{
long i, csize, lit, unit;

  unit = 0;
  csize = SATSizeClause(c);
  for (i = 0; i < csize; i++) {
    lit = c->lits[i];
    if (m->values[lit>>1] == 2) 
      if (unit == 0)   unit = lit;
      else  return 0;
    else if ((m->values[lit>>1]^(lit&1) ) == 1) 
      return 0;
  }
  return unit;
}

/**Function********************************************************************

  Synopsis    [ Calculate the abstract score of the clause ]

  Description [ Calculate the abstract score of the clause ] 
                
  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_calculate_clause_abs(satClause_t *c)
{
long i, size, abstract;

  abstract = 0;
  size = SATSizeClause(c); 
  for (i=0; i<size; i++) 
    abstract |= 1 << (SATVar(c->lits[i]) & 31);
  c->info.abstract = abstract;
}

/**Function********************************************************************

  Synopsis    [ Copy a clause to another ]

  Description [ Copy a clause to another ] 
                
  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
satClause_t *
sat_copy_clause(satManager_t *m, satClause_t *c) 
{
int learned;
long i, size;
satArray_t *arr;
satClause_t *ct;

  arr = m->clearned;
  arr->size = 0;

  /** Create a duplicate clause **/
  size = SATSizeClause(c);
  for (i = 0; i < size; i++) {
    arr = sat_array_insert(arr, c->lits[i]);
  }
  learned = SATClauseLearned(c);
  ct = sat_add_clause(m, arr, learned); 
 
  if (m->simplify)
    sat_add_all_watched_literal_without_scoring(m, c);

  m->clearned = arr;
  m->clearned->size = 0;
  return (ct);
}

/**Function********************************************************************

  Synopsis    [ Make resolution graph ]

  Description [ Make resolution graph :
                  Store c as one of parents resolved to derive ct. ]

                
  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_make_resolution_graph(satClause_t *c, satClause_t *ct)
{
  ct->dependent = sat_array_alloc_insert(ct->dependent, (long)c);   
}

/**Function********************************************************************

  Synopsis    [ Delete dependencies of clauses ]

  Description [ Delete dependencies of clauses ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void 
sat_delete_dependencies_of_clause_array(satArray_t *arr) 
{
long i;
satClause_t *c;

  if (arr) {
    for (i = 0; i < arr->size; i++) {
      c = (satClause_t *)arr->space[i];
      if (c->dependent) { 
	c->dependent->size = 0;
      }
    }
  }
}

/**Function********************************************************************

  Synopsis    [ Check occurrence list of eliminated variables ] 

  Description [ Check occurrence list of eliminated variables ]

  SideEffects [ Invariant : no clauses in the list of deleted clauses is left
                            unwatched by any eliminated variable. ]

  SeeAlso     [ ]

******************************************************************************/
void 
sat_check_all_watched_list_of_eliminated_variables(satManager_t *m)
{
long i, j, index;
long v, lit, csize;
int satisfied;
satClause_t *c;
satArray_t *elimVars, *occur, *deleted;

  /** Get eliminated variables **/
  elimVars = m->elimtable;
  for (i = 0; i < elimVars->size; i++) {
    v = elimVars->space[i];
    lit = v << 1;
     
    /** 1. Mark clauses in positive occurrence list **/
    index = lit | 1;
    occur = m->wls[index];
    if (occur && occur->size == 0) 
      fprintf(stdout, "WARNING : Empty occur list of eliminated Var %ld\n", v); 
    else if (occur) { 
      for (j = 0; j < occur->size; j++) {
        c = (satClause_t*)occur->space[j];
        if (!SATClauseVisited(c))
          c->size |= SATCVisited;
      }
    }  
    /** 2. Mark clauses in negative occurrence list **/
    index = lit;
    occur = m->wls[index];
    if (occur && occur->size == 0) 
      fprintf(stdout, "WARNING : Empty occur list of eliminated Var %ld\n", v);
    else if (occur) {
      for (j = 0; j < occur->size; j++) {
        c = (satClause_t*)occur->space[j];
        if (!SATClauseVisited(c))
          c->size |= SATCVisited;
      } 
    }
  }

  /** Check if all clauses deleted are either watched or satisfied **/
  deleted = m->deleted;
  for (i = 0; i < deleted->size; i++) {
    c = (satClause_t*)deleted->space[i];
    csize = SATSizeClause(c);
    satisfied = 0;
    if (!SATClauseVisited(c)) {
      for (j = 0; j < csize; j++) {
        lit = c->lits[j];
	if ((m->values[SATVar(lit)] ^ (lit&1)) == 1) {
          satisfied = 1;
	  break;
	}
      }
      if (satisfied == 0) {
        fprintf(stdout, "ERROR : unsatisfied deleted clause\n"); 
	sat_print_clause(m, c);
	fprintf(stdout, "\n");
      }
    }
  }
}

/**Function********************************************************************

  Synopsis    [ Utilities for Queue structure ]

  Description [ Utilities for Queue structure ] 
                
  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
satQueue_t * 
sat_queue_init(long maxElements)
{
satQueue_t *Q;

  Q = (satQueue_t *)malloc(sizeof(satQueue_t) + sizeof(long)*maxElements);
  if( Q == NULL ) 
    fprintf(stderr, " Queue Out of space!\n");
  
  Q->max = maxElements;
  Q->size = 0;
  Q->first = 0;
  Q->last = 0;
  Q->elems[0] = 0;
  return Q;
}

void
sat_queue_clear(satQueue_t *Q) 
{
  Q->first = Q->last = 0;
}

void 
sat_queue_free(satQueue_t *Q)
{
  if (Q)
    free(Q);
}

void 
sat_queue_insert(satQueue_t *Q, long n)
{
long last, max;
  
  max = Q->max;
  last = Q->last + 1;
  if (last % max == Q->first) { 
    return;
  }
  Q->elems[Q->last] = n;
  Q->last = last % max;
  ++(Q->size);
}

long 
sat_queue_pop(satQueue_t *Q)
{
long n, first;

  first = Q->first;
  if (first == Q->last) { 
    fprintf(stderr, " Queue underflow!\n");
    return -1;
  }
 
  n = Q->elems[first];
  Q->first = ++first % Q->max;
  --(Q->size);
  return n;
}

void
sat_queue_print(satQueue_t *Q)
{
long i;

  fprintf(stdout, " Queue contents :  First(%ld) -> Last(%ld)\n", Q->first, Q->last);
  for (i=Q->first; i!=Q->last; ) {
    fprintf(stdout, " %6ld", Q->elems[i++]);
    i = i%(Q->max);
    if (i%15 == 0) {
      fprintf(stdout, "\n");
    }
  }
  fprintf(stdout, "\n");
}