src/sat/satInc.c

Go to the documentation of this file.

#include "satInt.h"

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

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

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

static int ScoreDistillCompare(const void *x, const void *y);

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


void
sat_IncrementalUsingDistill(satManager_t *cm)
{
  sat_TrieBasedImplication(cm, cm->trieArray, 1);
  sat_FreeTrie(cm, cm->trieArray);
  cm->trieArray = 0;
  fprintf(cm->stdOut, "%s %d conflicts are forwarded from distillation,\n",
          cm->comment,
          cm->each->nDistillObjConflictCl + cm->each->nDistillNonobjConflictCl);
}

satLevel_t *
sat_DecisionBasedOnTrie(
        satManager_t *cm,
        long v,
        int value)
{
satLevel_t *d;

  d = sat_AllocLevel(cm);
  d->decisionNode = v;

  SATvalue(v) = value;
  SATmakeImplied(v, d);

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

  return(d);
}

void
sat_TrieBasedImplication(
        satManager_t *cm,
        satArray_t *trieArray,
        int depth)
{
int i;
satTrie_t *t;
satLevel_t *d;
satArray_t *tArray;

  if(trieArray == 0)    return;

  for(i=0; i<trieArray->num; i++) {
    t = (satTrie_t *)(trieArray->space[i]);
    if(SATvalue(t->id) < 2)     continue;

    tArray = t->child[0];
    if(tArray) {
      d = sat_DecisionBasedOnTrie(cm, t->id, 0);
      sat_ImplicationMain(cm, d);
      if(d->conflict) {
        sat_ConflictAnalysisOnTrie(cm, d);
      }
      else if(cm->status == 0) {
        sat_TrieBasedImplication(cm, tArray, depth+1);
      }
      sat_Backtrack(cm, depth-1);
    }

    tArray = t->child[1];
    if(tArray && cm->status == 0) {
      d = sat_DecisionBasedOnTrie(cm, t->id, 1);
      sat_ImplicationMain(cm, d);
      if(d->conflict) {
        sat_ConflictAnalysisOnTrie(cm, d);
      }
      else if(cm->status == 0) {
        sat_TrieBasedImplication(cm, tArray, depth+1);
      }
      sat_Backtrack(cm, depth-1);
    }

    if(cm->status == SAT_BACKTRACK && depth == 1) {
      cm->status = 0;
      d = SATgetDecision(0);
      sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
      sat_ImplyArray(cm, d, cm->objUnitLitArray);
      sat_MarkObjectiveFlagToArray(cm, cm->objUnitLitArray);
      sat_ImplicationMain(cm, d);
      if(d->conflict) {
        cm->status = SAT_UNSAT;
        return;
      }
      i--;
    }
  }
}

void
sat_ConflictAnalysisOnTrie(
        satManager_t *cm,
        satLevel_t *d)
{
int bLevel;
long v, learned, unitLit;
int objectFlag;
satArray_t *clauseArray;
satStatistics_t *stats;

  bLevel = 0;
  unitLit = -1;
  clauseArray = cm->auxArray;
  sat_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &unitLit);

  if(clauseArray->num > (int)(cm->currentDecision*2)) {
    sat_GetConflictAsConflictClause(cm, clauseArray);
  }

  if(clauseArray->num == 1) {
    cm->status = SAT_BACKTRACK;
    v = clauseArray->space[0];
    if(objectFlag)
      sat_ArrayInsert(cm->objUnitLitArray, SATnot(v));
    else
      sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(v));
  }
  else {
    learned = sat_AddClauseIncremental(cm, clauseArray, objectFlag, 1);
  }

  stats = cm->each;
  if(objectFlag) {
    stats->nInitObjConflictCl++;
    stats->nInitObjConflictLit += clauseArray->num;
    stats->nObjConflictCl++;
    stats->nObjConflictLit += clauseArray->num;
    stats->nDistillObjConflictCl++;
    stats->nDistillObjConflictLit += clauseArray->num;
  }
  else {
    stats->nInitNonobjConflictCl++;
    stats->nInitNonobjConflictLit += clauseArray->num;
    stats->nObjConflictCl++;
    stats->nObjConflictLit += clauseArray->num;
    stats->nDistillNonobjConflictCl++;
    stats->nDistillNonobjConflictLit += clauseArray->num;
  }
  stats->nConflictCl++;
  stats->nConflictLit += clauseArray->num;
}

