source: vis_dev/vis-2.3/src/sat/satMain.c

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

  FileName    [satMain.c]

  PackageName [sat]

  Synopsis    [Routines for sat main function.]

  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: satMain.c,v 1.30 2009/04/11 18:26:37 fabio Exp $";

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

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

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


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


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


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

  Synopsis    [ Pre-processing to run CirCUs ]

  Description [ Pre-processing to run CirCUs ]

  SideEffects [ One has to run sat_PostProcessing after running CirCUs]

  SeeAlso     [ sat_PostProcessing ]

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


  /** create implication queue **/
  cm->queue = sat_CreateQueue(1024);
  cm->BDDQueue = sat_CreateQueue(1024);
  cm->unusedAigQueue = sat_CreateQueue(1024);

  /**
  create variable array : one can reduce size of variable array using
  mapping. for fanout free internal node....
  **/

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

  /** compact fanout of AIG node **/
  //sat_CompactFanout(cm);

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

  /** Initial score **/
  sat_InitScore(cm);

  /** create decision stack **/
  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;

  /** to avoid purify warning **/
  SATvalue(2) = 2;
  SATflags(0) = 0;

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

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


  /** Level 0 decision.... **/
  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);
    }
  }

}

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

  Synopsis    [ Pre-processing to run CirCUs with AIG and CNF]

  Description [ Pre-processing to run CirCUs with AIG and CNF]

  SideEffects [ One has to run sat_PostProcessing for AllSat enumeration after running CirCUs]

  SeeAlso     [ sat_PostProcessing ]

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


  /** create implication queue **/
  cm->queue = sat_CreateQueue(1024);
  cm->BDDQueue = sat_CreateQueue(1024);
  cm->unusedAigQueue = sat_CreateQueue(1024);

  /**
  create variable array : one can reduce size of variable array using
  mapping. for fanout free internal node....
  **/

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

  /** compact fanout of AIG node **/
  sat_CompactFanout(cm);

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

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

  /** Initial score **/
  sat_InitScoreForMixed(cm);

  /** create decision stack **/
  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;

  /** to avoid purify warning **/
  SATvalue(2) = 2;
  SATflags(0) = 0;

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

  /** Level 0 decision.... **/
  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);
    }
  }

}

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

  Synopsis    [ Pre-processing to run CirCUs with AIG and CNF]

  Description [ Pre-processing to run CirCUs with AIG and CNF]

  SideEffects [ One has to run sat_PostProcessing for AllSat enumeration after running CirCUs]

  SeeAlso     [ sat_PostProcessing ]

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


  /** create implication queue **/
  cm->queue = sat_CreateQueue(1024);
  cm->BDDQueue = sat_CreateQueue(1024);
  cm->unusedAigQueue = sat_CreateQueue(1024);

  /**
  create variable array : one can reduce size of variable array using
  mapping. for fanout free internal node....
  **/

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

  /** compact fanout of AIG node
  sat_CompactFanout(cm);
  **/

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

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

  /** Initial score **/
  sat_InitScoreForMixed(cm);

  /** create decision stack **/
  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;

  /** to avoid purify warning **/
  SATvalue(2) = 2;
  SATflags(0) = 0;

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

  /** Level 0 decision.... **/
  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);
    }
  }

}

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

  Synopsis    [ Mark objective flag to given AIG node or CNF clauses]

  Description [ To use incremental SAT algorithm based on trace objective,
                the objective has to be identified before starting the
                SAT process.]

  SideEffects [ One has to run sat_PostProcessing after running CirCUs]

  SeeAlso     [ sat_PostProcessing ]

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

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

  Synopsis    [ Post-processing after running CirCUs]

  Description [ Post-processing after running CirCUs]

  SideEffects [ ]

  SeeAlso     [ sat_PreProcessing ]

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

}

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

  Synopsis    [ main function for SAT solving]

  Description [ main function for SAT solving]

  SideEffects [ ]

  SeeAlso     [ ]

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

  btime = util_cpu_time();
  sat_PreProcessing(cm);

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

  /** Bing: UNSAT core generation **/
  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 ;

}

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

  Synopsis    [ DPLL procedure for SAT solving]

  Description [ DPLL procedure for SAT solving]

  SideEffects [ ]

  SeeAlso     [ sat_Main ]

******************************************************************************/

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

  }
}

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

  Synopsis    [ Periodic functions for SAT solving]

  Description [ Periodically, score aging and conflict clause deletion
                are invoked ]

  SideEffects [ ]

  SeeAlso     [ sat_Solve ]

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

  /** need to review restart mechanism **/
  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);
  }

}

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

  Synopsis    [ Interface function for pure CNF based SAT solver]

  Description [ Interface function for pure CNF based SAT solver ]

  SideEffects [ ]

  SeeAlso     [ sat_Main ]

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

  /** trigerring strong conflict analysis **/
  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);
}

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

  Synopsis    [ Interface function for pure CNF based SAT solver from array of CNF]

  Description [ Interface function for pure CNF based SAT solver  from array of CNF]

  SideEffects [ ]

  SeeAlso     [ sat_Main ]

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

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

  Synopsis    [ Print satisfying assignment]

  Description [ Print satisfying assignment ]

  SideEffects [ ]

  SeeAlso     [ sat_CNFMain ]

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

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

  Synopsis    [ Verify satisfying assignment]

  Description [ Verify satisfying assignment when the instance is satisfiable]

  SideEffects [ ]

  SeeAlso     [ sat_Main ]

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