src/sat/satConflict.c

Go to the documentation of this file.

#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                                                     */
/*---------------------------------------------------------------------------*/

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

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

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


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

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

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

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

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 */
    /* 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);
}

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

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

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


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

}


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

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

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;

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

      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;

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

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

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



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

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

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

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

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

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


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


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

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


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


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;


}

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