src/sat/satMain.c

Go to the documentation of this file.

#include "satInt.h"

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

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

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


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


void
sat_PreProcessing(satManager_t *cm)
{
satLevel_t *d;


  cm->queue = sat_CreateQueue(1024);
  cm->BDDQueue = sat_CreateQueue(1024);
  cm->unusedAigQueue = sat_CreateQueue(1024);

  if(cm->variableArray == 0) {
    cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
    memset(cm->variableArray, 0,
            sizeof(satVariable_t) * (cm->initNumVariables+1));
  }

  cm->auxArray = sat_ArrayAlloc(1024);
  cm->nonobjUnitLitArray = sat_ArrayAlloc(128);
  cm->objUnitLitArray = sat_ArrayAlloc(128);

  //sat_CompactFanout(cm);

  //Bing:
  if(cm->option->AbRf == 0)
    sat_CompactFanout(cm);

  sat_InitScore(cm);

  if(cm->decisionHeadSize == 0) {
    cm->decisionHeadSize = 32;
    cm->decisionHead = ALLOC(satLevel_t, cm->decisionHeadSize);
    memset(cm->decisionHead, 0, sizeof(satLevel_t) * cm->decisionHeadSize);
  }
  cm->currentDecision = -1;

  SATvalue(2) = 2;
  SATflags(0) = 0;

  cm->initNodesArraySize = cm->nodesArraySize;
  cm->beginConflict = cm->nodesArraySize;

  if(cm->option->incTraceObjective) {
    sat_RestoreForwardedClauses(cm, 0);
  }
  else if(cm->option->incAll) {
    sat_RestoreForwardedClauses(cm, 1);
  }

  if(cm->option->incTraceObjective) {
    sat_MarkObjectiveFlagToArray(cm, cm->obj);
    sat_MarkObjectiveFlagToArray(cm, cm->objCNF);
  }


  d = sat_AllocLevel(cm);

  sat_ApplyForcedAssignmentMain(cm, d);

  if(cm->status == SAT_UNSAT)
    return;


  //Bing:
  if(cm->option->coreGeneration && cm->option->IP){
    cm->rm = ALLOC(RTManager_t, 1);
    memset(cm->rm,0,sizeof(RTManager_t));
  }
  //Bing
  if(!(cm->option->SSS==1 && cm->option->coreGeneration==1))
    sat_ImplyArray(cm, d, cm->pureLits);

  sat_ImplyArray(cm,d,cm->assertArray);
  sat_ImplyArray(cm, d, cm->assertion);
  sat_ImplyArray(cm, d, cm->unitLits);
  sat_ImplyArray(cm, d, cm->auxObj);
  sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
  sat_ImplyArray(cm, d, cm->obj);

  sat_ImplicationMain(cm, d);
  if(d->conflict) {
    cm->status = SAT_UNSAT;
  }

  if(cm->status == 0) {
    if(cm->option->incDistill) {
      sat_IncrementalUsingDistill(cm);
    }
  }

}

void
sat_PreProcessingForMixed(satManager_t *cm)
{
satLevel_t *d;


  cm->queue = sat_CreateQueue(1024);
  cm->BDDQueue = sat_CreateQueue(1024);
  cm->unusedAigQueue = sat_CreateQueue(1024);

  if(cm->variableArray == 0) {
    cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
    memset(cm->variableArray, 0,
            sizeof(satVariable_t) * (cm->initNumVariables+1));
  }

  cm->auxArray = sat_ArrayAlloc(1024);
  cm->nonobjUnitLitArray = sat_ArrayAlloc(128);
  cm->objUnitLitArray = sat_ArrayAlloc(128);

  sat_CompactFanout(cm);

  cm->initNodesArraySize = cm->nodesArraySize;
  cm->beginConflict = cm->nodesArraySize;

  if(cm->option->allSatMode) {
    sat_RestoreFrontierClauses(cm);
    sat_RestoreBlockingClauses(cm);
  }

  sat_InitScoreForMixed(cm);

  if(cm->decisionHeadSize == 0) {
    cm->decisionHeadSize = 32;
    cm->decisionHead = ALLOC(satLevel_t, cm->decisionHeadSize);
    memset(cm->decisionHead, 0, sizeof(satLevel_t) * cm->decisionHeadSize);
  }
  cm->currentDecision = -1;

  SATvalue(2) = 2;
  SATflags(0) = 0;

  if(cm->option->incTraceObjective) {
    sat_RestoreForwardedClauses(cm, 0);
  }
  else if(cm->option->incAll) {
    sat_RestoreForwardedClauses(cm, 1);
  }

  if(cm->option->incTraceObjective) {
    sat_MarkObjectiveFlagToArray(cm, cm->obj);
    sat_MarkObjectiveFlagToArray(cm, cm->objCNF);
  }

  d = sat_AllocLevel(cm);

  sat_ApplyForcedAssignmentMain(cm, d);

  if(cm->status == SAT_UNSAT)
    return;

  sat_ImplyArray(cm, d, cm->assertion);
  sat_ImplyArray(cm, d, cm->unitLits);
  sat_ImplyArray(cm, d, cm->pureLits);
  sat_ImplyArray(cm, d, cm->auxObj);
  sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
  sat_ImplyArray(cm, d, cm->obj);

  sat_ImplicationMain(cm, d);
  if(d->conflict) {
    cm->status = SAT_UNSAT;
  }

  if(cm->status == 0) {
    if(cm->option->incDistill) {
      sat_IncrementalUsingDistill(cm);
    }
  }

}

