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

  FileName    [satConflict.c]

  PackageName [sat]

  Synopsis    [Routines for sat conflict analysism and unsat proof generation
  for both CNF format and AIG format]

  Author      [HoonSang Jin,  Bing Li]

  Copyright [ This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]


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

#include "satInt.h"
#include "puresatInt.h"

static char rcsid[] UNUSED = "$Id: satConflict.c,v 1.31 2009/04/11 18:26:37 fabio Exp $";

static	satManager_t *SATcm;

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static int levelCompare( const void * node1, const void * node2);

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


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

  Synopsis    [ Conflict Analysis]

  Description [ Conflict Analysis]

  SideEffects []

  SeeAlso     []

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

int
sat_ConflictAnalysis(
	satManager_t *cm,
	satLevel_t *d)
{
satStatistics_t *stats;
satOption_t *option;
satArray_t *clauseArray;
int objectFlag;
int bLevel;
long fdaLit, conflicting;


  conflicting = d->conflict;

  if(d->level == 0) {
      /** Bing : UNSAT core generation */
    if(cm->option->coreGeneration)
      sat_ConflictAnalysisForCoreGen(cm, d);
    cm->currentDecision--;
    return (-1);
  }

  stats = cm->each;
  option = cm->option;


  stats->nBacktracks++;

  clauseArray = cm->auxArray;

  bLevel = 0;
  fdaLit = -1;
  clauseArray->num = 0;

  /*  Find Unique Implication Point */

  if(option->RT)
    sat_FindUIPWithRT(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
  else
    sat_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
  stats->nNonchonologicalBacktracks += (d->level - bLevel);


  if(clauseArray->num == 0) {
    sat_PrintImplicationGraph(cm, d);
    sat_PrintNode(cm, conflicting);
  }

  /* If we could find UIP then it is critical error...
  * at lease the decision node has to be detected as UIP.
  */
  if(fdaLit == -1) {
    fprintf(cm->stdOut, "%s ERROR : Illegal unit literal\n", cm->comment);
    fflush(cm->stdOut);
    sat_PrintNode(cm, conflicting);
    sat_PrintImplicationGraph(cm, d);
    sat_PrintDotForConflict(cm, d, conflicting, 0);
    exit(0);
  }

  if(bLevel && cm->lowestBacktrackLevel > bLevel)
    cm->lowestBacktrackLevel = bLevel;

  bLevel = sat_AddConflictClauseAndBacktrack(
	  cm, clauseArray, d, fdaLit, bLevel, objectFlag, 0);

  return(bLevel);
}

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

  Synopsis    [ Conflict Analysis for lifting instance]

  Description [ Conflict Analysis for lifting instance]

  SideEffects []

  SeeAlso     []

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

int
sat_ConflictAnalysisForLifting(
	satManager_t *cm,
	satLevel_t *d)
{
satStatistics_t *stats;
satOption_t *option;
satArray_t *clauseArray;
int objectFlag;
int bLevel;
long fdaLit, conflicting;


  conflicting = d->conflict;

  if(d->level == 0) {
    cm->currentDecision--;
    return (-1);
  }

  stats = cm->each;
  option = cm->option;


  stats->nBacktracks++;

  clauseArray = cm->auxArray;

  bLevel = 0;
  fdaLit = -1;
  clauseArray->num = 0;

  /*  Find Unique Implication Point */
  sat_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
  stats->nNonchonologicalBacktracks += (d->level - bLevel);


  if(clauseArray->num == 0) {
    sat_PrintImplicationGraph(cm, d);
    sat_PrintNode(cm, conflicting);
  }

  /* If we could find UIP then it is critical error...
  * at lease the decision node has to be detected as UIP.
  */
  if(fdaLit == -1) {
    fprintf(cm->stdOut, "%s ERROR : Illegal unit literal\n", cm->comment);
    fflush(cm->stdOut);
    sat_PrintNode(cm, conflicting);
    sat_PrintImplicationGraph(cm, d);
    sat_PrintDotForConflict(cm, d, conflicting, 0);
    exit(0);
  }

  if(bLevel && cm->lowestBacktrackLevel > bLevel)
    cm->lowestBacktrackLevel = bLevel;

  bLevel = sat_AddConflictClauseAndBacktrackForLifting(
	  cm, clauseArray, d, fdaLit, bLevel, objectFlag, 0);

  return(bLevel);
}
/**Function********************************************************************

  Synopsis    [ Conflict Analysis on blocking clause]

  Description [ Conflict Analysis on blocking clause]

  SideEffects []

  SeeAlso     []

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

int
sat_ConflictAnalysisWithBlockingClause(
	satManager_t *cm,
	satLevel_t *d)
{
satStatistics_t *stats;
satOption_t *option;
satArray_t *clauseArray;
int objectFlag;
int bLevel;
long fdaLit, conflicting;


  conflicting = d->conflict;

  if(d->level == 0) {
    cm->currentDecision--;
    return (-1);
  }

  stats = cm->each;
  option = cm->option;


  stats->nBacktracks++;

  clauseArray = cm->auxArray;

  bLevel = 0;
  fdaLit = -1;
  clauseArray->num = 0;

  /*  Find Unique Implication Point */
  sat_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
  stats->nNonchonologicalBacktracks += (d->level - bLevel);


  if(clauseArray->num == 0) {
    sat_PrintImplicationGraph(cm, d);
    sat_PrintNode(cm, conflicting);
  }

  /* If we could find UIP then it is critical error...
  * at lease the decision node has to be detected as UIP.
  */
  if(fdaLit == -1) {
    fprintf(cm->stdOut, "%s ERROR : Illegal unit literal\n", cm->comment);
    fflush(cm->stdOut);
    sat_PrintNode(cm, conflicting);
    sat_PrintImplicationGraph(cm, d);
    sat_PrintDotForConflict(cm, d, conflicting, 0);
    exit(0);
  }

  if(bLevel && cm->lowestBacktrackLevel > bLevel)
    cm->lowestBacktrackLevel = bLevel;

  bLevel = sat_AddConflictClauseWithNoScoreAndBacktrack(
	  cm, clauseArray, d, fdaLit, bLevel, objectFlag, 0);

  return(bLevel);
}

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

  Synopsis    [ Strong Conflict Analysis.]

  Description [ Strong Conflict Analysis.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
sat_StrongConflictAnalysis(
	satManager_t *cm,
	satLevel_t *d)
{
satStatistics_t *stats;
satOption_t *option;
satArray_t *clauseArray;
int objectFlag;
int bLevel;
long fdaLit, conflicting;


  conflicting = d->conflict;

  if(d->level == 0) {
      /** Bing : UNSAT core generation */
    if(cm->option->coreGeneration)
      sat_ConflictAnalysisForCoreGen(cm, d);
    cm->currentDecision--;
    return (-1);
  }

  stats = cm->each;
  option = cm->option;


  stats->nBacktracks++;

  if(SATflags(conflicting) & IsCNFMask) {
    SATnumConflict(conflicting) += 1;
  }

  clauseArray = cm->auxArray;

  bLevel = 0;
  fdaLit = -1;
  clauseArray->num = 0;

  /*  Find Unique Implication Point */
  sat_FindUIPAndNonUIP(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
  stats->nNonchonologicalBacktracks += (d->level - bLevel);


  if(clauseArray->num == 0) {
    sat_PrintImplicationGraph(cm, d);
    sat_PrintNode(cm, conflicting);
  }

  /* If we could find UIP then it is critical error...
  * at lease the decision node has to be detected as UIP.
  */
  if(fdaLit == -1) {
    fprintf(cm->stdOut, "%s ERROR : Illegal unit literal\n", cm->comment);
    fflush(cm->stdOut);
    sat_PrintNode(cm, conflicting);
    sat_PrintImplicationGraph(cm, d);
    sat_PrintDotForConflict(cm, d, conflicting, 0);
    exit(0);
  }

  if(bLevel && cm->lowestBacktrackLevel > bLevel)
    cm->lowestBacktrackLevel = bLevel;

  bLevel = sat_AddConflictClauseAndBacktrack(
	  cm, clauseArray, d, fdaLit, bLevel, objectFlag, 1);

  return(bLevel);
}

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

  Synopsis    [ Add conflict clause and backtrack.]

  Description [ Add conflict clause and backtrack.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
sat_AddConflictClauseAndBacktrack(
	satManager_t *cm,
	satArray_t *clauseArray,
	satLevel_t *d,
	long fdaLit,
	int bLevel,
	int objectFlag,
	int strongFlag)
{
int inverted;
long conflicting, learned;
satOption_t *option;
satStatistics_t *stats;
satArray_t *nClauseArray;

 RTManager_t * rm = cm->rm;

  option = cm->option;
  stats = cm->each;

  inverted = SATisInverted(fdaLit);
  fdaLit = SATnormalNode(fdaLit);

  conflicting = d->conflict;

  if(option->verbose > 2) {
    if(option->verbose > 4)
      sat_PrintNode(cm, conflicting);
    fprintf(cm->stdOut, "conflict at %3d on %6ld  bLevel %d UnitLit ",
	    d->level, conflicting, bLevel);
    sat_PrintNodeAlone(cm, fdaLit);
    fprintf(cm->stdOut, "\n");
  }

  d->conflict = 0;

  /* unit literal conflict clause */
  if(clauseArray->num == 1) {
    learned = sat_AddUnitConflictClause(cm, clauseArray, objectFlag);
    stats->nUnitConflictCl++;
    cm->currentTopConflict = cm->literals->last-1;
    cm->currentTopConflictCount = 0;

    sat_Backtrack(cm, 0);

    if(SATlevel(fdaLit) == 0) {
      if(cm->option->coreGeneration){
	if(cm->option->RT){
	  st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);

	  st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
	  RT_oriClsIdx(rm->root) = learned;
	}
	else{
	  st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
	  st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
	}
      }
      cm->currentDecision = -1;
      return (-1);
    }

    d = SATgetDecision(cm->currentDecision);
    cm->implicatedSoFar -= d->implied->num;
    SATante(fdaLit) = 0;

    SATvalue(fdaLit) = inverted;
    SATmakeImplied(fdaLit, d);

    if((SATflags(fdaLit) & InQueueMask)  == 0) {
      sat_Enqueue(cm->queue, fdaLit);
      SATflags(fdaLit) |= InQueueMask;
    }

    clauseArray->num = 0;

    if(option->incTraceObjective && objectFlag == 0)
      sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(fdaLit));

    if(option->incDistill && objectFlag)
      sat_ArrayInsert(cm->objUnitLitArray, SATnot(fdaLit));

    if(objectFlag)
      SATflags(fdaLit) |= ObjMask;

    /* Bing: UNSAT core generation */
    if(cm->option->coreGeneration){
      if(cm->option->RT){
	st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);

	st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
	RT_oriClsIdx(rm->root) = learned;
	 }
      else{
	st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
	st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
      }
    }
    return(bLevel);
  }

  if(strongFlag && (SATnumConflict(conflicting) % 5) == 0 &&
	  clauseArray->num > 4) {
    nClauseArray = sat_ArrayAlloc(clauseArray->num);
    memcpy(nClauseArray->space, clauseArray->space, sizeof(long)*clauseArray->num);
    nClauseArray->num = clauseArray->num;
    clauseArray->num = 0;
    bLevel = sat_ConflictAnalysisUsingAuxImplication(cm, nClauseArray);
    sat_ArrayFree(nClauseArray);
  }
  else {
    /* add conflict learned clause */
    learned = sat_AddConflictClause(cm, clauseArray, objectFlag);
    cm->currentTopConflict = cm->literals->last-1;
    cm->currentTopConflictCount = 0;

     /* Bing: UNSAT core generation */
    if(cm->option->coreGeneration){

      if(cm->option->RT){
	st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
	RT_oriClsIdx(rm->root) = learned;
	}
      else{
	st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
      }
    }

    if(option->verbose > 2) {
      sat_PrintNode(cm, learned);
      fflush(cm->stdOut);
    }


    /* apply Deepest Variable Hike decision heuristic */
    if(option->decisionHeuristic & DVH_DECISION)
      sat_UpdateDVH(cm, d, clauseArray, bLevel, fdaLit);

    /* Backtrack and failure driven assertion */
    sat_Backtrack(cm, bLevel);

    d = SATgetDecision(bLevel);
    cm->implicatedSoFar -= d->implied->num;

    SATante(fdaLit) = learned;
    SATvalue(fdaLit) = inverted;
    SATmakeImplied(fdaLit, d);

    if((SATflags(fdaLit) & InQueueMask)  == 0) {
      sat_Enqueue(cm->queue, fdaLit);
      SATflags(fdaLit) |= InQueueMask;
    }

    clauseArray->num = 0;
    if(objectFlag)
      SATflags(fdaLit) |= ObjMask;

  }

  return(bLevel);
}

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

  Synopsis    [ Add conflict clause and backtrack.]

  Description [ Add conflict clause and backtrack.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
sat_AddConflictClauseAndBacktrackForLifting(
	satManager_t *cm,
	satArray_t *clauseArray,
	satLevel_t *d,
	long fdaLit,
	int bLevel,
	int objectFlag,
	int strongFlag)
{
int inverted;
long conflicting, learned;
satOption_t *option;
satStatistics_t *stats;
satArray_t *nClauseArray;

  option = cm->option;
  stats = cm->each;

  inverted = SATisInverted(fdaLit);
  fdaLit = SATnormalNode(fdaLit);

  conflicting = d->conflict;

  if(option->verbose > 2) {
    if(option->verbose > 4)
      sat_PrintNode(cm, conflicting);
    fprintf(cm->stdOut, "conflict at %3d on %6ld  bLevel %d UnitLit ",
	    d->level, conflicting, bLevel);
    sat_PrintNodeAlone(cm, fdaLit);
    fprintf(cm->stdOut, "\n");
  }

  d->conflict = 0;

  /* unit literal conflict clause */
  if(clauseArray->num == 1) {
    learned = sat_AddUnitConflictClause(cm, clauseArray, objectFlag);
    stats->nUnitConflictCl++;
    cm->currentTopConflict = cm->literals->last-1;
    cm->currentTopConflictCount = 0;

    sat_Backtrack(cm, 0);

    if(SATlevel(fdaLit) == 0) {
      if(cm->option->coreGeneration){
	st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
	st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
      }
      cm->currentDecision = -1;
      return (-1);
    }

    d = SATgetDecision(cm->currentDecision);
    cm->implicatedSoFar -= d->implied->num;
    SATante(fdaLit) = 0;

    SATvalue(fdaLit) = inverted;
    SATmakeImplied(fdaLit, d);

    if((SATflags(fdaLit) & InQueueMask)  == 0) {
      sat_Enqueue(cm->queue, fdaLit);
      SATflags(fdaLit) |= InQueueMask;
    }

    clauseArray->num = 0;

    if(option->incTraceObjective && objectFlag == 0)
      sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(fdaLit));

    if(option->incDistill && objectFlag)
      sat_ArrayInsert(cm->objUnitLitArray, SATnot(fdaLit));

    if(objectFlag)
      SATflags(fdaLit) |= ObjMask;

    /* Bing: UNSAT core generation */
    if(cm->option->coreGeneration){
      st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
      st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
    }
    return(0);
  }

  if(strongFlag && (SATnumConflict(conflicting) % 5) == 0 &&
	  clauseArray->num > 4) {
    nClauseArray = sat_ArrayAlloc(clauseArray->num);
    memcpy(nClauseArray->space, clauseArray->space, sizeof(long)*clauseArray->num);
    nClauseArray->num = clauseArray->num;
    clauseArray->num = 0;
    bLevel = sat_ConflictAnalysisUsingAuxImplication(cm, nClauseArray);
    sat_ArrayFree(nClauseArray);
  }
  else {
    /* add conflict learned clause */
    learned = sat_AddConflictClause(cm, clauseArray, objectFlag);
    cm->currentTopConflict = cm->literals->last-1;
    cm->currentTopConflictCount = 0;

     /* Bing: UNSAT core generation */
    if(cm->option->coreGeneration){
      st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
    }

    if(option->verbose > 2) {
      sat_PrintNode(cm, learned);
      fflush(cm->stdOut);
    }


    /* apply Deepest Variable Hike decision heuristic */
    /**
    if(option->decisionHeuristic & DVH_DECISION)
      sat_UpdateDVH(cm, d, clauseArray, bLevel, fdaLit);
      **/

    /* Backtrack and failure driven assertion */
    sat_Backtrack(cm, bLevel);

    d = SATgetDecision(bLevel);
    cm->implicatedSoFar -= d->implied->num;

    SATante(fdaLit) = learned;
    SATvalue(fdaLit) = inverted;
    SATmakeImplied(fdaLit, d);

    if((SATflags(fdaLit) & InQueueMask)  == 0) {
      sat_Enqueue(cm->queue, fdaLit);
      SATflags(fdaLit) |= InQueueMask;
    }

    clauseArray->num = 0;
    if(objectFlag)
      SATflags(fdaLit) |= ObjMask;

  }

  return(bLevel);
}

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

  Synopsis    [ Add conflict clause with no score update and backtrack.]

  Description [ Add conflict clause with no score update and backtrack.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
sat_AddConflictClauseWithNoScoreAndBacktrack(
	satManager_t *cm,
	satArray_t *clauseArray,
	satLevel_t *d,
	long fdaLit,
	int bLevel,
	int objectFlag,
	int strongFlag)
{
int inverted;
long conflicting, learned;
satOption_t *option;
satStatistics_t *stats;
satArray_t *nClauseArray;

  option = cm->option;
  stats = cm->each;

  inverted = SATisInverted(fdaLit);
  fdaLit = SATnormalNode(fdaLit);

  conflicting = d->conflict;

  if(option->verbose > 2) {
    if(option->verbose > 4)
      sat_PrintNode(cm, conflicting);
    fprintf(cm->stdOut, "conflict at %3d on %6ld  bLevel %d UnitLit ",
	    d->level, conflicting, bLevel);
    sat_PrintNodeAlone(cm, fdaLit);
    fprintf(cm->stdOut, "\n");
  }

  d->conflict = 0;

  /* unit literal conflict clause */
  if(clauseArray->num == 1) {
    learned = sat_AddUnitConflictClause(cm, clauseArray, objectFlag);
    stats->nUnitConflictCl++;
    cm->currentTopConflict = cm->literals->last-1;
    cm->currentTopConflictCount = 0;

    sat_Backtrack(cm, 0);

    if(SATlevel(fdaLit) == 0) {
      if(cm->option->coreGeneration){
	st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
	st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
      }
      cm->currentDecision = -1;
      return (-1);
    }

    d = SATgetDecision(cm->currentDecision);
    cm->implicatedSoFar -= d->implied->num;
    SATante(fdaLit) = 0;

    SATvalue(fdaLit) = inverted;
    SATmakeImplied(fdaLit, d);

    if((SATflags(fdaLit) & InQueueMask)  == 0) {
      sat_Enqueue(cm->queue, fdaLit);
      SATflags(fdaLit) |= InQueueMask;
    }

    clauseArray->num = 0;

    if(option->incTraceObjective && objectFlag == 0)
      sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(fdaLit));

    if(option->incDistill && objectFlag)
      sat_ArrayInsert(cm->objUnitLitArray, SATnot(fdaLit));

    if(objectFlag)
      SATflags(fdaLit) |= ObjMask;

    /* Bing: UNSAT core generation */
    if(cm->option->coreGeneration){
      st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
      st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
    }
    return(bLevel);
  }

  if(strongFlag && (SATnumConflict(conflicting) % 5) == 0 &&
	  clauseArray->num > 4) {
    nClauseArray = sat_ArrayAlloc(clauseArray->num);
    memcpy(nClauseArray->space, clauseArray->space, sizeof(long)*clauseArray->num);
    nClauseArray->num = clauseArray->num;
    clauseArray->num = 0;
    bLevel = sat_ConflictAnalysisUsingAuxImplication(cm, nClauseArray);
    sat_ArrayFree(nClauseArray);
  }
  else {
    /* add conflict learned clause */
    learned = sat_AddConflictClauseNoScoreUpdate(cm, clauseArray, objectFlag);
    cm->currentTopConflict = cm->literals->last-1;
    cm->currentTopConflictCount = 0;

     /* Bing: UNSAT core generation */
    if(cm->option->coreGeneration){
      st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
    }

    if(option->verbose > 2) {
      sat_PrintNode(cm, learned);
      fflush(cm->stdOut);
    }


    /* apply Deepest Variable Hike decision heuristic */
    if(option->decisionHeuristic & DVH_DECISION)
      sat_UpdateDVH(cm, d, clauseArray, bLevel, fdaLit);

    /* Backtrack and failure driven assertion */
    sat_Backtrack(cm, bLevel);

    d = SATgetDecision(bLevel);
    cm->implicatedSoFar -= d->implied->num;

    SATante(fdaLit) = learned;
    SATvalue(fdaLit) = inverted;
    SATmakeImplied(fdaLit, d);

    if((SATflags(fdaLit) & InQueueMask)  == 0) {
      sat_Enqueue(cm->queue, fdaLit);
      SATflags(fdaLit) |= InQueueMask;
    }

    clauseArray->num = 0;
    if(objectFlag)
      SATflags(fdaLit) |= ObjMask;

  }

  return(bLevel);
}

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

  Synopsis    [ Minimize conflict clause by rebuilding implication graph.]

  Description [ Minimize conflict clause by rebuilding implication graph.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
sat_ConflictAnalysisUsingAuxImplication(
	satManager_t *cm,
	satArray_t *clauseArray)
{
int tLevel, level, bLevel;
int i, size;
int value, tvalue;
int minConflict, maxConflict;
long v, tv, conflicting;
satLevel_t *d;
satArray_t *nClauseArray;
double aMean, hMean, gMean;
int objectFlag;
long fdaLit;

  SATcm = cm;
  qsort(clauseArray->space, clauseArray->num, sizeof(int), levelCompare);
  tLevel = cm->currentDecision;

  tv = clauseArray->space[0];
  v = SATnormalNode(tv);
  level = SATlevel(v);
  minConflict = cm->decisionHead[level].nConflict;
  tv = clauseArray->space[clauseArray->num-1];
  v = SATnormalNode(tv);
  level = SATlevel(v);
  maxConflict = cm->decisionHead[level].nConflict;

  aMean = hMean = 0;

  for(i=0; i<clauseArray->num; i++) {
    tv = clauseArray->space[i];
    v = SATnormalNode(tv);
    level = SATlevel(v);
    if(level < tLevel) tLevel = level;
    aMean = aMean + (double)level;
    hMean = hMean + 1.0/(double)level;
  }
  aMean = aMean/(double)clauseArray->num;
  hMean = (double)clauseArray->num/hMean;
  gMean = sqrt(aMean*hMean);

  sat_Backtrack(cm, tLevel-1);

  size = clauseArray->num;

  for(i=0; i<size; i++) {
    tv = clauseArray->space[i];
    value = !SATisInverted(tv);
    v = SATnormalNode(tv);
    tvalue = SATvalue(v);

    if(tvalue != 2)	{
	/**
      if(tvalue != value) {
	fprintf(stdout, "ERROR : Inconsitent value is implied\n");
	sat_ReportStatistics(cm, cm->each);
      }
      **/
      continue;
    }
    d = sat_AllocLevel(cm);

    SATvalue(v) = value;
    SATmakeImplied(v, d);
    d->decisionNode = v;
    d->nConflict = cm->each->nConflictCl;
    if((SATflags(v) & InQueueMask) == 0) {
      sat_Enqueue(cm->queue, v);
      SATflags(v) |= InQueueMask;
    }
    sat_ImplicationMain(cm, d);

    if(d->conflict) {
      conflicting = d->conflict;
      break;
    }
  }

  if(d->conflict) {
    nClauseArray = cm->auxArray;
    bLevel = 0;
    fdaLit = -1;
    nClauseArray->num = 0;
    sat_FindUIP(cm, nClauseArray, d, &objectFlag, &bLevel, &fdaLit);

    /**
    fprintf(stdout, "tLevel %d gLevel %.1lf  %ld -> %ld min %d max %d\n",
	    tLevel, gMean, clauseArray->num, nClauseArray->num,
	    minConflict, maxConflict);
	    **/

    bLevel = sat_AddConflictClauseAndBacktrack(
	    cm, nClauseArray, d, fdaLit, bLevel, objectFlag, 0);


  }
  else {
    bLevel = cm->currentDecision;
  }
  return(bLevel);

}


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

  Synopsis    [ Conflict Analysis that is used for UNSAT core generation.]

  Description [ Conflict Analysis that is used for UNSAT core generation.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
sat_ConflictAnalysisForCoreGen(
	satManager_t *cm,
	satLevel_t *d)
{
satStatistics_t *stats;
satOption_t *option;
satArray_t *clauseArray;
int objectFlag;
int bLevel;
long fdaLit, learned, conflicting;
int inverted;

RTManager_t * rm = cm->rm;

  if(d->level != 0) {
    fprintf(stdout, "ERROR : Can't use this function at higher than level 0\n");
    return(0);
  }

  conflicting = d->conflict;

  stats = cm->each;
  option = cm->option;

  stats->nBacktracks++;

  clauseArray = cm->auxArray;

  bLevel = 0;
  fdaLit = -1;
  clauseArray->num = 0;

  /* Find Unique Implication Point */

  if(option->RT)
    sat_FindUIPForCoreGenWithRT(cm, clauseArray, d, &objectFlag, &bLevel,&fdaLit);
  else
    sat_FindUIPForCoreGen(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);

  if(fdaLit < 0 )
    fprintf(stdout, "ERROR : critical\n");

  inverted = SATisInverted(fdaLit);
  fdaLit = SATnormalNode(fdaLit);

  d->conflict = 0;

  assert(clauseArray->num == 1);
  learned = sat_AddUnitConflictClause(cm, clauseArray, objectFlag);

  SATante(fdaLit) = 0;

  clauseArray->num = 0;

  /* Bing: UNSAT core generation */
  if(cm->option->coreGeneration){
    st_insert(cm->anteTable,(char*)(long)SATnormalNode(fdaLit),(char*)(long)learned);
    if(option->RT){
      st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
      RT_oriClsIdx(rm->root) = learned;
    }
    else
      st_insert(cm->dependenceTable, (char *)(long)learned, (char *)(long)cm->dependenceArray);
  }
  return 1;
}

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

  Synopsis    [ Find Unique implication point]

  Description [ After finding unique implication point, the backtrack level
		and failure driven assertion are identified. ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_FindUIP(
	satManager_t *cm,
	satArray_t *clauseArray,
	satLevel_t *d,
	int *objectFlag,
	int *bLevel,
	long *fdaLit)
{
long conflicting;
int nMarked, value;
int first, i;
long *space, v;
satArray_t *implied;
satOption_t *option;

  conflicting = d->conflict;
  nMarked = 0;
  option = cm->option;
  if(option->incTraceObjective) *objectFlag = 0;
  else                          *objectFlag = ObjMask;

  (*objectFlag) |= (SATflags(conflicting) & ObjMask);

  /* find seed from conflicting clause to find unique implication point.
   * */
  clauseArray->num = 0;

  if(SATflags(conflicting) & IsCNFMask)
    SATconflictUsage(conflicting)++;

  sat_MarkNodeInConflict(
	  cm, d, &nMarked, objectFlag, bLevel, clauseArray);

  /* Traverse implication graph backward */
  first = 1;
  implied = d->implied;
  space = implied->space+implied->num-1;
  /* Bing:  UNSAT core generation */
  if(cm->option->coreGeneration){
    cm->dependenceArray = sat_ArrayAlloc(1);
    sat_ArrayInsert(cm->dependenceArray,conflicting);
  }

  for(i=implied->num-1; i>=0; i--, space--) {
    v = *space;
    if(SATflags(v) & VisitedMask) {
      SATflags(v) &= ResetVisitedMask;
      --nMarked;

      if(nMarked == 0 && (!first || i==0))  {
	value = SATvalue(v);
	*fdaLit = v^(!value);
	sat_ArrayInsert(clauseArray, *fdaLit);
	break;
      }

      /* Bing: UNSAT core genration */
      if(cm->option->coreGeneration){
	int ante = SATante(v);
	if(ante!=0 && !(SATflags(ante) & IsCNFMask)){
	  printf("node %d is not CNF\n", ante);
	  exit(0);
	}
	if(ante==0){
	  if(!st_lookup(cm->anteTable, (char *)SATnormalNode(v), &ante)){
	    printf("ante = 0 and is not in anteTable %ld\n",v);
	    exit(0);
	  }
	}
	sat_ArrayInsert(cm->dependenceArray,ante);
      }

      sat_MarkNodeInImpliedNode(
	      cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
    }
    first = 0;
  }


  /* Minimize conflict clause */
  if(option->minimizeConflictClause)
    sat_MinimizeConflictClause(cm, clauseArray);
  else
    sat_ResetFlagForClauseArray(cm, clauseArray);

  return;
}
/**Function********************************************************************

  Synopsis    [find UIP with resolution generation]

  Description []

  SideEffects []

  SeeAlso     []

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


void
sat_FindUIPWithRT(
	satManager_t *cm,
	satArray_t *clauseArray,
	satLevel_t *d,
	int *objectFlag,
	int *bLevel,
	long *fdaLit)
{
long conflicting;
int nMarked, value;
int first, i,j;
long *space, v,left,right,inverted,result,*tmp;
satArray_t *implied;
satOption_t *option;
RTnode_t  tmprt;
int size = 0;
long *lp,*tmpIP,ante,ante2,node;
 RTManager_t * rm = cm->rm;

  conflicting = d->conflict;
  nMarked = 0;
  option = cm->option;
  if(option->incTraceObjective) *objectFlag = 0;
  else                          *objectFlag = ObjMask;

  (*objectFlag) |= (SATflags(conflicting) & ObjMask);

  /* find seed from conflicting clause to find unique implication point.
   * */
  clauseArray->num = 0;
  sat_MarkNodeInConflict(
	  cm, d, &nMarked, objectFlag, bLevel, clauseArray);

  /* Traverse implication graph backward */
  first = 1;
  implied = d->implied;
  space = implied->space+implied->num-1;


  if(cm->option->coreGeneration){
    /*if last conflict is CNF*/
    if(SATflags(conflicting)&IsCNFMask){
      /*is conflict CNF*/
      if(SATflags(conflicting)&IsConflictMask){
	 if(!st_lookup(cm->RTreeTable,(char*)conflicting,&tmprt)){
	    printf("RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
	    exit(0);
	  }
	  else{
	    rm->root = tmprt;
#if PR
	    printf("Get formula for CONFLICT CLAUSE:%d\n",ante);
#endif
	  }
      }
      /*CNF but not conflict*/
      else{
	rm->root = RTCreateNode(rm);

	size = SATnumLits(conflicting);
	RT_fSize(rm->root) = size;
	lp = (long*)SATfirstLit(conflicting);
	sat_BuildRT(cm,rm->root, lp, tmpIP,size,0);
      }
    }
    /*if last conflict is AIG*/
    else{
      rm->root = RTCreateNode(rm);
      node = SATnormalNode(conflicting);
      left = SATleftChild(node);
      right = SATrightChild(node);
      result = PureSat_IdentifyConflict(cm,left,right,conflicting);
      inverted = SATisInverted(left);
      left = SATnormalNode(left);
      left = inverted ? SATnot(left) : left;

      inverted = SATisInverted(right);
      right = SATnormalNode(right);
      right = inverted ? SATnot(right) : right;

      j = node;

      if(result == 1){
	tmp = ALLOC(long,3);
	tmp[0] = left;
	tmp[1] = SATnot(j);
	size = 2;
      }
      else if(result == 2){
	tmp = ALLOC(long,3);
	tmp[0] = right;
	tmp[1] = SATnot(j);
	size = 2;
      }
      else if(result == 3){
	tmp = ALLOC(long,4);
	tmp[0] = SATnot(left);
	tmp[1] = SATnot(right);
	tmp[2] = j;
	size = 3;
      }
      else{
	printf("wrong returned result value, exit\n");
	exit(0);
      }

      lp = tmp;
      sat_BuildRT(cm,rm->root, lp, tmpIP,size,1);
      FREE(tmp);
    }
  }


  for(i=implied->num-1; i>=0; i--, space--) {
    v = *space;
    if(SATflags(v) & VisitedMask) {
      SATflags(v) &= ResetVisitedMask;
      --nMarked;

      if(nMarked == 0 && (!first || i==0))  {
	value = SATvalue(v);
	*fdaLit = v^(!value);
	sat_ArrayInsert(clauseArray, *fdaLit);
	break;
      }


      if(cm->option->coreGeneration){
	ante = SATante(v);
	if(ante==0){
	  if(!(st_lookup(cm->anteTable, (char *)SATnormalNode(v),&ante))){
	    printf("ante = 0 and is not in anteTable %ld\n",v);
	    exit(0);
	  }
	}

	/*build non-leaf node*/
	tmprt = RTCreateNode(rm);
	RT_pivot(tmprt) = SATnormalNode(v);
	RT_right(tmprt) = rm->root;
	rm->root = tmprt;

	if((SATflags(ante)&IsConflictMask)&&(SATflags(ante)&IsCNFMask)){
	  if(!st_lookup(cm->RTreeTable,(char*)ante,&tmprt)){
	    printf("RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
	    exit(0);
	  }
	  else{
	    RT_left(rm->root) = tmprt;
#if PR
	    printf("Get formula for CONFLICT CLAUSE:%d\n",ante);
#endif
	  }
	}
	else{ /* if not conflict CNF*/
	  /*left  */
	  tmprt = RTCreateNode(rm);
	  RT_left(rm->root) = tmprt;
	  /*left is AIG*/
	  if(!(SATflags(ante) & IsCNFMask)){
	    /*generate formula for left*/
	    tmp = ALLOC(long,3);
	    value = SATvalue(v);
	    node = SATnormalNode(v);
	    node = value==1?node:SATnot(node);
	    tmp[0] = node;

	    size = 1;
	    if(ante != SATnormalNode(v)){
	      value = SATvalue(ante);
	      node = SATnormalNode(ante);
	      node = value==1?SATnot(node):node;
	      tmp[1] = node;
	      size++;
	      ante2 = SATante2(v);
	      if(ante2){
		value = SATvalue(ante2);
		node = SATnormalNode(ante2);
		node = value==1?SATnot(node):node;
		tmp[2] = node;
		size++;
	      }
	    }

	    lp = tmp;
	    sat_BuildRT(cm,tmprt,lp,tmpIP,size,1);
	    FREE(tmp);
	  }
	  /* left is CNF*/
	  else{

	    lp = (long*)SATfirstLit(ante);
	    size = SATnumLits(ante);
	    RT_fSize(tmprt) = size;
	    sat_BuildRT(cm,tmprt, lp, tmpIP,size,0);
	  }
	} /*else{ // if not conflict CNF*/

      }/*if(cm->option->coreGeneration){*/


      sat_MarkNodeInImpliedNode(
	      cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
    }
    first = 0;
  }


  /* Minimize conflict clause */
  if(option->minimizeConflictClause)
    sat_MinimizeConflictClause(cm, clauseArray);
  else
    sat_ResetFlagForClauseArray(cm, clauseArray);

  return;
}

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

  Synopsis    [ Find Unique implication point and find cut to generate additional conflict clause]

  Description [ After finding unique implication point, the backtrack level
		and failure driven assertion are identified. ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_FindUIPAndNonUIP(
	satManager_t *cm,
	satArray_t *clauseArray,
	satLevel_t *d,
	int *objectFlag,
	int *bLevel,
	long *fdaLit)
{
long conflicting;
int nMarked, value;
int first, i, j;
int size, oSize;
int depth, maxSize;
long *space, v, nv, maxV;
long ante, ante2;
long learned;
long *plit;
satArray_t *implied;
satArray_t *nClauseArray;
satOption_t *option;
int tLevel, inverted, lBacktrace, uBacktrace;
int minLimit, markLimit, tObjectFlag;
int inserted;
long tFdaLit;

/** HSJIN : Need to be update to make it consider UNSAT core generation **/
  conflicting = d->conflict;
  nMarked = 0;
  option = cm->option;
  if(option->incTraceObjective) *objectFlag = 0;
  else                          *objectFlag = ObjMask;

  (*objectFlag) |= (SATflags(conflicting) & ObjMask);

  /* find seed from conflicting clause to find unique implication point.
   * */
  clauseArray->num = 0;

  if(SATflags(conflicting) & IsCNFMask)
    SATconflictUsage(conflicting)++;

  sat_MarkNodeInConflict(
	  cm, d, &nMarked, objectFlag, bLevel, clauseArray);

  /* Traverse implication graph backward */
  first = 1;
  implied = d->implied;
  space = implied->space+implied->num-1;
  maxSize = 0;
  maxV = 0;
  /* Bing:  UNSAT core generation */
  if(cm->option->coreGeneration){
    cm->dependenceArray = sat_ArrayAlloc(1);
    sat_ArrayInsert(cm->dependenceArray,conflicting);
  }

  for(i=implied->num-1; i>=0; i--, space--) {
    v = *space;
    if(SATflags(v) & VisitedMask) {
      SATflags(v) &= ResetVisitedMask;
      --nMarked;

      depth = cm->variableArray[SATnodeID(v)].depth;
      if(nMarked == 0 && (!first || i==0))  {
	value = SATvalue(v);
	*fdaLit = v^(!value);
	sat_ArrayInsert(clauseArray, *fdaLit);
	break;
      }

      ante = SATante(v);
      /* Bing: UNSAT core genration */
      if(cm->option->coreGeneration){
	if(ante!=0 && !(SATflags(ante) & IsCNFMask)){
	  printf("node %ld is not CNF\n", ante);
	  exit(0);
	}
	if(ante==0){
	  if(!st_lookup(cm->anteTable, (char *)SATnormalNode(v), &ante)){
	    printf("ante = 0 and is not in anteTable %ld\n",v);
	    exit(0);
	  }
	}
	sat_ArrayInsert(cm->dependenceArray,ante);
      }

      /**
      sat_MarkNodeInImpliedNode(
	      cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
	      **/

      if(SATflags(ante) & IsCNFMask) {
	SATconflictUsage(ante)++;
	size = SATnumLits(ante);
	oSize = clauseArray->num;
	for(j=0, plit=(long*)SATfirstLit(ante); j<size; j++, plit++) {
	  nv = SATgetNode(*plit);
	  if(SATnormalNode(nv) != v)	{
	    sat_MarkNodeSub(cm, nv, &nMarked, bLevel, d, clauseArray);
	    if(cm->variableArray[SATnodeID(nv)].depth <= depth) {
	      cm->variableArray[SATnodeID(nv)].depth = depth+1;
	    }
	  }
	}
	oSize = clauseArray->num-oSize;
	if(oSize > maxSize) {
	  maxSize = oSize;
	  maxV = v;
	}
      }
      else {
	sat_MarkNodeSub(cm, ante, &nMarked, bLevel, d, clauseArray);
	ante2 = SATante2(v);
	if(ante2)
	  sat_MarkNodeSub(cm, ante2, &nMarked, bLevel, d, clauseArray);
      }

    }
    first = 0;
  }

  /* Minimize conflict clause */
  if(option->minimizeConflictClause)
    sat_MinimizeConflictClause(cm, clauseArray);
  else
    sat_ResetFlagForClauseArray(cm, clauseArray);

  if(maxSize > clauseArray->num/4 && maxSize > 5) {
    nClauseArray = sat_ArrayAlloc(clauseArray->num);

    nMarked = 0;
    tLevel = 0;
    tObjectFlag |= (SATflags(conflicting) & ObjMask);

    sat_MarkNodeInConflict(
	  cm, d, &nMarked, &tObjectFlag, &tLevel, nClauseArray);

    /* Traverse implication graph backward */
    first = 1;
    implied = d->implied;
    space = implied->space+implied->num-1;
    for(i=implied->num-1; i>=0; i--, space--) {
      v = *space;
      if(v == maxV) {
	if(SATflags(v) & VisitedMask) {
	  SATflags(v) &= ResetVisitedMask;
	  --nMarked;
	  value = SATvalue(v);
	  sat_ArrayInsert(nClauseArray, v^(!value));
	}
	continue;
      }

      if(SATflags(v) & VisitedMask) {
	SATflags(v) &= ResetVisitedMask;
	--nMarked;

	if(nMarked == 0 && (!first || i == 0))  {
	  value = SATvalue(v);
	  tFdaLit = v^(!value);
	  sat_ArrayInsert(nClauseArray, tFdaLit);
	  break;
	}

	ante= SATante(v);
	inverted = SATisInverted(ante);
	ante= SATnormalNode(ante);

	if(SATflags(ante) & IsCNFMask) {
	  size = SATnumLits(ante);
	  for(j=0, plit=(long*)SATfirstLit(ante); j<size; j++, plit++) {
	    nv = SATgetNode(*plit);
	    if(SATnormalNode(nv) != v)
	      sat_MarkNodeSub(cm, nv, &nMarked, &tLevel, d, nClauseArray);
	  }
	}
	else {
	  sat_MarkNodeSub(cm, ante, &nMarked, &tLevel, d, nClauseArray);
	  ante2 = SATante2(v);
	  if(ante2)
	    sat_MarkNodeSub(cm, ante2, &nMarked, &tLevel, d, nClauseArray);
	}
      }
      first = 0;
    }
    sat_MinimizeConflictClause(cm, nClauseArray);

    inserted = 0;
    if(clauseArray->num*4/5 > nClauseArray->num) {
      learned = sat_AddConflictClauseNoScoreUpdate(cm, nClauseArray, tObjectFlag);
      inserted = 1;
    }
    sat_ArrayFree(nClauseArray);
  }
  if( inserted == 0 &&
      depth > 20) {
    nClauseArray = sat_ArrayAlloc(clauseArray->num);

    lBacktrace = depth/3;
    uBacktrace = depth*2/3;

    /** HSJIN : depth, lBacktrace and uBacktrace may affect to
     * performance **/
    markLimit = 1;
    minLimit = 1000;
    while(1){
      nMarked = 0;
      tLevel = 0;
      depth = 0;
      nClauseArray->num = 0;
      markLimit++;
      if(markLimit > 3)	break;
      if(minLimit != 1000 && minLimit > 3)
	break;
      tObjectFlag |= (SATflags(conflicting) & ObjMask);

      sat_MarkNodeInConflict(
	    cm, d, &nMarked, &tObjectFlag, &tLevel, nClauseArray);

      first = 1;
      implied = d->implied;
      space = implied->space+implied->num-1;
      for(i=implied->num-1; i>=0; i--, space--) {
	v = *space;
	if(uBacktrace < depth) {
	  sat_ResetFlagForClauseArray(cm, nClauseArray);
	  nClauseArray->num = 0;
	  for(; i>=0; i--, space--) {
	    v = *space;
	    if(SATflags(v) & VisitedMask) {
	      SATflags(v) &= ResetVisitedMask;
	      --nMarked;
	      if(nMarked == 0)
		break;
	    }
	  }
	  break;
	}
	if(nMarked < minLimit)
	  minLimit = nMarked;
	if(depth > lBacktrace && nMarked < markLimit) {
	  for(; i>=0; i--, space--) {
	    v = *space;
	    if(SATflags(v) & VisitedMask) {
	      SATflags(v) &= ResetVisitedMask;
	      --nMarked;
	      value = SATvalue(v);
	      sat_ArrayInsert(nClauseArray, v^(!value));
	      if(nMarked == 0)
		break;
	    }
	  }
	}

	if(SATflags(v) & VisitedMask) {
	  depth = cm->variableArray[SATnodeID(v)].depth;

	  SATflags(v) &= ResetVisitedMask;
	  --nMarked;

	  if(nMarked == 0 && (!first || i == 0))  {
	    value = SATvalue(v);
	    tFdaLit = v^(!value);
	    sat_ArrayInsert(nClauseArray, tFdaLit);
	    break;
	  }

	  ante= SATante(v);
	  inverted = SATisInverted(ante);
	  ante= SATnormalNode(ante);

	  if(SATflags(ante) & IsCNFMask) {
	    size = SATnumLits(ante);
	    for(j=0, plit=(long*)SATfirstLit(ante); j<size; j++, plit++) {
	      nv = SATgetNode(*plit);
	      if(SATnormalNode(nv) != v)
		sat_MarkNodeSub(cm, nv, &nMarked, &tLevel, d, nClauseArray);
	    }
	  }
	  else {
	    sat_MarkNodeSub(cm, ante, &nMarked, &tLevel, d, nClauseArray);
	    ante2 = SATante2(v);
	    if(ante2)
	      sat_MarkNodeSub(cm, ante2, &nMarked, &tLevel, d, nClauseArray);
	  }
	}
	first = 0;
      }
      if(nClauseArray->num == 0)
	continue;
      sat_MinimizeConflictClause(cm, nClauseArray);

      if(clauseArray->num*4/5 > nClauseArray->num) {

	learned = sat_AddConflictClauseNoScoreUpdate(cm, nClauseArray, tObjectFlag);
	break;
      }
    }
    sat_ArrayFree(nClauseArray);
  }

  return;
}

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

  Synopsis    [ UIP Analysis that is used for UNSAT core generation.]

  Description [ UIP Analysis that is used for UNSAT core generation.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_FindUIPForCoreGen(
	satManager_t *cm,
	satArray_t *clauseArray,
	satLevel_t *d,
	int *objectFlag,
	int *bLevel,
	long *fdaLit)
{
long conflicting;
int nMarked, value;
long v;
int first, i;
long *space;
satArray_t *implied;
satOption_t *option;

  conflicting = d->conflict;
  nMarked = 0;
  option = cm->option;
  if(option->incTraceObjective) *objectFlag = 0;
  else                          *objectFlag = ObjMask;

  (*objectFlag) |= (SATflags(conflicting) & ObjMask);

  /*  find seed from conflicting clause to find unique implication point. */
  clauseArray->num = 0;
  sat_MarkNodeInConflict(
	  cm, d, &nMarked, objectFlag, bLevel, clauseArray);

  /* Traverse implication graph backward */
  first = 1;
  implied = d->implied;
  space = implied->space+implied->num-1;
  /* Bing: UNSAT core generation */
  if(cm->option->coreGeneration){
    cm->dependenceArray = sat_ArrayAlloc(1);
    sat_ArrayInsert(cm->dependenceArray,conflicting);
  }

  for(i=implied->num-1; i>=0; i--, space--) {
    v = *space;
    if(SATflags(v) & VisitedMask) {
      SATflags(v) &= ResetVisitedMask;
      --nMarked;

      if(nMarked == 0 && (!first || i==0))  {
	value = SATvalue(v);
	*fdaLit = v^(!value);
	sat_ArrayInsert(clauseArray, *fdaLit);
	break;
      }


       /* Bing: UNSAT core generation */
      if(cm->option->coreGeneration){
	int ante = SATante(v);
	if(ante!=0 && !(SATflags(ante) & IsCNFMask)){
	  printf("node %d is not CNF\n", ante);
	  exit(0);
	}
	if(ante==0){
	  if(!st_lookup(cm->anteTable, (char *)SATnormalNode(v), &ante)){
	    printf("ante = 0 and is not in anteTable %ld\n",v);
	    exit(0);
	  }
	}
	sat_ArrayInsert(cm->dependenceArray,ante);
      }


      sat_MarkNodeInImpliedNode(
	      cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
    }
    first = 0;
  }

  sat_ResetFlagForClauseArray(cm, clauseArray);

  return;
}

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

  Synopsis    [find UIP with resolution generation]

  Description []

  SideEffects []

  SeeAlso     []

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


void
sat_FindUIPForCoreGenWithRT(
	satManager_t *cm,
	satArray_t *clauseArray,
	satLevel_t *d,
	int *objectFlag,
	int *bLevel,
	long *fdaLit)
{
long conflicting;
int nMarked, value;
 long v,left,right,inverted,result;
int first, i,size=0;
long *space,*tmp;
satArray_t *implied;
satOption_t *option;
RTnode_t tmprt;
long  *lp, *tmpIP,ante,ante2,node,j;
 RTManager_t * rm = cm->rm;

  conflicting = d->conflict;
  nMarked = 0;
  option = cm->option;
  if(option->incTraceObjective) *objectFlag = 0;
  else                          *objectFlag = ObjMask;

  (*objectFlag) |= (SATflags(conflicting) & ObjMask);

  /*  find seed from conflicting clause to find unique implication point. */
  clauseArray->num = 0;
  sat_MarkNodeInConflict(
	  cm, d, &nMarked, objectFlag, bLevel, clauseArray);

  /* Traverse implication graph backward */
  first = 1;
  implied = d->implied;
  space = implied->space+implied->num-1;


  if(cm->option->coreGeneration){
    /*if last conflict is CNF*/
    if(SATflags(conflicting)&IsCNFMask){
      /*is conflict CNF*/
      if(SATflags(conflicting)&IsConflictMask){
	 if(!st_lookup(cm->RTreeTable,(char*)conflicting,&tmprt)){
	    printf("RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
	    exit(0);
	  }
	  else{
	    rm->root = tmprt;
#if PR
	    printf("Get formula for CONFLICT CLAUSE:%d\n",ante);
#endif
	  }
      }
      /*CNF but not conflict*/
      else{
	rm->root = RTCreateNode(rm);

	size = SATnumLits(conflicting);
	RT_fSize(rm->root) = size;
	lp = (long*)SATfirstLit(conflicting);
	sat_BuildRT(cm,rm->root, lp, tmpIP,size,0);
      }
    }
    /*if last conflict is AIG*/
    else{
      rm->root = RTCreateNode(rm);
      node = SATnormalNode(conflicting);
      left = SATleftChild(node);
      right = SATrightChild(node);
      result = PureSat_IdentifyConflict(cm,left,right,conflicting);
      inverted = SATisInverted(left);
      left = SATnormalNode(left);
      left = inverted ? SATnot(left) : left;

      inverted = SATisInverted(right);
      right = SATnormalNode(right);
      right = inverted ? SATnot(right) : right;

      j = node;

      if(result == 1){
	tmp = ALLOC(long,3);
	tmp[0] = left;
	tmp[1] = SATnot(j);
	size = 2;
      }
      else if(result == 2){
	tmp = ALLOC(long,3);
	tmp[0] = right;
	tmp[1] = SATnot(j);
	size = 2;
      }
      else if(result == 3){
	tmp = ALLOC(long,4);
	tmp[0] = SATnot(left);
	tmp[1] = SATnot(right);
	tmp[2] = j;
	size = 3;
      }
      else{
	printf("wrong returned result value, exit\n");
	exit(0);
      }

      lp = tmp;
      sat_BuildRT(cm,rm->root, lp, tmpIP,size,1);
      FREE(tmp);
    }
  }



  for(i=implied->num-1; i>=0; i--, space--) {
    v = *space;
    if(SATflags(v) & VisitedMask) {
      SATflags(v) &= ResetVisitedMask;
      --nMarked;

      if(nMarked == 0 && (!first || i==0))  {
	value = SATvalue(v);
	*fdaLit = v^(!value);
	sat_ArrayInsert(clauseArray, *fdaLit);
	break;
      }


      if(cm->option->coreGeneration){
	ante = SATante(v);
	if(ante==0){
	  if(!(st_lookup(cm->anteTable, (char *)SATnormalNode(v),&ante))){
	    printf("ante = 0 and is not in anteTable %ld\n",v);
	    exit(0);
	  }
	}

	/*build non-leaf node*/
	tmprt = RTCreateNode(rm);
	RT_pivot(tmprt) = SATnormalNode(v);
	RT_right(tmprt) = rm->root;
	rm->root = tmprt;

	if((SATflags(ante)&IsConflictMask)&&(SATflags(ante)&IsCNFMask)){
	  if(!st_lookup(cm->RTreeTable,(char*)ante,&tmprt)){
	    printf("RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
	    exit(0);
	  }
	  else{
	    RT_left(rm->root) = tmprt;
#if PR
	    printf("Get formula for CONFLICT CLAUSE:%d\n",ante);
#endif
	  }
	}
	else{ /* if not conflict CNF*/
	  /*left */
	  tmprt = RTCreateNode(rm);
	  RT_left(rm->root) = tmprt;
	  /*left is AIG*/
	  if(!(SATflags(ante) & IsCNFMask)){
	    /*generate formula for left*/
	    tmp = ALLOC(long,3);
	    value = SATvalue(v);
	    node = SATnormalNode(v);
	    node = value==1?node:SATnot(node);
	    tmp[0] = node;

	    size = 1;
	    if(ante != SATnormalNode(v)){
	      value = SATvalue(ante);
	      node = SATnormalNode(ante);
	      node = value==1?SATnot(node):node;
	      tmp[1] = node;
	      size++;
	      ante2 = SATante2(v);
	      if(ante2){
		value = SATvalue(ante2);
		node = SATnormalNode(ante2);
		node = value==1?SATnot(node):node;
		tmp[2] = node;
		size++;
	      }
	    }

	    lp = tmp;
	    sat_BuildRT(cm,tmprt,lp,tmpIP,size,1);
	    FREE(tmp);
	  }
	  /* left is CNF*/
	  else{

	    lp = (long*)SATfirstLit(ante);
	    size = SATnumLits(ante);
	    RT_fSize(tmprt) = size;
	    sat_BuildRT(cm,tmprt, lp, tmpIP,size,0);
	  }
	} /*else{ // if not conflict CNF*/

      }/*if(cm->option->coreGeneration){*/


      sat_MarkNodeInImpliedNode(
	      cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
    }
    first = 0;
  }

  sat_ResetFlagForClauseArray(cm, clauseArray);

  return;
}



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

  Synopsis    [ Minimize the literals of conflict clause]

  Description [ If the literal can be implied by other literals in
		conflict clause then we can delete it from conflict clause.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_MinimizeConflictClause(
	satManager_t *cm,
	satArray_t *clauseArray)
{
int i, j, size, all, tsize;
int inverted;
long v, tv;
long ante, ante2;
long *plit;
satArray_t *newArray;
satVariable_t *var;

  size = clauseArray->num;
  newArray = sat_ArrayAlloc(size);
  for(i=0; i<size; i++) {
    v = clauseArray->space[i];
    inverted = SATisInverted(v);
    v = SATnormalNode(v);

    ante = SATante(v);
    ante = SATnormalNode(ante);
    if(SATflags(ante) & IsCNFMask) {
      tsize = SATnumLits(ante);
      all = 1;
      for(j=0, plit=(long*)SATfirstLit(ante); j<tsize; j++, plit++) {
	tv = SATgetNode(*plit);
	tv = SATnormalNode(tv);
	if(tv == v)	continue;
	if(!(SATflags(tv) & NewMask)) {
	  all = 0;
	  break;
	}
      }
      if(all) {
	var = SATgetVariable(v);
	if(inverted)	(var->litsCount[1])++;
	else		(var->litsCount[0])++;
	continue;
      }
    }
    else {
      if(SATflags(ante) & NewMask) {
	ante2 = SATante2(v);
	ante2 = SATnormalNode(ante2);
	if((ante2==0) || (SATflags(ante2) & NewMask)) {
	  var = SATgetVariable(v);
	  if(inverted)	(var->litsCount[1])++;
	  else		(var->litsCount[0])++;
	  continue;
	}
      }
    }
    sat_ArrayInsert(newArray, v^inverted);
  }
  sat_ResetFlagForClauseArray(cm, clauseArray);
  memcpy(clauseArray->space, newArray->space, sizeof(long)*(newArray->num));
  clauseArray->num = newArray->num;
  sat_ArrayFree(newArray);
}

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

  Synopsis    [ Reset flags that are used to indentify conflict clause]

  Description [ Reset flags that are used to indentify conflict clause]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_ResetFlagForClauseArray(
	satManager_t *cm,
	satArray_t *clauseArray)
{
int size, i;
long v;

  size = clauseArray->num;
  for(i=0; i<size; i++) {
    v = clauseArray->space[i];
    v = SATnormalNode(v);
    SATflags(v) &= ResetNewVisitedMask;
  }
}

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

  Synopsis    [ Find seed for unique implication point analysis
		from conflicting clause]

  Description [ Find seed for unique implication point analysis
		from conflicting clause]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_MarkNodeInConflict(
	satManager_t *cm,
	satLevel_t *d,
	int *nMarked,
	int *objectFlag,
	int *bLevel,
	satArray_t *clauseArray)
{
satOption_t *option;

  option = cm->option;
  if(option->incTraceObjective == 0) {
    sat_MarkNodeInConflictClauseNoObj(
	cm, d, nMarked, objectFlag, bLevel, clauseArray);
  }
  else if(option->incTraceObjective == 1) { /* conservative */
    sat_MarkNodeInConflictClauseObjConservative(
	cm, d, nMarked, objectFlag, bLevel, clauseArray);
  }
}

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

  Synopsis    [ Traverse the antecedent to find unique implication point]

  Description [ Traverse the antecedent to find unique implication point]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_MarkNodeInImpliedNode(
	satManager_t *cm,
	satLevel_t *d,
	long v,
	int *nMarked,
	int *objectFlag,
	int *bLevel,
	satArray_t *clauseArray)
{
satOption_t *option;

  option = cm->option;
  if(option->incTraceObjective == 0) {
    sat_MarkNodeInImpliedNodeNoObj(
	cm, d, v, nMarked, objectFlag, bLevel, clauseArray);
  }
  else if(option->incTraceObjective == 1) { /* conservative */
    sat_MarkNodeInImpliedNodeObjConservative(
	cm, d, v, nMarked, objectFlag, bLevel, clauseArray);
  }
}

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

  Synopsis    [ If the node is implied in current level then mark it,
		otherwise add it to conflict clause]

  Description [ If the node is implied in current level then mark it,
		otherwise add it to conflict clause]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_MarkNodeSub(
	satManager_t *cm,
	long v,
	int *nMarked,
	int *bLevel,
	satLevel_t *d,
	satArray_t *clauseArray)
{
satLevel_t *td;
satOption_t *option;
int value;

  v = SATnormalNode(v);

  td = SATgetDecision(SATlevel(v));
  if(d == td) {
    if(!(SATflags(v) & VisitedMask)) {
      (*nMarked)++;
      SATflags(v) |= VisitedMask;
    }
  }
  else if(td->level < d->level) {
    if(!(SATflags(v) & NewMask)) {
      option = cm->option;
      if((td->level != 0) ||
	 (td->level == 0 && option->includeLevelZeroLiteral)) {
	SATflags(v) |= NewMask;
	value = SATvalue(v);
	sat_ArrayInsert(clauseArray, v^(!value));
	if(*bLevel < td->level)
	  *bLevel = td->level;
      }
    }
  }
  return;
}

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

  Synopsis    [ Traverse the antecedent to find unique implication point]

  Description [ Traverse the antecedent to find unique implication point]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_MarkNodeInImpliedNodeNoObj(
	satManager_t *cm,
	satLevel_t *d,
	long v,
	int *nMarked,
	int *oFlag,
	int *bLevel,
	satArray_t *clauseArray)
{
long ante, ante2, nv;
int inverted, size, i;
long *plit;
satOption_t *option;

  ante= SATante(v);
  /* Bing: UNSAT core generation */
  if(cm->option->coreGeneration){
    if(ante==0){
      if(!(st_lookup(cm->anteTable, (char *)(long)SATnormalNode(v), &ante))){
	printf("ante = 0 and is not in anteTable %ld\n",v);
	exit(0);
      }
    }
  }
  inverted = SATisInverted(ante);
  ante= SATnormalNode(ante);

  option = cm->option;
  if(SATflags(ante) & IsCNFMask) {
    SATconflictUsage(ante)++;
    size = SATnumLits(ante);
    for(i=0, plit=(long*)SATfirstLit(ante); i<size; i++, plit++) {
      nv = SATgetNode(*plit);
      if((int)(SATnormalNode(nv)) == v)	continue;
      sat_MarkNodeSub(cm, nv, nMarked, bLevel, d, clauseArray);
    }
  }
  else {
    /*Bing: very inmportant for level zero conflict analysis*/
    if(ante != SATnormalNode(v))
      sat_MarkNodeSub(cm, ante, nMarked, bLevel, d, clauseArray);

    ante2 = SATante2(v);
    if(ante2)
      sat_MarkNodeSub(cm, ante2, nMarked, bLevel, d, clauseArray);
  }
}


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

  Synopsis    [ Traverse the antecedent to find unique implication point]

  Description [ Traverse the antecedent to find unique implication point]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_MarkNodeInImpliedNodeObjConservative(
	satManager_t *cm,
	satLevel_t *d,
	long v,
	int *nMarked,
	int *oFlag,
	int *bLevel,
	satArray_t *clauseArray)
{
long ante, ante2, nv;
int inverted, size, i;
int objectFlag;
long *plit;
satOption_t *option;

  ante= SATante(v);
  /* Bing: UNSAT core generation */
  if(cm->option->coreGeneration){
    if(ante==0){
      if(!(st_lookup(cm->anteTable, (char *)SATnormalNode(v), &ante))){
	printf("ante = 0 and is not in anteTable %ld\n",v);
	exit(0);
      }
    }
  }
  inverted = SATisInverted(ante);
  ante= SATnormalNode(ante);

  objectFlag = 0;
  option = cm->option;
  if(SATflags(ante) & IsCNFMask) {
    SATconflictUsage(ante)++;
    size = SATnumLits(ante);
    for(i=0, plit=(long*)SATfirstLit(ante); i<size; i++, plit++) {
      nv = SATgetNode(*plit);
      nv = SATnormalNode(nv);
      if(nv == v)	continue;
      sat_MarkNodeSub(cm, nv, nMarked, bLevel, d, clauseArray);
    }
    objectFlag |= SATflags(ante) & ObjMask;
  }
  else {
    /*Bing: very inmportant for level zero conflict analysis*/
    if(ante != SATnormalNode(v))
      sat_MarkNodeSub(cm, ante, nMarked, bLevel, d, clauseArray);

    ante2 = SATante2(v);
    if(ante2) {
      ante2 = SATnormalNode(ante2);
      sat_MarkNodeSub(cm, ante2, nMarked, bLevel, d, clauseArray);
    }
  }
  *oFlag |= objectFlag;
}


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

  Synopsis    [ Find seed for unique implication point analysis
		from conflicting clause]

  Description [ Find seed for unique implication point analysis
		from conflicting clause]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_MarkNodeInConflictClauseNoObj(
	satManager_t *cm,
	satLevel_t *d,
	int *nMarked,
	int *oFlag,
	int *bLevel,
	satArray_t *clauseArray)
{
long conflict, left, right, nv;
int inverted, size, value, i;
long *plit;
satOption_t *option;

  conflict = d->conflict;
  inverted = SATisInverted(conflict);
  conflict = SATnormalNode(conflict);

  option = cm->option;
  if(SATflags(conflict) & IsCNFMask) {
    size = SATnumLits(conflict);
    for(i=0, plit=(long*)SATfirstLit(conflict); i<size; i++, plit++) {
      nv = SATgetNode(*plit);
      sat_MarkNodeSub(cm, nv, nMarked, bLevel, d, clauseArray);
    }
  }
  else {
    value = SATvalue(conflict);
    if(value == 1) {
      sat_MarkNodeSub(cm, conflict, nMarked, bLevel, d, clauseArray);

      left = SATleftChild(conflict);
      inverted = SATisInverted(left);
      left = SATnormalNode(left);
      value = SATvalue(left) ^ inverted;
      if(value == 0) {
	sat_MarkNodeSub(cm, left, nMarked, bLevel, d, clauseArray);
	return;
      }

      right = SATrightChild(conflict);
      inverted = SATisInverted(right);
      right = SATnormalNode(right);
      value = SATvalue(right) ^ inverted;
      if(value == 0) {
	sat_MarkNodeSub(cm, right, nMarked, bLevel, d, clauseArray);
	return;
      }
    }
    else if(value == 0) {
      left = SATleftChild(conflict);
      right = SATrightChild(conflict);
      sat_MarkNodeSub(cm, conflict, nMarked, bLevel, d, clauseArray);
      sat_MarkNodeSub(cm, left, nMarked, bLevel, d, clauseArray);
      sat_MarkNodeSub(cm, right, nMarked, bLevel, d, clauseArray);
    }
  }
}

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

  Synopsis    [ Find seed for unique implication point analysis
		from conflicting clause]

  Description [ Find seed for unique implication point analysis
		from conflicting clause]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_MarkNodeInConflictClauseObjConservative(
	satManager_t *cm,
	satLevel_t *d,
	int *nMarked,
	int *oFlag,
	int *bLevel,
	satArray_t *clauseArray)
{
long conflict, left, right, nv;
int inverted, size, value, i;
long *plit;
satOption_t *option;

  conflict = d->conflict;
  inverted = SATisInverted(conflict);
  conflict = SATnormalNode(conflict);

  option = cm->option;
  if(SATflags(conflict) & IsCNFMask) {
    size = SATnumLits(conflict);
    for(i=0, plit=(long*)SATfirstLit(conflict); i<size; i++, plit++) {
      nv = SATgetNode(*plit);
      *oFlag |= (SATflags(nv) & ObjMask);
      sat_MarkNodeSub(cm, nv, nMarked, bLevel, d, clauseArray);
    }
  }
  else {
    value = SATvalue(conflict);
    if(value == 1) {
      *oFlag |= (SATflags(conflict) & ObjMask);
      sat_MarkNodeSub(cm, conflict, nMarked, bLevel, d, clauseArray);

      left = SATleftChild(conflict);
      inverted = SATisInverted(left);
      left = SATnormalNode(left);
      value = SATvalue(left) ^ inverted;
      if(value == 0) {
	*oFlag |= (SATflags(left) & ObjMask);
	sat_MarkNodeSub(cm, left, nMarked, bLevel, d, clauseArray);
	return;
      }

      right = SATrightChild(conflict);
      inverted = SATisInverted(right);
      right = SATnormalNode(right);
      value = SATvalue(right) ^ inverted;
      if(value == 0) {
	*oFlag |= (SATflags(right) & ObjMask);
	sat_MarkNodeSub(cm, right, nMarked, bLevel, d, clauseArray);
	return;
      }
    }
    else if(value == 0) {
      *oFlag |= (SATflags(conflict) & ObjMask);

      left = SATleftChild(conflict);
      inverted = SATisInverted(left);
      left = SATnormalNode(left);
      *oFlag |= (SATflags(left) & ObjMask);

      right = SATrightChild(conflict);
      inverted = SATisInverted(right);
      right = SATnormalNode(right);
      *oFlag |= (SATflags(right) & ObjMask);

      sat_MarkNodeSub(cm, conflict, nMarked, bLevel, d, clauseArray);
      sat_MarkNodeSub(cm, left, nMarked, bLevel, d, clauseArray);
      sat_MarkNodeSub(cm, right, nMarked, bLevel, d, clauseArray);
    }
  }
}


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

  Synopsis    [ Backtrack to given decision level ]

  Description [ Backtrack to given decision level ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_Backtrack(
	satManager_t *cm,
	int level)
{
satLevel_t *d;

/*Bing*/
 if(cm->option->ForceFinish == 0)
   if(level < 0)	return;

  d = SATgetDecision(cm->currentDecision);
  while(1) {
    if(d->level <= level)
      break;

    sat_Undo(cm, d);
    cm->currentDecision--;
    if(cm->currentDecision == -1)
      break;
    d = SATgetDecision(cm->currentDecision);
  }
  return;
}


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

  Synopsis    [ Undo implication]

  Description [ Undo implication]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_Undo(
	satManager_t *cm,
	satLevel_t *d)
{
satArray_t *implied, *satisfied;
satVariable_t *var;
int size, i;
long *space, v;

  implied = d->implied;
  space = implied->space;
  size = implied->num;
  for(i=0; i<size; i++, space++) {
    v = *space;

    SATvalue(v) = 2;
    SATflags(v) &= ResetNewVisitedObjInQueueMask;
    var = &(cm->variableArray[SATnodeID(v)]);
    var->antecedent = 0;
    var->antecedent2 = 0;
    var->level = -1;
    var->depth = 0;
  }

  cm->implicatedSoFar -= size;

  if(d->satisfied) {
    satisfied = d->implied;
    space = satisfied->space;
    size = satisfied->num;
    for(i=0; i<size; i++, space++) {
      v = *space;

      SATflags(v) &= ResetBDDSatisfiedMask;
    }
    d->satisfied->num = 0;
  }
  if(d->level > 0) {
    if((cm->decisionHead[d->level-1]).currentVarPos < cm->currentVarPos)
      cm->currentVarPos = (cm->decisionHead[d->level-1]).currentVarPos;
  }
  else
    cm->currentVarPos = d->currentVarPos;

  d->implied->num = 0;
  d->currentVarPos = 0;
  d->conflict = 0;


}

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

  Synopsis    [ Compare decision level of variable ]

  Description [ Compare decision level of variable ]

  SideEffects []

  SeeAlso     []

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

static int
levelCompare(
  const void * node1,
  const void * node2)
{
  long v1, v2;
  int l1, l2;

  v1 = *(int *)(node1);
  v2 = *(int *)(node2);
  l1 = SATcm->variableArray[SATnodeID(v1)].level;
  l2 = SATcm->variableArray[SATnodeID(v2)].level;

  if(l1 == l2)	return(v1 > v2);
  return (l1 > l2);
}