src/sat/satMain.c File Reference

#include "satInt.h"

Include dependency graph for satMain.c:

Go to the source code of this file.

Functions
void	sat_PreProcessing (satManager_t *cm)
void	sat_PreProcessingForMixed (satManager_t *cm)
void	sat_PreProcessingForMixedNoCompact (satManager_t *cm)
void	sat_MarkObjectiveFlagToArray (satManager_t *cm, satArray_t *objArr)
void	sat_PostProcessing (satManager_t *cm)
void	sat_Main (satManager_t *cm)
void	sat_Solve (satManager_t *cm)
void	sat_PeriodicFunctions (satManager_t *cm)
void	sat_CNFMain (satOption_t *option, char *filename)
int	sat_CNFMainWithArray (satOption_t *option, satArray_t *cnfArray, int unsatCoreFlag, satArray_t *coreArray, st_table *mappedTable)
int	sat_PrintSatisfyingAssignment (satManager_t *cm)
void	sat_Verify (satManager_t *cm)
Variables
static char rcsid[]	UNUSED = "$Id: satMain.c,v 1.30 2009/04/11 18:26:37 fabio Exp $"

---

Function Documentation

void sat_CNFMain	(	satOption_t *	option,
		char *	filename
	)

Function********************************************************************

Synopsis [ Interface function for pure CNF based SAT solver]

Description [ Interface function for pure CNF based SAT solver ]

SideEffects [ ]

SeeAlso [ sat_Main ]

trigerring strong conflict analysis

Definition at line 641 of file satMain.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

int sat_CNFMainWithArray	(	satOption_t *	option,
		satArray_t *	cnfArray,
		int	unsatCoreFlag,
		satArray_t *	coreArray,
		st_table *	mappedTable
	)

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 ]

Definition at line 728 of file satMain.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_Main

(

satManager_t *

cm

)

Function********************************************************************

Synopsis [ main function for SAT solving]

Description [ main function for SAT solving]

SideEffects [ ]

SeeAlso [ ]

Bing: UNSAT core generation

Definition at line 453 of file satMain.c.

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

}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_MarkObjectiveFlagToArray	(	satManager_t *	cm,
		satArray_t *	objArr
	)

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 ]

Definition at line 382 of file satMain.c.

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

Here is the caller graph for this function:

void sat_PeriodicFunctions

(

satManager_t *

cm

)

Function********************************************************************

Synopsis [ Periodic functions for SAT solving]

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

SideEffects [ ]

SeeAlso [ sat_Solve ]

need to review restart mechanism

Definition at line 586 of file satMain.c.

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

}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_PostProcessing

(

satManager_t *

cm

)

Function********************************************************************

Synopsis [ Post-processing after running CirCUs]

Description [ Post-processing after running CirCUs]

SideEffects [ ]

SeeAlso [ sat_PreProcessing ]

Definition at line 410 of file satMain.c.

{

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

}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_PreProcessing

(

satManager_t *

cm

)

AutomaticStart AutomaticEnd 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 ]

create implication queue

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

compact fanout of AIG node

Initial score

create decision stack

to avoid purify warning

incremental SAT....

Level 0 decision....

Definition at line 54 of file satMain.c.

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

}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_PreProcessingForMixed

(

satManager_t *

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 ]

create implication queue

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

compact fanout of AIG node

Initial score

create decision stack

to avoid purify warning

incremental SAT....

Level 0 decision....

Definition at line 168 of file satMain.c.

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

}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_PreProcessingForMixedNoCompact

(

satManager_t *

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 ]

create implication queue

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

compact fanout of AIG node sat_CompactFanout(cm);

Initial score

create decision stack

to avoid purify warning

incremental SAT....

Level 0 decision....

Definition at line 272 of file satMain.c.

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

}

Here is the call graph for this function:

Here is the caller graph for this function:

int sat_PrintSatisfyingAssignment

(

satManager_t *

cm

)

Function********************************************************************

Synopsis [ Print satisfying assignment]

Description [ Print satisfying assignment ]

SideEffects [ ]

SeeAlso [ sat_CNFMain ]

Definition at line 832 of file satMain.c.

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

Here is the caller graph for this function:

void sat_Solve

(

satManager_t *

cm

)

Function********************************************************************

Synopsis [ DPLL procedure for SAT solving]

Description [ DPLL procedure for SAT solving]

SideEffects [ ]

SeeAlso [ sat_Main ]

Definition at line 492 of file satMain.c.

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

  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void sat_Verify

(

satManager_t *

cm

)

Function********************************************************************

Synopsis [ Verify satisfying assignment]

Description [ Verify satisfying assignment when the instance is satisfiable]

SideEffects [ ]

SeeAlso [ sat_Main ]

Definition at line 873 of file satMain.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

---

Variable Documentation

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

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.]

Definition at line 21 of file satMain.c.