void
sat_PreProcessingForMixedNoCompact(satManager_t *cm)
{
satLevel_t *d;


  cm->queue = sat_CreateQueue(1024);
  cm->BDDQueue = sat_CreateQueue(1024);
  cm->unusedAigQueue = sat_CreateQueue(1024);

  if(cm->variableArray == 0) {
    cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
    memset(cm->variableArray, 0,
            sizeof(satVariable_t) * (cm->initNumVariables+1));
  }

  if(cm->auxArray == 0)
    cm->auxArray = sat_ArrayAlloc(1024);
  if(cm->nonobjUnitLitArray == 0)
    cm->nonobjUnitLitArray = sat_ArrayAlloc(128);
  if(cm->objUnitLitArray == 0)
    cm->objUnitLitArray = sat_ArrayAlloc(128);

  cm->initNodesArraySize = cm->nodesArraySize;
  cm->beginConflict = cm->nodesArraySize;

  if(cm->option->allSatMode) {
    sat_RestoreFrontierClauses(cm);
    sat_RestoreBlockingClauses(cm);
  }

  sat_InitScoreForMixed(cm);

  if(cm->decisionHeadSize == 0) {
    cm->decisionHeadSize = 32;
    cm->decisionHead = ALLOC(satLevel_t, cm->decisionHeadSize);
    memset(cm->decisionHead, 0, sizeof(satLevel_t) * cm->decisionHeadSize);
  }
  cm->currentDecision = -1;

  SATvalue(2) = 2;
  SATflags(0) = 0;

  if(cm->option->incTraceObjective) {
    sat_RestoreForwardedClauses(cm, 0);
  }
  else if(cm->option->incAll) {
    sat_RestoreForwardedClauses(cm, 1);
  }

  if(cm->option->incTraceObjective) {
    sat_MarkObjectiveFlagToArray(cm, cm->obj);
    sat_MarkObjectiveFlagToArray(cm, cm->objCNF);
  }

  d = sat_AllocLevel(cm);

  sat_ApplyForcedAssignmentMain(cm, d);

  if(cm->status == SAT_UNSAT)
    return;

  sat_ImplyArray(cm, d, cm->assertion);
  sat_ImplyArray(cm, d, cm->unitLits);
  sat_ImplyArray(cm, d, cm->pureLits);
  sat_ImplyArray(cm, d, cm->auxObj);
  sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
  sat_ImplyArray(cm, d, cm->obj);

  sat_ImplicationMain(cm, d);
  if(d->conflict) {
    cm->status = SAT_UNSAT;
  }

  if(cm->status == 0) {
    if(cm->option->incDistill) {
      sat_IncrementalUsingDistill(cm);
    }
  }

}

void
sat_MarkObjectiveFlagToArray(
        satManager_t *cm,
        satArray_t *objArr)
{
int i;
long v;

  if(objArr == 0)       return;

  for(i=0; i<objArr->num; i++) {
    v = objArr->space[i];
    v = SATnormalNode(v);
    SATflags(v) |= ObjMask;
  }
}

