src/sat/satDecision.c

Go to the documentation of this file.

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

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

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

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


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;
  SATmakeImplied(v, d);

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

  return(d);
}


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

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

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

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

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

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


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

}


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

}

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

    }
  }
}

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;
  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->option->verbose > 3)
    sat_PrintScore(cm);
}

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;

  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(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->option->verbose > 3)
    sat_PrintScore(cm);

}
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);
  if(s1 == s2) {
    return(v1 > v2);
  }
  return(s1 < s2);
}