void
sat_GetConflictAsConflictClause(
        satManager_t *cm,
        satArray_t *clauseArray)
{
int i;
satLevel_t *d;

  clauseArray->num = 0;
  for(i=1; i<=cm->currentDecision; i++) {
    d = SATgetDecision(i);
    sat_ArrayInsert(clauseArray,
            (d->decisionNode)^(!(SATvalue(d->decisionNode))));
  }
}

void
sat_RestoreForwardedClauses(satManager_t *cm, int objectFlag)
{
int i, size;
int total;
long *space, c, *start;
satArray_t *saved;
satArray_t *clause;
//Bing
 int NotCoi = 0, ct=0;


  if(cm->option->checkNonobjForwarding) {
    sat_CheckForwardedClauses(cm);
  }

  saved = cm->savedConflictClauses;
  if(saved == 0)
    return;

  clause = sat_ArrayAlloc(50);

  total = 0;
  for(i=0, space=saved->space; i<saved->num; i++, space++){
    if(*space < 0) {
      space++;
      i++;
      start = space;
      size = 0;
      clause->num = 0;
      //Bing:
      NotCoi = 0;
      while(*space > 0) {
        sat_ArrayInsert(clause, SATnot((*space)));
        //Bing:
        if(!(SATflags(*space)&CoiMask)){
          NotCoi = 1;
        }
        size++;
        i++;
        space++;
      }


      //Bing:
      if(cm->option->AbRf){
        if(!NotCoi){
          c = sat_AddClauseIncremental(cm, clause, objectFlag, 0);
          total++;
        }
        else
          ct++;
      }
      else{
        c = sat_AddClauseIncremental(cm, clause, objectFlag, 0);
        total++;
      }
    }
  }
  sat_ArrayFree(clause);
  sat_ArrayFree(saved);
  cm->savedConflictClauses = 0;

}

void
sat_CheckForwardedClauses(satManager_t *cm)
{
long *space, *start;
long nv;
int size, i;
int total;
int conflictFlag, inverted;
int j, value, level;
satLevel_t *d;
satArray_t *saved;
satArray_t *clause;

  d = 0;
  saved = cm->savedConflictClauses;
  if(saved == 0)
    return;

  clause = sat_ArrayAlloc(50);

  total = 0;
  for(i=0, space=saved->space; i<saved->num; i++, space++){
    if(*space < 0) {
      start = space;
      space++;
      i++;
      size = 0;
      clause->num = 0;
      conflictFlag = 0;
      while(*space > 0) {
        sat_ArrayInsert(clause, SATnot((*space)));
        if(conflictFlag == 0) {
          nv = *space;
          inverted = (SATisInverted(nv));
          nv = SATnormalNode(nv);

          d = sat_AllocLevel(cm);
          d->decisionNode = nv;
          SATvalue(nv) = inverted;
          SATmakeImplied(nv, d);

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

          sat_ImplicationMain(cm, d);
          if(d->conflict)       conflictFlag = 1;
        }
        size++;
        i++;
        space++;
      }

      if(d->conflict == 0) {
        fprintf(cm->stdOut, "%s ERROR : %ld does not result in conflict\n",
            cm->comment, *start);
        for(j=0; j<clause->num; j++) {
          nv = clause->space[j];
          inverted = SATisInverted(nv);
          nv = SATnormalNode(nv);
          value = SATvalue(nv);
          level = value>1 ? -1 : SATlevel(nv);
          fprintf(cm->stdOut, "%6ld%c@%d=%c%c ",
                  nv, inverted ? '\'' : ' ', level, SATgetValueChar(value),
                  ' ');
        }
        fprintf(cm->stdOut, "\n");
      }
      sat_Backtrack(cm, -1);

      total++;
    }
  }
  sat_ArrayFree(clause);
}