void
sat_PostProcessing(satManager_t *cm)
{

  sat_Verify(cm);

  if(cm->option->incTraceObjective) {
    sat_SaveNonobjClauses(cm);
  }

  if(cm->option->incAll) {
    sat_SaveAllClauses(cm);
  }

  if(cm->option->allSatMode) {
    sat_CollectBlockingClause(cm);
  }

  //Bing:
  //sat_RestoreFanout(cm);
  if(cm->option->AbRf == 0)
    sat_RestoreFanout(cm);

  if(cm->mgr) {
#ifdef BDDcu
    Cudd_Quit(cm->mgr);
#endif
    cm->mgr = 0;
  }

}

void
sat_Main(satManager_t *cm)
{
long btime, etime;

  btime = util_cpu_time();
  sat_PreProcessing(cm);

  if(cm->status == 0)
    sat_Solve(cm);

  if(cm->option->coreGeneration && cm->status == SAT_UNSAT){
    //Bing
    if(cm->option->RT)
      sat_GenerateCore_All(cm);
    else
      sat_GenerateCore(cm);
  }

  sat_PostProcessing(cm);

  etime = util_cpu_time();
  cm->each->satTime = (double)(etime - btime) / 1000.0 ;

}

void
sat_Solve(satManager_t *cm)
{
satLevel_t *d;
satOption_t *option;
satVariable_t *var;
int level;

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

  option = cm->option;
  if(option->BDDMonolithic) {
    sat_TryToBuildMonolithicBDD(cm);
  }

  if(cm->status == SAT_UNSAT) {
    sat_Undo(cm, SATgetDecision(0));
    return;
  }

  while(1) {
    sat_PeriodicFunctions(cm);

    if(cm->currentDecision == 0)
      sat_BuildLevelZeroHyperImplicationGraph(cm);

    d = sat_MakeDecision(cm);

    if(d == 0)  {
      cm->status = SAT_SAT;
      return;
    }

    while(1) {
      sat_ImplicationMain(cm, d);

      if(d->conflict == 0)      {
        if(cm->option->verbose > 2) {
          var = SATgetVariable(d->decisionNode);
          fprintf(cm->stdOut, "decision at %3d on %6ld <- %ld score(%d %d) %d %ld implied %.3f %%\n",
            d->level, d->decisionNode, SATvalue(d->decisionNode),
            var->scores[0], var->scores[1],
            cm->each->nDecisions, d->implied->num,
            (double)cm->implicatedSoFar/(double)cm->initNumVariables * 100);
          fflush(cm->stdOut);
        }

        break;
      }

        if(cm->option->verbose > 2) {
          var = SATgetVariable(d->decisionNode);
          fprintf(cm->stdOut, "decision at %3d on %6ld <- %ld score(%d %d) %d %ld implied  %.3f %% Conflict\n",
            d->level, d->decisionNode, SATvalue(d->decisionNode),
            var->scores[0], var->scores[1],
            cm->each->nDecisions, d->implied->num,
            (double)cm->implicatedSoFar/(double)cm->initNumVariables * 100);
          fflush(cm->stdOut);
        }

      if(cm->option->useStrongConflictAnalysis)
        level = sat_StrongConflictAnalysis(cm, d);
      else
        level = sat_ConflictAnalysis(cm, d);

      if(cm->currentDecision == -1) {
        if(cm->option->incDistill) {
          sat_BuildTrieForDistill(cm);
        }
        sat_Undo(cm, SATgetDecision(0));
        cm->status = SAT_UNSAT;
        return;
      }

      d = SATgetDecision(cm->currentDecision);
    }

  }
}

