source: vis_dev/vis-2.3/src/sat/satDebug.c @ 17

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

  FileName    [satDebug.c]

  PackageName [sat]

  Synopsis    [Routines for various debug 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: satDebug.c,v 1.14 2009/04/11 18:26:37 fabio Exp $";

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

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

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/
static int numCompareInt(const void *x, const void *y);


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


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


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

  Synopsis    [ Print node infomation]

  Description [ Print node infomation]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_PrintNode(
        satManager_t *cm,
        long v)
{
int inverted, i, size;
long ante, cur, *fan, *plit;
satVariable_t *var;
satArray_t *wl;

  inverted = SATisInverted(v);
  v = SATnormalNode(v);
  if(SATflags(v) & IsCNFMask) {
    size = SATnumLits(v);
    fprintf(cm->stdOut, "CNF %6ld (%4ld) U(%ld)", v, SATnumConflict(v), SATconflictUsage(v));
    sat_PrintFlag(cm, v);
    fprintf(cm->stdOut, "    ");
    for(i=0, plit = (long*)SATfirstLit(v); i<size; i++, plit++) {
      if(i!=0 && i%5 == 0)
        fprintf(cm->stdOut, "\n    ");
      sat_PrintLiteral(cm, *plit);
    }
    fprintf(cm->stdOut, "\n");
  }
  else if(SATflags(v) & IsBDDMask) {
  }
  else {
    fprintf(cm->stdOut, "AIG ");
    sat_PrintFlag(cm, SATnormalNode(v));
    fprintf(cm->stdOut, "    ");
    sat_PrintNodeAlone(cm, v);
    sat_PrintNodeAlone(cm, SATleftChild(v));
    sat_PrintNodeAlone(cm, SATrightChild(v));
    fprintf(cm->stdOut, "\n");
    size = SATnFanout(v);
    fprintf(cm->stdOut, "%4d ", size);
    for(i=0, fan=SATfanout(v); i<size; i++, fan++) {
      cur = (*fan) >>1;
      fprintf(cm->stdOut, "%6ld ", cur);
    }
    fprintf(cm->stdOut, "\n");

    fprintf(cm->stdOut, "  canonocal : %ld\n", sat_GetCanonical(cm, v));
    if(cm->variableArray && SATvalue(v) < 2) {
      ante = SATante(v);
      if(SATflags(ante) & IsCNFMask) {
        fprintf(cm->stdOut, "  ante CNF  : %ld\n", SATante(v));
      }
      else{
        fprintf(cm->stdOut, "  ante      : %ld\n", SATante(v));
        fprintf(cm->stdOut, "  ante2     : %ld\n", SATante2(v));
      }
    }

    if(cm->variableArray) {
    var = SATgetVariable(v);
    wl = var->wl[0];
    if(wl && wl->num) {
      fprintf(cm->stdOut, "  0 wl : ");
      for(i=0; i<wl->num; i++) {
        plit = (long *)(wl->space[i]);
        if(plit == 0)   continue;
        fprintf(cm->stdOut, "%ld", (*plit)>>2);
        while(1) {
          plit++;
          if(*plit < 0) break;
        }
        fprintf(cm->stdOut, "(%ld) ", -(*plit));
      }
      fprintf(cm->stdOut, "\n");
    }
    wl = var->wl[1];
    if(wl && wl->num) {
      fprintf(cm->stdOut, "  1 wl : ");
      for(i=0; i<wl->num; i++) {
        plit = (long *)(wl->space[i]);
        if(plit == 0)   continue;
        fprintf(cm->stdOut, "%ld", (*plit)>>2);
        while(1) {
          plit++;
          if(*plit < 0) break;
        }
        fprintf(cm->stdOut, "(%ld) ", -(*plit));
      }
      fprintf(cm->stdOut, "\n");
    }
    }
  }
  fflush(cm->stdOut);
}

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

  Synopsis    [ Print flag infomation]

  Description [ Print flag infomation]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_PrintFlag(satManager_t *cm, long v)
{
int flag;

  flag = SATflags(SATnormalNode(v));
  fprintf(cm->stdOut, "%c%c%c%c%c%c%c%c%c%c%c%c%c%c\n",
          (flag & CoiMask)           ? 'C' : ' ',
          (flag & VisitedMask)       ? 'V' : ' ',
          (flag & NewMask)           ? 'N' : ' ',
          (flag & InQueueMask)       ? 'Q' : ' ',
          (flag & ObjMask)           ? 'o' : ' ',
          (flag & NonobjMask)        ? 'n' : ' ',
          (flag & IsSystemMask)      ? 'S' : ' ',
          (flag & IsConflictMask)    ? 'c' : ' ',
          (flag & InUseMask)         ? 'U' : ' ',
          (flag & StaticLearnMask)   ? 's' : ' ',
          (flag & StateBitMask)      ? 'T' : ' ',
          (flag & IsBlockingMask)    ? 'B' : ' ',
          (flag & IsFrontierMask)    ? 'F' : ' ',
          (flag & LeafNodeMask)      ? 'L' : ' ');

}

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

  Synopsis    [ Print node infomation in the form of (id'@level = value)]

  Description [ Print node infomation in the form of (id'@level = value)]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_PrintNodeAlone(satManager_t *cm, long v)
{
int value, level, inverted;

  inverted = SATisInverted(v);
  v = SATnormalNode(v);
  value = SATvalue(v);
  level = value>1 ? -1 : (cm->variableArray ? SATlevel(v) : -1);
  fprintf(cm->stdOut, "%6ld%c@%d=%c%c ",
          v, inverted ? '\'' : ' ', level,
          SATgetValueChar(value),
          (SATflags(v)&ObjMask) ? '*' : ' ');
}

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

  Synopsis    [ Print literal information.]

  Description [ Print literal information.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_PrintLiteral(satManager_t *cm, long lit)
{
int value, level, inverted;
long v;

  v = SATgetNode(lit);
  inverted = SATisInverted(v);
  v = SATnormalNode(v);
  value = SATvalue(v);
  level = value>1 ? -1 : SATlevel(v);
  fprintf(cm->stdOut, "%6ld%c@%d=%c%c ",
          v, inverted ? '\'' : ' ', level, SATgetValueChar(value),
          SATisWL(lit) ? '*' : ' ');
}

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

  Synopsis    [ Print implication graph ]

  Description [ Print implication graph.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_PrintImplicationGraph(
        satManager_t *cm,
        satLevel_t *d)
{
long ante, ante2, v;
int i;
satArray_t *implied;

  fprintf(cm->stdOut, "++++++++++++++++++++++++++++++++\n");
  fprintf(cm->stdOut, "* Level %d %ld->%ld\n",
                d->level, d->decisionNode, SATvalue(d->decisionNode));
  fprintf(cm->stdOut, "++++++++++++++++++++++++++++++++\n");

  implied = d->implied;
  for(i=0; i<implied->num; i++) {
    v = implied->space[i];
    ante = SATante(v);
    if(SATflags(ante) & IsCNFMask) {
      sat_PrintNodeAlone(cm, v);
      fprintf(cm->stdOut, "<= %6ld %c(%cCNF)\n",
              ante, (SATflags(ante) & ObjMask) ? '*' : ' ',
              (SATflags(ante) & IsConflictMask) ? 'c' : ' ');
      sat_PrintNode(cm, ante);
    }
    else if(SATflags(ante) & IsBDDMask) {
    }
    else {
      sat_PrintNodeAlone(cm, v);
      fprintf(cm->stdOut, "<= ");
      sat_PrintNodeAlone(cm, ante);
      ante2 = SATante2(v);
      if(ante2)
        sat_PrintNodeAlone(cm, ante2);
      fprintf(cm->stdOut, "\n");
    }
  }
  fflush(cm->stdOut);
}

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

  Synopsis    [ Check flags then is used for conflict analysis. ]

  Description [ Check flags then is used for conflict analysis.
                After conflict analysis, these flags has to be reset ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_CheckFlagsOnConflict(satManager_t *cm)
{
long i;

  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    if(!(SATflags(i) & CoiMask))
      continue;

    if(SATflags(i) & VisitedMask || SATflags(i) & NewMask) {
      fprintf(cm->stdOut, "%s ERROR : %ld has flag\n",
              cm->comment, i);
      sat_PrintNode(cm, i);
    }
  }
}

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

  Synopsis    [ Print score]

  Description [ Print score]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_PrintScore(satManager_t *cm)
{
int i;
long v;
satArray_t *ordered;
satVariable_t *var;

  fprintf(cm->stdOut, "------------Print Score-----------\n");
  ordered = cm->orderedVariableArray;
  for(i=0; i<ordered->num; i++) {
    v = ordered->space[i];
    var = SATgetVariable(v);
    fprintf(cm->stdOut, "%5ld : %3d %3d\n", v, var->scores[0], var->scores[1]);
  }
  fflush(cm->stdOut);
}


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

  Synopsis    [ Print dot file of implication graph]

  Description [ Print dot file of implication graph ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_PrintDotForConflict(
        satManager_t *cm,
        satLevel_t *d,
        long conflict,
        int includePreviousLevel)
{
satArray_t *root;
long left, right, nv;
int inverted, size, value, i;
long *plit;
satOption_t *option;

  root = sat_ArrayAlloc(8);

  conflict = d->conflict;
  inverted = SATisInverted(conflict);
  conflict = SATnormalNode(conflict);

  option = cm->option;
  if(SATflags(conflict) & IsCNFMask) {
    size = SATnumLits(conflict);
    for(i=0, plit=(long*)SATfirstLit(conflict); i<size; i++, plit++) {
      nv = SATgetNode(*plit);
      if(d->level == SATlevel(nv))
        sat_ArrayInsert(root, nv);
    }
  }
  else {
    value = SATvalue(conflict);
    if(value == 1) {
      if(d->level == SATlevel(conflict))
        sat_ArrayInsert(root, conflict);

      left = SATleftChild(conflict);
      inverted = SATisInverted(left);
      left = SATnormalNode(left);
      value = SATvalue(left) ^ inverted;
      if(value == 0) {
        if(d->level == SATlevel(left))
          sat_ArrayInsert(root, left);
      }
      else {
        right = SATrightChild(conflict);
        inverted = SATisInverted(right);
        right = SATnormalNode(right);
        value = SATvalue(right) ^ inverted;
        if(value == 0) {
          if(d->level == SATlevel(right))
            sat_ArrayInsert(root, right);
        }
      }
    }
    else if(value == 0) {
      left = SATleftChild(conflict);
      right = SATrightChild(conflict);
      if(d->level == SATlevel(conflict))
        sat_ArrayInsert(root, conflict);
      if(d->level == SATlevel(left))
        sat_ArrayInsert(root, left);
      if(d->level == SATlevel(right))
        sat_ArrayInsert(root, right);
    }
  }

  sat_PrintDotForImplicationGraph(cm, d, root, includePreviousLevel);
  sat_ArrayFree(root);
}

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

  Synopsis    [ Print dot file of whole implication graph]

  Description [ Print dot file of whole implication graph ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_PrintDotForWholeGraph(
        satManager_t *cm,
        satLevel_t *d,
        int includePreviousLevel)
{
satArray_t *root, *implied;
int v, i;

  root = sat_ArrayAlloc(8);
  implied = d->implied;
  for(i=implied->num-1; i>=0; i--) {
    v = implied->space[i];
    sat_ArrayInsert(root, v);
  }
  sat_PrintDotForImplicationGraph(cm, d, root, includePreviousLevel);
  sat_ArrayFree(root);
}
/**Function********************************************************************

  Synopsis    [ Print dot file of implication graph]

  Description [ Print dot file of implication graph ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_PrintDotForImplicationGraph(
        satManager_t *cm,
        satLevel_t *d,
        satArray_t *root,
        int includePreviousLevel)
{
char name[1024];
long v, nv, *plit, lit;
int i, j, size;
int inverted;
long ante, ante2;
st_table *table;
FILE *fp;
satArray_t *implied;


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

  sprintf(name, "%d_%ld_%d_%d.dot",
          d->level, d->decisionNode, cm->each->nDecisions, includePreviousLevel);
  fp = fopen(name, "w");

  fprintf(fp, "digraph \"AndInv\" {\n  rotate=90;\n");
  fprintf(fp, "  margin=0.5;\n  label=\"AndInv\";\n");
  fprintf(fp, "  size=\"10,7.5\";\n  ratio=\"fill\";\n");

  table = st_init_table(st_numcmp, st_numhash);
  implied = d->implied;
  for(i=implied->num-1; i>=0; i--) {
    v = implied->space[i];
    if(!(SATflags(v) & VisitedMask)) continue;
    if((SATflags(v) & NewMask)) continue;

    st_insert(table, (char *)(long)v, (char *)(long)v);

    ante = SATante(v);
    if(SATflags(ante) & IsCNFMask) {
      size = SATnumLits(ante);
      for(j=0, plit=(long *)SATfirstLit(ante); j<size; j++) {
        lit = plit[j];
        nv = SATgetNode(lit);
        inverted = SATisInverted(nv);
        nv = SATnormalNode(nv);
        if(nv == v)     continue;

        st_insert(table, (char *)nv, (char *)nv);
        if(SATlevel(nv) == d->level) {
          fprintf(fp,"%ld.%d -> %ld.%d [color = red];\n",
                  nv, SATlevel(nv), v, SATlevel(v));
          SATflags(nv) |= VisitedMask;
        }
        else if(includePreviousLevel) {
          fprintf(fp,"%ld.%d -> %ld.%d [color = black];\n",
                  nv, SATlevel(nv), v, SATlevel(v));
        }
      }
    }
    else {
      fprintf(fp,"%ld.%d  [label=\"%ld.%d \"];\n", v, SATlevel(v), v, SATlevel(v));
      ante2 = SATnormalNode(SATante2(v));
      if(ante2) {
        st_insert(table, (char *)ante2, (char *)ante2);
        if(SATlevel(ante2) == d->level) {
          fprintf(fp,"%ld.%d -> %ld.%d [color = red];\n", ante2, SATlevel(ante2), v, SATlevel(v));
          SATflags(ante2) |= VisitedMask;
        }
        else if(includePreviousLevel && SATlevel(ante2)>=0) {
          fprintf(fp,"%ld.%d -> %ld.%d [color = black];\n", ante2, SATlevel(ante2), v, SATlevel(v));
        }
      }

      if(ante) {
        st_insert(table, (char *)ante, (char *)ante);
        if(SATlevel(ante) == d->level) {
          fprintf(fp,"%ld.%d -> %ld.%d [color = red];\n", ante, SATlevel(ante), v, SATlevel(v));
          SATflags(ante) |= VisitedMask;
        }
        else if(includePreviousLevel && SATlevel(ante)>=0) {
          fprintf(fp,"%ld.%d -> %ld.%d [color = black];\n", ante, SATlevel(ante), v, SATlevel(v));
        }
      }
    }
    SATflags(v) |= NewMask;
  }
  fprintf(fp, "}\n");
  fclose(fp);

  for(i=implied->num-1; i>=0; i--) {
    v = implied->space[i];
    SATflags(v) &= ResetNewVisitedMask;
  }
  for(i=0; i<root->num; i++) {
    v = root->space[i];
    SATflags(v) &= ResetVisitedMask;
  }

  st_free_table(table);

}

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

  Synopsis    [ Check whether the given conflict clauses are
                objective independent ]

  Description [ Check whether the given conflict clauses are
                objective independent ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_CheckNonobjConflictClause(
        satManager_t *cm,
        long v)
{
int i, size, inverted;
long *plit, nv;
satLevel_t *d;

  d = 0;
  size = SATnumLits(v);
  for(i=0, plit = (long*)SATfirstLit(v); i<size; i++, plit++) {
    nv = SATgetNode(*plit);
    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)     break;
  }

  if(d->conflict == 0) {
    fprintf(cm->stdOut, "%s ERROR : %ld does not result in conflict\n",
            cm->comment, v);
    sat_PrintNode(cm, v);
  }
  sat_Backtrack(cm, -1);
}

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

  Synopsis    [ Check whether the given conflict clauses are
                objective independent ]

  Description [ Check whether the given conflict clauses are
                objective independent ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_CheckNonobjUnitClause(
        satManager_t *cm)
{
int v, i;
int inverted;
satLevel_t *d;
satArray_t *arr;

  arr = cm->nonobjUnitLitArray;

  for(i=0; i<arr->num; i++) {
    v = arr->space[i];
    inverted = SATisInverted(v);
    v = SATnormalNode(v);

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

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

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

    sat_ImplicationMain(cm, d);
    if(d->conflict == 0) {
      fprintf(cm->stdOut, "%s ERROR : %d unit literal does not result in conflict\n",
            cm->comment, v);
    }
    sat_Backtrack(cm, -1);

  }
}

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

  Synopsis    [ Check initial condition of SAT solving ]

  Description [ Check initial condition of SAT solving ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_CheckInitialCondition(
        satManager_t *cm)
{
long i;

  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    if(!(SATflags(i) & CoiMask))
      continue;

    if(SATvalue(i) != 2) {
      fprintf(cm->stdOut, "%s ERROR : %ld has value %ld\n",
              cm->comment, i, SATvalue(i));
    }
    if(SATflags(i) & VisitedMask || SATflags(i) & NewMask) {
      fprintf(cm->stdOut, "%s ERROR : %ld has flag\n",
              cm->comment, i);
      sat_PrintNode(cm, i);
    }
  }
}

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

  Synopsis    [ Check whether inverse assignment of literals
                in conflict clause create conflict]

  Description [ Check whether inverse assignment of literals
                in conflict clause create conflict]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_CheckConflictClause(
        satManager_t *cm,
        satArray_t *clauseArray)
{
satArray_t *decisionArray;
satLevel_t *d;
int i, value, inverted;
long v;
int conflictFlag, tvalue;

  decisionArray = sat_ArrayAlloc(cm->currentDecision);
  for(i=1; i<=cm->currentDecision; i++) {
    v = cm->decisionHead[i].decisionNode;
    value = SATvalue(v);
    sat_ArrayInsert(decisionArray, v^(!value));
  }

  sat_Backtrack(cm, 0);

  conflictFlag = 0;
  for(i=0; i<clauseArray->num; i++) {
    v = clauseArray->space[i];
    inverted = SATisInverted(v);
    v = SATnormalNode(v);

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

    value = !inverted;
    tvalue = SATvalue(v);
    if(tvalue < 2 && tvalue !=  value) {
      fprintf(cm->stdOut, "ERROR : Early conflict condition detect\n");
      break;
    }
    SATvalue(v) = value;
    SATmakeImplied(v, d);

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

    sat_ImplicationMain(cm, d);

    if(d->conflict) {
      conflictFlag = 1;
      break;
    }
  }

  if(conflictFlag == 0) {
    fprintf(cm->stdOut, "ERROR : Wrong conflict clause\n");
    sat_PrintClauseArray(cm, clauseArray);
  }

  sat_Backtrack(cm, 0);

  conflictFlag = 0;
  for(i=0; i<decisionArray->num; i++) {
    v = decisionArray->space[i];
    inverted = SATisInverted(v);
    v = SATnormalNode(v);

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

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

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

    sat_ImplicationMain(cm, d);
    if(d->conflict) {
      conflictFlag = 1;
    }
  }
  if(conflictFlag == 0) {
    fprintf(cm->stdOut, "ERROR : Can't produce conflict\n");
    exit(0);
  }
}

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

  Synopsis    [ Print clause array ]

  Description [ Print clause array ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_PrintClauseArray(
        satManager_t *cm,
        satArray_t *clauseArray)
{
int i, inverted;
long v;

  fprintf(cm->stdOut, "    ");
  for(i=0; i<clauseArray->num; i++) {
    v = clauseArray->space[i];
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    if(i!=0 && i%5 == 0)
      fprintf(cm->stdOut, "\n    ");
    sat_PrintNodeAlone(cm, v);
  }
  fprintf(cm->stdOut, "\n");
  fflush(cm->stdOut);
}

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

  Synopsis    [ Print profile of the number of conflict on each clause]

  Description [ Print profile of the number of conflict on each clause]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_PrintProfileForNumConflict(satManager_t *cm)
{
char filename[1024];
FILE *fout;
int i, index;
satArray_t *arr;
long count;
long total, part;
long v;
long maxValue;


  sprintf(filename, "nConflict.dat");
  fout = fopen(filename, "w");
  index = 1;
  maxValue = 0;
  arr = sat_ArrayAlloc(1024);
  for(v=satNodeSize; v<cm->nodesArraySize; v+=satNodeSize) {
    if(!(SATflags(v) & IsCNFMask))      continue;
    if(SATnumConflict(v) == 0)  continue;
    if(SATnumConflict(v) > maxValue)
      maxValue = SATnumConflict(v);
    sat_ArrayInsert(arr, SATnumConflict(v));
  }

  qsort(arr->space, arr->num, sizeof(int), numCompareInt);
  total = 0;
  part = 0;
  for(i=0; i<arr->num; i++) {
    count = arr->space[i];
    if(count == 0)      continue;
    total += count;
    if(count > 1) {
      part += count;
    }
    fprintf(fout, "%d %ld\n", i, count);
  }
  index = i;
  sat_ArrayFree(arr);
  fclose(fout);


  sprintf(filename, "nConflict.gp");
  fout = fopen(filename, "w");
  fprintf(fout, "set xlabel \"Conflict Index\"\n");
  fprintf(fout, "set ylabel \"Number of Conflicting %ld/%ld\"\n", part, total);
  fprintf(fout, "set nokey\n");
  fprintf(fout, "set size square 0.8,1\n");
  fprintf(fout, "set xrange [0:%d]\n", index+1);
  fprintf(fout, "set yrange [0:%ld]\n", maxValue+1);
  fprintf(fout, "set grid\n");
  fprintf(fout, "set border 3 linewidth 0.5\n");
  fprintf(fout, "set xtics nomirror\n");
  fprintf(fout, "set ytics nomirror\n");
  fprintf(fout, "set mxtics 2\n");
  fprintf(fout, "set mytics 2\n");
  fprintf(fout, "set pointsize 2\n");
  fprintf(fout, "set terminal postscript eps enhanced color solid \"Times-Roman\" 24\n");
  fprintf(fout, "set output \"nConflict.eps\"\n");
  fprintf(fout, "plot \"nConflict.dat\" using 1:2 with line linetype 3\n");
  fclose(fout);
}

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

  Synopsis    [ Compare integer number]

  Description [ Compare integer number]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
numCompareInt(const void *x, const void *y)
{
long n1, n2;

  n1 = *(int *)x;
  n2 = *(int *)y;
  return(n1 > n2);
}