void
sat_SaveNonobjClauses(satManager_t *cm)
{
int limit, total, passed;
int size, j;
long *plit, nv, v, i;
satArray_t *savedArray;

  savedArray = sat_ArrayAlloc(1024);

  total = passed = 0;
  limit = cm->option->incNumNonobjLitsLimit;
  for(i=cm->beginConflict; i<cm->nodesArraySize; i+= satNodeSize) {
    if(SATreadInUse(i) == 0)            continue;
    if(!(SATflags(i) & NonobjMask))     {
      continue;
    }
    size = SATnumLits(i);
    if(size > limit) {
      total++;
    }
    else {
      total++;
      passed++;
      plit = (long*)SATfirstLit(i);
      nv = (*(plit-1));
      sat_ArrayInsert(savedArray, nv);
      for(j=0; j<size; j++, plit++) {
        v = SATgetNode(*plit);
        sat_ArrayInsert(savedArray, v);
      }
      sat_ArrayInsert(savedArray, nv);
    }
  }
  if(cm->option->verbose > 1) {
    fprintf(cm->stdOut, "%s %d NonObjective Clauses forwarded out of %d\n",
            cm->comment, passed, total);
  }
  cm->savedConflictClauses = savedArray;
}

void
sat_SaveAllClauses(satManager_t *cm)
{
int limit, total, passed;
int size, j;
long *plit, nv, v, i;
satArray_t *savedArray;

  savedArray = sat_ArrayAlloc(1024);

  total = passed = 0;
  limit = cm->option->incNumNonobjLitsLimit;
  for(i=cm->beginConflict; i<cm->nodesArraySize; i+= satNodeSize) {
    if(SATreadInUse(i) == 0)            continue;
    size = SATnumLits(i);
    total++;
    plit = (long*)SATfirstLit(i);
    nv = (*(plit-1));
    sat_ArrayInsert(savedArray, nv);
    for(j=0; j<size; j++, plit++) {
      v = SATgetNode(*plit);
      sat_ArrayInsert(savedArray, v);
    }
    sat_ArrayInsert(savedArray, nv);
  }
  cm->savedConflictClauses = savedArray;
}