void
sat_PeriodicFunctions(satManager_t *cm)
{
satStatistics_t *stats;
satOption_t *option;
int nDecisions;
int gap;

  stats = cm->each;
  option = cm->option;
  nDecisions = stats->nDecisions-stats->nShrinkDecisions;
  if(nDecisions && !(nDecisions % option->decisionAgeInterval)) {
    if(option->decisionAgeRestart) {
      gap = stats->nConflictCl-stats->nOldConflictCl;
      if(gap > option->decisionAgeInterval>>2)  {
        sat_UpdateScore(cm);
        sat_Backtrack(cm, cm->lowestBacktrackLevel);
        cm->currentTopConflict = cm->literals->last-1;
        cm->currentTopConflictCount = 0;
        cm->lowestBacktrackLevel = MAXINT;
      }
      stats->nOldConflictCl = stats->nConflictCl;
    }
    else {
      sat_UpdateScore(cm);
    }

  }

  if(option->clauseDeletionHeuristic & LATEST_ACTIVITY_DELETION &&
          stats->nBacktracks > option->nextClauseDeletion &&
     cm->implicatedSoFar > cm->initNumVariables/3) {
    option->nextClauseDeletion += option->clauseDeletionInterval;
    sat_ClauseDeletionLatestActivity(cm);
  }
  else if(option->clauseDeletionHeuristic & MAX_UNRELEVANCE_DELETION &&
          stats->nBacktracks > option->nextClauseDeletion) {
    option->nextClauseDeletion += option->clauseDeletionInterval;
    sat_ClauseDeletion(cm);
  }

}

void
sat_CNFMain(satOption_t *option, char *filename)
{
satManager_t *cm;
int maxSize;

  cm = sat_InitManager(0);
  cm->comment = ALLOC(char, 2);
  cm->comment[0] = ' ';
  cm->comment[1] = '\0';
  if(option->outFilename) {
    if(!(cm->stdOut = fopen(option->outFilename, "w"))) {
      fprintf(stdout, "ERROR : Can't open file %s\n", option->outFilename);
      cm->stdOut = stdout;
      cm->stdErr = stderr;
    }
    else {
      cm->stdErr = cm->stdOut;
    }
  }
  else {
    cm->stdOut = stdout;
    cm->stdErr = stderr;
  }

  cm->option = option;
  cm->each = sat_InitStatistics();

  cm->unitLits = sat_ArrayAlloc(16);
  cm->pureLits = sat_ArrayAlloc(16);

  maxSize = 1024 << 8;
  cm->nodesArray = ALLOC(long, maxSize);
  cm->maxNodesArraySize = maxSize;
  cm->nodesArraySize = satNodeSize;

  sat_AllocLiteralsDB(cm);

  if(!sat_ReadCNF(cm, filename)) {
    sat_FreeManager(cm);
    return;
  }

  if(cm->option->coreGeneration==0)
    cm->option->useStrongConflictAnalysis = 1;

  sat_Main(cm);

  //Bing:change
  //unsat core
  if(cm->option->coreGeneration)
    fclose(cm->fp);

  if(cm->status == SAT_UNSAT) {
    if(cm->option->forcedAssignArr)
      fprintf(cm->stdOut, "%s UNSAT under given assignment\n",
              cm->comment);
    fprintf(cm->stdOut, "%s UNSATISFIABLE\n", cm->comment);
    fflush(cm->stdOut);
    sat_ReportStatistics(cm, cm->each);
    sat_FreeManager(cm);
  }
  else if(cm->status == SAT_SAT) {
    fprintf(cm->stdOut, "%s SATISFIABLE\n", cm->comment);
    fflush(cm->stdOut);
    sat_PrintSatisfyingAssignment(cm);
    sat_ReportStatistics(cm, cm->each);
    sat_FreeManager(cm);
  }
  if(cm->stdOut != stdout)
    fclose(cm->stdOut);
  if(cm->stdErr != stderr && cm->stdErr != cm->stdOut)
    fclose(cm->stdErr);
}

