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

  FileName    [satDecision.c]

  PackageName [sat]

  Synopsis    [Routines for various decision heuristics.]

  Author      [HoonSang Jin]

  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"

static char rcsid[] UNUSED = "$Id: satDecision.c,v 1.28 2009/04/11 18:26:37 fabio Exp $";
static	satManager_t *SatCm;

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

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

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

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

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


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


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

  Synopsis    [ Select decision variable]

  Description [ Select decision variable]

  SideEffects []

  SeeAlso     []

******************************************************************************/
satLevel_t *
sat_MakeDecision(satManager_t *cm)
{
satLevel_t *d;
int value;
long v;
satStatistics_t *stats;

  d = SATgetDecision(cm->currentDecision);

  if(cm->queue->size)
    return(d);

  d = sat_AllocLevel(cm);

  v = 0;
  v = sat_DecisionBasedOnBDD(cm, d);

  if(v == 0)
    v = sat_DecisionBasedOnLatestConflict(cm, d);

  if(v == 0)
    v = sat_DecisionBasedOnScore(cm, d);

  if(v == 0)
    return(0);


  stats = cm->each;

  stats->nDecisions++;

  value = !(SATisInverted(v));
  v = SATnormalNode(v);
  d->decisionNode = v;
  d->nConflict = cm->each->nConflictCl;

  SATvalue(v) = value;
  /**
  if(cm->option->verbose > 1) {
    var = SATgetVariable(v);
    fprintf(cm->stdOut, "decision at %3d on %6d <- %d score(%d %d) %d\n",
	    d->level, v, value, var->scores[0], var->scores[1],
	    cm->each->nDecisions);
    fflush(cm->stdOut);
  }
  **/
  SATmakeImplied(v, d);

  sat_Enqueue(cm->queue, v);
  SATflags(v) |= InQueueMask;

  return(d);
}


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

  Synopsis    [ Decision making based on current top clause ]

  Description [ Decision making based on current top clause ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
long
sat_DecisionBasedOnLatestConflict(
	satManager_t *cm,
	satLevel_t *d)
{
satOption_t *option;
satStatistics_t *stats;
satLiteralDB_t *literals;
satVariable_t *var;
int size, limit;
long *plit, *tplit;
long v, lit, tv, maxV;
int tsize, count;
int inverted, value;
int i, j, satisfied;
int tmpScore, maxScore;

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

  if(!(option->decisionHeuristic & LATEST_CONFLICT_DECISION))
    return(0);

  /** CONSIDER
  if(stats->nConflictCl < option->minConflictForDecision)
    return(0);

  **/


  if(cm->currentTopConflict == 0)
    return(0);

  literals = cm->literals;
  size = literals->last - literals->begin;

  limit = MAXINT;
  if(option->maxConflictForDecision > 0)
    limit = option->maxConflictForDecision;

  count = cm->currentTopConflictCount;
  tv = -(*(cm->currentTopConflict));
  tsize = SATnumLits(tv);
  tplit = (long*)SATfirstLit(tv);
  plit = tplit + tsize;

  for(i=plit-literals->begin; i>=0; i--, plit--) {
/**  for(plit =literals->last-1, i=literals->last - literals->begin; i>=0; i--, plit--) { */
    if(count > limit)	break;

    lit = *plit;
    if(lit < 0) {
      tv = -lit;

      if(!(SATflags(tv) & IsConflictMask))
	return(0);

      if(plit < (long*)SATfirstLit(tv))
	continue;

      count++;

      if(option->skipSatisfiedClauseForDecision) {
	tsize = SATnumLits(tv);
	tplit = (long *)SATfirstLit(tv);
	satisfied = 0;
	maxScore = -1;
	maxV = 0;
	for(j=0; j<tsize; j++, tplit++) {
	  v = SATgetNode(*tplit);
	  inverted = SATisInverted(v);
	  v = SATnormalNode(v);
	  value = SATvalue(v) ^ inverted;
	  if(value == 1) {
	    satisfied = 1;
	    break;
	  }
	  else if(value == 0) {
	    continue;
	  }
	  var = SATgetVariable(v);
	  tmpScore = (var->scores[0] >= var->scores[1]) ? var->scores[0] : var->scores[1];
	  if(tmpScore > maxScore) {
	    maxScore = tmpScore;
	    maxV = v;
	  }
	}
	if(satisfied) {
	  i = i - tsize - 1;
	  plit = plit - tsize -1;
	}
	else {
	  var = SATgetVariable(maxV);
	  value = (var->scores[0] >= var->scores[1]) ? 0 : 1;

	  cm->currentTopConflict = (long*)SATfirstLit(tv) + SATnumLits(tv);
	  cm->currentTopConflictCount = count;

	  stats = cm->each;
	  stats->nLatestConflictDecisions++;
	  return(maxV ^ !value);
	}
      }
      continue;
    }
    else if(lit == 0)
      continue;

    v = SATgetNode(lit);
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    value = SATvalue(v) ^ inverted;

    if(value >= 2) {
      var = SATgetVariable(v);
      value = (var->conflictLits[0] >= var->conflictLits[1]) ? 0 : 1;

      cm->currentTopConflict = (long*)SATfirstLit(tv) + SATnumLits(tv);
      cm->currentTopConflictCount = count;

      stats = cm->each;
      stats->nLatestConflictDecisions++;
      return(v ^ !value);
    }
  }
  return(0);
}

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

  Synopsis    [ Check decision variable to check correctness of currentVarPos,
		since currentVarPos has to point lowest variable that are
		not implied.]

  Description [ Check decision variable to check correctness of currentVarPos,
		since currentVarPos has to point lowest variable that are
		not implied.]

  SideEffects []

  SeeAlso     []

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

  orderedVariableArray = cm->orderedVariableArray;
  size = orderedVariableArray->num;
  for(i=0; i<cm->currentVarPos; i++) {
    v = orderedVariableArray->space[i];
    if(SATvalue(v) > 1)	{
      fprintf(stdout, " ERROR : wrong current variable pos %d at %d\n",
	      cm->currentVarPos, i);
    }
  }
}

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

  Synopsis    [ Decision making based on score based heuristic ]

  Description [ Decision making based on score based heuristic ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
long
sat_DecisionBasedOnScore(
	satManager_t *cm,
	satLevel_t *d)
{
int size, i;
long v;
int value;
satVariable_t *var;
satArray_t *orderedVariableArray;
satStatistics_t *stats;
satOption_t *option;


  option = cm->option;
  orderedVariableArray = cm->orderedVariableArray;
  size = orderedVariableArray->num;

  for(i=cm->currentVarPos; i<size; i++) {
    v = orderedVariableArray->space[i];
    if(SATvalue(v) < 2)	continue;

    var = SATgetVariable(v);
    value = (var->scores[0] >= var->scores[1]) ? 0 : 1;

    stats = cm->each;
    if((var->scores[0]+var->scores[1]) < 1) {
      stats->nLowScoreDecisions++;
    }


    if((option->decisionHeuristic & DVH_DECISION))
      stats->nDVHDecisions++;
    else
      stats->nVSIDSDecisions++;

    cm->currentVarPos = i;
    d->currentVarPos = i;

    return(v ^ !value);
  }

  return(0);
}

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

  Synopsis    [ Take care of decision by BDD based mathod ]

  Description [ Take care of decision by BDD based mathod ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
long
sat_DecisionBasedOnBDD(
	satManager_t *cm,
	satLevel_t *d)
{
satArray_t *arr;
long nv, v;

  if(cm->assignByBDD == 0)
    return(0);

  arr = cm->assignByBDD;
  if(arr->num == 0)
    return(0);

  /**
  for(i=0; i<arr->num; i++) {
    v = arr->space[i];
    nv = SATnormalNode(v);
    if(SATvalue(nv) > 1)
      return(v);
  }
  **/

  while(arr->num) {
    v = arr->space[arr->num-1];
    nv = SATnormalNode(v);
    arr->num--;
    if(SATvalue(nv) > 1)
      return(v);
  }
  return(0);
}


long
sat_DecisionBasedOnShrink(
	satManager_t *cm)
{
satArray_t *arr;
long nv, v;

  if(cm->shrinkArray == 0)
    return(0);

  arr = cm->shrinkArray;
  if(arr->num == 0)
    return(0);

  while(arr->num) {
    v = arr->space[arr->num-1];
    nv = SATnormalNode(v);
    arr->num--;
    if(SATvalue(nv) > 1)
      return(v);
  }
  return(0);
}


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

  Synopsis    [ Update the score of variables ]

  Description [ Update the score of variables ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_UpdateScore(
	satManager_t *cm)
{
satArray_t *one, *tmp;
satArray_t *ordered;
satVariable_t *var;
int size, i;
long v;
int value;

  ordered = cm->orderedVariableArray;

  one = sat_ArrayAlloc(ordered->num);
  tmp = sat_ArrayAlloc(ordered->num);

  size = ordered->num;
  for(i=0; i<size; i++) {
    v = ordered->space[i];

    if(SATvalue(v) < 2 && SATlevel(v) == 0)
      continue;

    var = SATgetVariable(v);
    var->scores[0] = (var->scores[0]>>1) + var->litsCount[0] - var->lastLitsCount[0];
    var->scores[1] = (var->scores[1]>>1) + var->litsCount[1] - var->lastLitsCount[1];
    var->lastLitsCount[0] = var->litsCount[0];
    var->lastLitsCount[1] = var->litsCount[1];


    if((var->scores[0] + var->scores[1]) < 1) {
      sat_ArrayInsert(one, v);
    }
    else {
      value = (var->scores[0] > var->scores[1]) ? var->scores[0] : var->scores[1];
      sat_ArrayInsert(tmp, v);
      sat_ArrayInsert(tmp, value);
    }
  }

  SatCm = cm;
  qsort(tmp->space, (tmp->num)>>1, sizeof(long)*2, ScoreCompare);

  ordered->num = 0;
  size = tmp->num;
  for(i=0; i<size; i++) {
    v = tmp->space[i];
    sat_ArrayInsert(ordered, v);
    var = SATgetVariable(v);
    var->pos = (i>>1);
    i++;
  }

  size = one->num;
  for(i=0; i<size; i++) {
    v = one->space[i];
    var = SATgetVariable(v);
    var->pos = ordered->num;
    sat_ArrayInsert(ordered, v);
  }

  sat_ArrayFree(one);
  sat_ArrayFree(tmp);

  cm->orderedVariableArray = ordered;
  cm->currentVarPos = 0;

  for(i=1; i<cm->currentDecision; i++) {
    cm->decisionHead[i].currentVarPos = 0;
  }

  if(cm->option->verbose > 3)
    sat_PrintScore(cm);

}


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

  Synopsis    [ Update the score of variables by deepest variable hike]

  Description [ Update the score of variables by deepest variable hike]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_UpdateDVH(
	satManager_t *cm,
	satLevel_t *d,
	satArray_t *clauseArray,
	int bLevel,
	long unitLit)
{
satArray_t *ordered;
satLevel_t *td;
satVariable_t *var, *tvar, *ttvar;
int score, tscore, ttscore;
int value;
long v;
int gap, i, insert;


  ordered = cm->orderedVariableArray;

  unitLit = SATnormalNode(unitLit);
  gap = cm->currentDecision - bLevel;
  td = SATgetDecision(bLevel+1);

  if(gap <= 1) {
      /** CONSIDER .... */
  }
  var = SATgetVariable(unitLit);
  tvar = SATgetVariable(td->decisionNode);

  score = (var->scores[1] > var->scores[0]) ? var->scores[1] : var->scores[0];
  tscore = (tvar->scores[1] > tvar->scores[0]) ? tvar->scores[1] : tvar->scores[0];

  if(score >= tscore)	{
    return;
  }

  tscore += 1;

  value = SATvalue(unitLit);
  if(value == 0)var->scores[1] = tscore;
  else		var->scores[0] = tscore;

  ordered = cm->orderedVariableArray;
  insert = 0;
  for(i=var->pos; i>=1; i--) {
    v = ordered->space[i-1];
    ttvar = SATgetVariable(v);
    ttscore = (ttvar->scores[1] > ttvar->scores[0]) ? ttvar->scores[1] : ttvar->scores[0];
    if(tscore > ttscore && i>1) {
      ttvar->pos = i;
      ordered->space[i] = v;
      continue;
    }

    var->pos = i;
    ordered->space[i] = unitLit;
    insert = 1;
    break;
  }

  if(insert == 0) {
    var->pos = i;
    ordered->space[0] = unitLit;
  }

  for(i=d->level; i>0; i--) {
    td = SATgetDecision(i);
    if(td->currentVarPos < var->pos)
      break;
    td->currentVarPos = var->pos;
  }
  cm->currentVarPos = td->currentVarPos;

}

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

  Synopsis    [ Check correctness of variable order ]

  Description [ Check correctness of variable order ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_CheckOrderedVariableArray(satManager_t *cm)
{
satArray_t *ordered;
satVariable_t *var;
int i;
long v;

  ordered = cm->orderedVariableArray;
  for(i=0; i<ordered->num; i++) {
    v = ordered->space[i];
    var = SATgetVariable(v);
    if(i != var->pos) {
      fprintf(cm->stdOut, "Error : wrong variable position %d %d in ordered array\n", i, var->pos);

    }
  }
}

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

  Synopsis    [ Generate initial score ]

  Description [ Generate initial score ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_InitScore(satManager_t *cm)
{
int objExist;
int j, inverted;
long *plit, v, nv, i;
int size;
int count0, count1;
satArray_t *ordered, *newOrdered;
satVariable_t *var;

  ordered = cm->orderedVariableArray;
  if(ordered == 0)
    ordered = sat_ArrayAlloc(cm->initNumVariables);
  else
    ordered->num = 0;
  cm->orderedVariableArray = ordered;

  objExist = 0;
  /**
  if(cm->obj && cm->obj->num) {
    sat_MarkTransitiveFaninForArray(cm, cm->obj, VisitedMask);
    objExist = 1;
  }
  **/


  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    v = i;
    if((SATflags(v) & IsBDDMask)) {
      continue;
    }
    if((SATflags(v) & IsCNFMask)) {
      size = SATnumLits(v);
      plit = (long*)SATfirstLit(v);
      for(j=0; j<size; j++, plit++) {
	nv = SATgetNode(*plit);
	inverted = !(SATisInverted(nv));
	nv = SATnormalNode(nv);
	var = SATgetVariable(nv);
	var->litsCount[inverted]++;
      }
      continue;
    }
    if(!(SATflags(v) & CoiMask))	continue;
    if(!(SATflags(v) & VisitedMask) && objExist)	continue;

    if(SATvalue(v) != 2 && SATlevel(v) == 0)	continue;

    count0 = count1 = SATnFanout(v);
    if(count0 == 0 && SATleftChild(v) == 2 && SATrightChild(v) == 2) {
      count0 = 0;
      count1 = 0;
    }
    else if(SATleftChild(v) != 2) {
      count0 += 2;
      count1++;
    }
    else {
      count0 += 3;
      count1 += 3;
    }

    var = SATgetVariable(v);
    var->litsCount[0] += count0;
    var->litsCount[1] += count1;

    sat_ArrayInsert(ordered, v);
  }

  //Bing:
  if(cm->unitLits){
    for(i=0; i<cm->unitLits->num; i++) {
      v = cm->unitLits->space[i];
      v = SATnormalNode(v);
      SATflags(v) |= NewMask;
    }
  }

  if(cm->assertion) {
    for(i=0; i<cm->assertion->num; i++) {
      v = cm->assertion->space[i];
      v = SATnormalNode(v);
      SATflags(v) |= NewMask;
    }
  }

  newOrdered = sat_ArrayAlloc((ordered->num) * 2);
  size = ordered->num;
  for(i=0; i<size; i++) {
    v = ordered->space[i];
    var = SATgetVariable(v);
    var->scores[0] = var->lastLitsCount[0] = var->litsCount[0];
    var->scores[1] = var->lastLitsCount[1] = var->litsCount[1];

    if(SATflags(v) & NewMask);
    else if(var->scores[0] == 0 && var->scores[1] == 0 && !(SATflags(v) & NewMask)) {
      sat_ArrayInsert(cm->pureLits, (v));
    }
    else if(var->scores[0] == 0 && !(SATflags(v) & NewMask)) {
      sat_ArrayInsert(cm->pureLits, (v));
    }
    else if(var->scores[1] == 0 && !(SATflags(v) & NewMask)) {
      sat_ArrayInsert(cm->pureLits, SATnot(v));
    }
    else {
      sat_ArrayInsert(newOrdered, v);
      sat_ArrayInsert(newOrdered, (var->scores[0] > var->scores[1]) ? var->scores[0] : var->scores[1]);
    }
  }

  //Bing:
  if(cm->unitLits){
    for(i=0; i<cm->unitLits->num; i++) {
      v = cm->unitLits->space[i];
      v = SATnormalNode(v);
      SATflags(v) &= ResetNewMask;
    }
  }

  if(cm->assertion) {
    for(i=0; i<cm->assertion->num; i++) {
      v = cm->assertion->space[i];
      v = SATnormalNode(v);
      SATflags(v) &= ResetNewMask;
    }
  }

  cm->orderedVariableArray = ordered;
  size = newOrdered->num;
  qsort(newOrdered->space, size>>1, sizeof(long)*2, ScoreCompare);

  cm->currentVarPos = 0;
  ordered->num = 0;
  for(i=0; i<size; i++) {
    v = newOrdered->space[i];
    var = SATgetVariable(v);
    var->pos = (i>>1);
    sat_ArrayInsert(ordered, v);
    i++;
  }

  sat_ArrayFree(newOrdered);

  /**
  if(cm->obj && cm->obj->num) {
    sat_UnmarkTransitiveFaninForArray(
	    cm, cm->obj, VisitedMask, ResetVisitedMask);
  }
  **/

  if(cm->option->verbose > 3)
    sat_PrintScore(cm);
}

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

  Synopsis    [ Generate initial score for CNF and AIG ]

  Description [ Generate initial score for CNF and AIG]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_InitScoreForMixed(satManager_t *cm)
{
int j, inverted;
long *plit, v, nv, i;
int size;
int count0, count1;
satArray_t *ordered, *newOrdered;
satVariable_t *var;

  ordered = cm->orderedVariableArray;
  if(ordered == 0)
    ordered = sat_ArrayAlloc(cm->initNumVariables);
  else
    ordered->num = 0;
  cm->orderedVariableArray = ordered;

  /**
  objExist = 0;
  if(cm->obj && cm->obj->num) {
    sat_MarkTransitiveFaninForArray(cm, cm->obj, VisitedMask);
    objExist = 1;
  }
  **/


  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    v = i;
    if((SATflags(v) & IsBDDMask)) {
      continue;
    }
    if((SATflags(v) & IsCNFMask)) {
      size = SATnumLits(v);
      plit =(long*) SATfirstLit(v);
      for(j=0; j<size; j++, plit++) {
	nv = SATgetNode(*plit);
	inverted = !(SATisInverted(nv));
	nv = SATnormalNode(nv);
	var = SATgetVariable(nv);
	var->litsCount[inverted]++;
      }
      continue;
    }
    if(!(SATflags(v) & CoiMask))	continue;
    /**
    if(!(SATflags(v) & VisitedMask) && objExist)	continue;
    **/

    if(SATvalue(v) != 2 && SATlevel(v) == 0)	continue;

    count0 = count1 = SATnFanout(v);
    if(count0 == 0 && SATleftChild(v) == 2 && SATrightChild(v) == 2) {
      count0 = 0;
      count1 = 0;
    }
    else if(SATleftChild(v) != 2) {
      count0 += 2;
      count1++;
    }
    else {
      count0 += 3;
      count1 += 3;
    }

    var = SATgetVariable(v);
    var->litsCount[0] += count0;
    var->litsCount[1] += count1;

    sat_ArrayInsert(ordered, v);
  }

  for(i=0; i<cm->unitLits->num; i++) {
    v = cm->unitLits->space[i];
    v = SATnormalNode(v);
    SATflags(v) |= NewMask;
  }
  if(cm->assertion) {
    for(i=0; i<cm->assertion->num; i++) {
      v = cm->assertion->space[i];
      v = SATnormalNode(v);
      SATflags(v) |= NewMask;
    }
  }

  newOrdered = sat_ArrayAlloc((ordered->num) * 2);
  size = ordered->num;
  for(i=0; i<size; i++) {
    v = ordered->space[i];
    var = SATgetVariable(v);
    var->scores[0] = var->lastLitsCount[0] = var->litsCount[0];
    var->scores[1] = var->lastLitsCount[1] = var->litsCount[1];

    if(SATflags(v) & NewMask);
    else if(var->scores[0] == 0 && var->scores[1] == 0 && !(SATflags(v) & NewMask)) {
      sat_ArrayInsert(cm->pureLits, (v));
    }
    else if(var->scores[0] == 0 && !(SATflags(v) & NewMask)) {
      sat_ArrayInsert(cm->pureLits, (v));
    }
    else if(var->scores[1] == 0 && !(SATflags(v) & NewMask)) {
      sat_ArrayInsert(cm->pureLits, SATnot(v));
    }
    else {
      sat_ArrayInsert(newOrdered, v);
      sat_ArrayInsert(newOrdered, (var->scores[0] > var->scores[1]) ? var->scores[0] : var->scores[1]);
    }
  }

  for(i=0; i<cm->unitLits->num; i++) {
    v = cm->unitLits->space[i];
    v = SATnormalNode(v);
    SATflags(v) &= ResetNewMask;
  }
  if(cm->assertion) {
    for(i=0; i<cm->assertion->num; i++) {
      v = cm->assertion->space[i];
      v = SATnormalNode(v);
      SATflags(v) &= ResetNewMask;
    }
  }

  cm->orderedVariableArray = ordered;
  size = newOrdered->num;
  qsort(newOrdered->space, size>>1, sizeof(long)*2, ScoreCompare);

  cm->currentVarPos = 0;
  ordered->num = 0;
  for(i=0; i<size; i++) {
    v = newOrdered->space[i];
    var = SATgetVariable(v);
    var->pos = (i>>1);
    sat_ArrayInsert(ordered, v);
    i++;
  }

  sat_ArrayFree(newOrdered);

  /**
  if(cm->obj && cm->obj->num) {
    sat_UnmarkTransitiveFaninForArray(
	    cm, cm->obj, VisitedMask, ResetVisitedMask);
  }
  **/

  if(cm->option->verbose > 3)
    sat_PrintScore(cm);

}
/**Function********************************************************************

  Synopsis    [ Compare score to sort variable array]

  Description [ Compare score to sort variable array]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
ScoreCompare(
  const void * node1,
  const void * node2)
{
int v1;
int v2;
int s1, s2;

  v1 = *(int *)(node1);
  v2 = *(int *)(node2);
  s1 = *((int *)(node1) + 1);
  s2 = *((int *)(node2) + 1);
  /**
  var1 = SatCm->variableArray[SATnodeID(v1)];
  var2 = SatCm->variableArray[SATnodeID(v2)];
  s1 = (var1.scores[0] > var1.scores[1]) ? var1.scores[0] : var1.scores[1];
  s2 = (var2.scores[0] > var2.scores[1]) ? var2.scores[0] : var2.scores[1];
  **/
  if(s1 == s2) {
    return(v1 > v2);
  }
  return(s1 < s2);
}