void
sat_BuildTrieForDistill(satManager_t *cm)
{
int limit, nCl, nLit;
int j, n;
int size, inverted;
long v, *plit, i;
int findFlag;
satVariable_t *var;
satArray_t *trieArray;
satArray_t *unitArray;
satTrie_t *t;

  size = cm->initNumVariables * satNodeSize;
  for(i=satNodeSize; i<size; i+= satNodeSize) {
    var = SATgetVariable(i);
    var->scores[0] = 0;
    var->scores[1] = 0;
  }

  nCl = nLit = 0;
  limit = cm->option->incNumObjLitsLimit;
  for(i=cm->beginConflict; i<cm->nodesArraySize; i+= satNodeSize) {
    if(SATreadInUse(i) == 0)            continue;
    if(SATflags(i) & NonobjMask)        continue;

    size = SATnumLits(i);
    if(size > limit)    continue;
    n = 0;
    for(j=0, plit = (long*)SATfirstLit(i); j<size; j++, plit++) {
      v = SATgetNode(*plit);
      inverted = SATisInverted(v);
      v = SATnormalNode(v);
      var = SATgetVariable(v);
      var->scores[inverted] += 1;
      if(SATvalue(v) < 2)       continue;
      n++;
    }
    if(n > 0) {
      nCl++;
      nLit += n;
    }
  }
  if(cm->option->verbose > 1) {
    fprintf(cm->stdOut, "%s Candidates for Distill %d clauses %d literals\n",
            cm->comment, nCl, nLit);
  }

  trieArray = sat_ArrayAlloc(64);
  cm->trieArray = trieArray;
  unitArray = cm->objUnitLitArray;
  if(unitArray) {
    for(i=0; i<unitArray->num; i++) {
      v = unitArray->space[i];
      inverted = SATisInverted(v);
      v = SATnormalNode(v);

      findFlag = 0;
      for(j=0;  j<trieArray->num; j++) {
        t = (satTrie_t *)(trieArray->space[j]);
        if(t->id == v) {
          if(t->child[inverted] == 0)
            t->child[inverted] = sat_ArrayAlloc(2);
          findFlag = 1;
        }
      }

      if(findFlag == 0) {
        t = ALLOC(satTrie_t, 1);
        memset(t, 0, sizeof(satTrie_t));
        t->id = v;
        if(t->child[inverted] == 0)
          t->child[inverted] = sat_ArrayAlloc(2);
        sat_ArrayInsert(trieArray, (long)t);
      }
    }
  }

  for(i=cm->beginConflict; i<cm->nodesArraySize; i+=satNodeSize) {
    if(SATreadInUse(i) == 0)            continue;
    if(SATflags(i) & NonobjMask)        continue;

    size = SATnumLits(i);
    if(size > limit)    continue;

    plit = (long*)SATfirstLit(i);
    SatCm = cm;
    qsort(plit, size, sizeof(long), ScoreDistillCompare);
    sat_BuildTrie(cm, trieArray, plit, 1);
  }
}

void
sat_BuildTrie(
        satManager_t *cm,
        satArray_t *trieArray,
        long *plit,
        int depth)
{
int i, inverted;
long v;
satTrie_t *t;

  while(1) {
    if(*plit <= 0)      return;
    v = SATgetNode(*plit);
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    if(SATvalue(v) < 2)plit++;
    else                break;
  }

  for(i=0; i<trieArray->num; i++) {
    t = (satTrie_t *)(trieArray->space[i]);
    if(t->id == v) {
      if(t->child[inverted] == 0)
        t->child[inverted] = sat_ArrayAlloc(2);
      plit++;
      sat_BuildTrie(cm, t->child[inverted], plit, depth+1);
      return;
    }
  }

  t = ALLOC(satTrie_t, 1);
  memset(t, 0, sizeof(satTrie_t));
  t->id = v;
  t->depth = depth;
  sat_ArrayInsert(trieArray, (long)t);

  if(t->child[inverted] == 0)
    t->child[inverted] = sat_ArrayAlloc(2);
  plit++;
  sat_BuildTrie(cm, t->child[inverted], plit, depth+1);
}



void
sat_FreeTrie(satManager_t *cm, satArray_t *arr)
{
int i;
satTrie_t *t;

  if(arr == 0)  return;

  for(i=0; i<arr->num; i++) {
    t = (satTrie_t *)(arr->space[i]);
    if(t->child[0]) {
      sat_FreeTrie(cm, t->child[0]);
      sat_ArrayFree(t->child[0]);
    }
    if(t->child[1]) {
      sat_FreeTrie(cm, t->child[1]);
      sat_ArrayFree(t->child[1]);
    }
    free(t);
  }

}
static int
ScoreDistillCompare(const void *x, const void *y)
{
int n1, n2;
int i1, i2;
satVariable_t  v1, v2;

  n1 = *(int *)x;
  n2 = *(int *)y;
  n1 >>= 2;
  n2 >>= 2;
  i1 = SATisInverted(n1);
  n1 = SATnormalNode(n1);
  i2 = SATisInverted(n2);
  n2 = SATnormalNode(n2);
  v1 = SatCm->variableArray[SATnodeID(n1)];
  v2 = SatCm->variableArray[SATnodeID(n2)];

  if(v1.scores[i1] == v2.scores[i2]) {
    return(n1 > n2);
  }
  return(v1.scores[i1] < v2.scores[i2]);
}