int
sat_CNFMainWithArray(
        satOption_t *option,
        satArray_t *cnfArray,
        int unsatCoreFlag,
        satArray_t *coreArray,
        st_table *mappedTable)
{
satManager_t *cm;
int maxSize;
int flag;
int i;
long v;

  cm = sat_InitManager(0);
  cm->comment = ALLOC(char, 2);
  cm->comment[0] = ' ';
  cm->comment[1] = '\0';
  if(option->outFilename) {
    if(!(cm->stdOut = fopen(option->outFilename, "w"))) {
      fprintf(stdout, "ERROR : Can't open file %s\n", option->outFilename);
      cm->stdOut = stdout;
      cm->stdErr = stderr;
    }
    else {
      cm->stdErr = cm->stdOut;
    }
  }
  else {
    cm->stdOut = stdout;
    cm->stdErr = stderr;
  }

  cm->option = option;
  cm->each = sat_InitStatistics();

  cm->unitLits = sat_ArrayAlloc(16);
  cm->pureLits = sat_ArrayAlloc(16);

  maxSize = 1024 << 8;
  cm->nodesArray = ALLOC(long, maxSize);
  cm->maxNodesArraySize = maxSize;
  cm->nodesArraySize = satNodeSize;

  sat_AllocLiteralsDB(cm);

  if(unsatCoreFlag) {
    cm->option->useStrongConflictAnalysis = 0;
    cm->option->coreGeneration = 1;
    cm->dependenceTable = st_init_table(st_ptrcmp, st_ptrhash);
    cm->anteTable = st_init_table(st_numcmp, st_numhash);
  }

  if(!sat_ReadCNFFromArray(cm, cnfArray, mappedTable)) {
    sat_FreeManager(cm);
    return(SAT_UNSAT);
  }

  sat_Main(cm);

  if(cm->status == SAT_UNSAT) {
    if(cm->option->forcedAssignArr)
      fprintf(cm->stdOut, "%s UNSAT under given assignment\n",
              cm->comment);
    fprintf(cm->stdOut, "%s UNSATISFIABLE\n", cm->comment);
    fflush(cm->stdOut);
    sat_ReportStatistics(cm, cm->each);
    flag = SAT_UNSAT;

    if(unsatCoreFlag) {
      for(i=0; i<cm->clauseIndexInCore->num; i++) {
        v = cm->clauseIndexInCore->space[i];
        sat_ArrayInsert(coreArray, v);
      }
    }
  }
  else if(cm->status == SAT_SAT) {
    fprintf(cm->stdOut, "%s SATISFIABLE\n", cm->comment);
    fflush(cm->stdOut);
    sat_PrintSatisfyingAssignment(cm);
    sat_ReportStatistics(cm, cm->each);
    flag = SAT_SAT;
  }
  if(cm->stdOut != stdout)
    fclose(cm->stdOut);
  if(cm->stdErr != stderr && cm->stdErr != cm->stdOut)
    fclose(cm->stdErr);

  sat_FreeManager(cm);

  return(flag);
}

int
sat_PrintSatisfyingAssignment(satManager_t *cm)
{
int i, size, index, value;

  index = 0;
  size = cm->initNumVariables * satNodeSize;
  for(i=satNodeSize; i<=size; i+=satNodeSize) {
    if(!(SATflags(i) & CoiMask))        continue;
    index ++;
    value = SATvalue(i);
    if(value == 1) {
      fprintf(cm->stdOut, "%ld ", SATnodeID(i));
    }
    else if(value == 0) {
      fprintf(cm->stdOut, "%ld ", -(SATnodeID(i)));
    }
    else {
      fprintf(cm->stdOut, "\n%s ERROR : unassigned variable %d\n", cm->comment, i);
      fflush(cm->stdOut);
      return(0);
    }

    if(((index % 10) == 0) && (i+satNodeSize <= size))
      fprintf(cm->stdOut, "\n ");
  }
  fprintf(cm->stdOut, "\n");
  return(1);
}

void
sat_Verify(satManager_t *cm)
{
int value, size, i;
int v, flag;
satArray_t *arr;
satLevel_t *d;

  if(cm->status != SAT_SAT)     return;

  size = cm->initNumVariables * satNodeSize;
  arr = sat_ArrayAlloc(cm->initNumVariables);
  for(i=satNodeSize; i<=size; i+=satNodeSize) {
    if(!(SATflags(i) & CoiMask))
      continue;
    value = SATvalue(i);
    if(value > 1) {
      fprintf(cm->stdOut, "%s ERROR : unassigned variable %d\n", cm->comment, i);
      fflush(cm->stdOut);
    }
    else {
      v = value ? i : SATnot(i);
      sat_ArrayInsert(arr, v);
    }
  }

  sat_Backtrack(cm, -1);

  d = sat_AllocLevel(cm);
  flag = sat_ApplyForcedAssigment(cm, arr, d);
  sat_ArrayFree(arr);
  if(flag == 1) {
    fprintf(cm->stdOut,
           "%s ERROR : Wrong satisfying assignment\n", cm->comment);
    fflush(cm->stdOut);
    exit(0);
  }
}