src/sat/satBDD.c

Go to the documentation of this file.

#include "satInt.h"
#ifdef BDDcu
#include "cuddInt.h"
#endif

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

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

#ifdef BDDcu

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

static int heapCostCompare(const void *c1, const void *c2);
static int sat_ConvertCNF2BDD(satManager_t *cm, DdManager *mgr, int conflictFlag);
static void sat_FreeLinearHead(satLinearHead_t *head);
static int linearVarCompare(const void * node1, const void * node2);
static int linearElemCompare(const void * node1, const void * node2);
static void sat_GetArrangementByForce(satManager_t *cm, satLinearHead_t *head);
static int sat_PrintCutProfile(satManager_t *cm, satLinearHead_t *head, char *baseName, int printFlag);
static int sat_ClusteringElementMain(satManager_t *cm, satLinearHead_t *head);
static void sat_ComputeVariableRange(satManager_t *cm, satLinearHead_t *head);
static void sat_InitClusteringElement(satManager_t *cm, satLinearHead_t *head);
static void sat_PrintSupportVariable(satLinearHead_t *head, satLinearElem_t *e1);
static void sat_ClusteringGetCandidate(satManager_t *cm, satLinearHead_t *head);
static DdNode *sat_SmoothWithDeadVariable(DdManager *mgr, satArray_t *deadArray, DdNode *bdd1, DdNode *bdd2, int bddAndLimit);
static int sat_ClusteringElement(satManager_t *cm, satLinearHead_t *head);
static void sat_FreeCluster(DdManager *mgr, satLinearCluster_t *clu);
static void sat_CheckDeadNode(satLinearHead_t *head, satLinearCluster_t *clu);

#endif


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

#ifdef BDDcu

void
sat_TryToBuildMonolithicBDD(satManager_t *cm)
{
DdManager *mgr;
int nVariables, flag;

  nVariables = cm->initNumVariables - cm->implicatedSoFar;

  if(nVariables
          > cm->option->maxLimitOfVariablesForMonolithicBDD)    return;

  mgr = Cudd_Init((unsigned int)(nVariables+1), 0, CUDD_UNIQUE_SLOTS,
                   CUDD_CACHE_SLOTS, getSoftDataLimit() / 10 * 9);
  cm->mgr = mgr;
  flag = sat_ConvertCNF2BDD(cm, mgr, 0);

  Cudd_Quit(mgr);
  cm->mgr = 0;

  if(flag == SAT_BDD_UNSAT)
    cm->status = SAT_UNSAT;

  return;
}


DdNode *
sat_CofactorBDDArray(
        satLinearHead_t *head,
        DdManager *mgr,
        DdNode *l1,
        satArray_t *satArr)
{
int i, vid, inverted;
long v;
DdNode *bdd, *result, *nresult;
satLinearVar_t *var;

  result = l1;
  cuddRef(result);
  for(i=0; i<satArr->num; i++) {
    v = satArr->space[i];
    inverted = SATisInverted(v);
    v = SATnormalNode(v);
    vid = head->edge2vid[SATnodeID(v)];
    var = &(head->varHead[vid]);
    bdd = inverted ? Cudd_Not(var->bdd) : var->bdd;

    nresult = Cudd_bddConstrain(mgr, result, bdd);
    cuddRef(nresult);
    Cudd_RecursiveDeref(mgr, result);
    result = nresult;
  }
  return(result);
}

void
sat_ExtractAssignmentFromBDD(
        satLinearHead_t *head,
        DdManager *mgr,
        satArray_t *arr,
        DdNode *cube)
{
DdNode *C, *T, *E, *zero;

  C = Cudd_Regular(cube);
  zero = Cudd_Not(DD_ONE(mgr));
  if (!cuddIsConstant(C)) {
    while (!cuddIsConstant(C)) {
      T = cuddT(C);
      E = cuddE(C);
      if (Cudd_IsComplement(cube)) {
        T = Cudd_Not(T);
        E = Cudd_Not(E);
      }
      if (T == zero)  { 
          sat_ArrayInsert(arr, ((head->id2edge[C->index]) + 1));
          cube = E;
      }
      else {                   
          sat_ArrayInsert(arr, (head->id2edge[C->index]));
          cube = T;
      }
      C = Cudd_Regular(cube);
    }
  }
  return;
}


satLinearHead_t *
sat_CreateLinearHead(
        satManager_t *cm,
        int conflictFlag)
{
satLinearHead_t *head;
satLinearElem_t *elem;
satLinearVar_t *lvar;
satArray_t *cArray, *vArray;
int nVars, nCls, varId;
int j, size, satisfied, inverted;
int value;
long v, *plit, i;
int elemIndex, varIndex;
int clauseLimit;

  nVars = 0;
  nCls = 0;
  cArray = sat_ArrayAlloc(1024);
  vArray = sat_ArrayAlloc(1024);
  for(i=satNodeSize; i<cm->initNodesArraySize; i+=satNodeSize) {
    if(!(SATflags(i) & IsCNFMask))      continue;
    if(SATreadInUse(i) == 0)    continue;
    size = SATnumLits(i);
    satisfied = 0;
    plit = (long *)SATfirstLit(i);
    for(j=0; j<size; j++, plit++) {
      v = SATgetNode(*plit);
      inverted = SATisInverted(v);
      v = SATnormalNode(v);
      value = SATvalue(v) ^ inverted;
      if(value == 1) {
        satisfied = 1;
        break;
      }
    }
    if(satisfied)       continue;

    nCls++;
    SATflags(i) |= VisitedMask;
    sat_ArrayInsert(cArray, i);

    plit = (long *)SATfirstLit(i);
    for(j=0; j<size; j++, plit++) {
      v = SATgetNode(*plit);
      v = SATnormalNode(v);
      if(SATvalue(v) < 2)       continue;
      if(!(SATflags(v) & VisitedMask)) {
        nVars++;
        SATflags(v) |= VisitedMask;
        sat_ArrayInsert(vArray, v);
      }
    }
  }

  if(conflictFlag)
    clauseLimit = cm->option->maxLimitOfClausesForBDDDPLL;
  else
    clauseLimit = cm->option->maxLimitOfClausesForMonolithicBDD;

  if(nCls > clauseLimit) {
    if(nVars > 100) {
      for(i=0; i<cArray->num; i++) {
        v = cArray->space[i];
        SATflags(v) &= ResetVisitedMask;
      }
      sat_ArrayFree(cArray);
      for(i=0; i<vArray->num; i++) {
        v = vArray->space[i];
        SATflags(v) &= ResetVisitedMask;
      }
      sat_ArrayFree(vArray);
      return(0);
    }
  }

  if(cm->option->verbose > 1) {
    fprintf(cm->stdOut, "NOTICE : Apply BDD based method at level %d with %d vars %d cls\n", cm->currentDecision, nVars, nCls);
    fflush(cm->stdOut);
  }
  head = ALLOC(satLinearHead_t, 1);
  memset(head, 0, sizeof(satLinearHead_t));
  head->clausesArray = cArray;
  head->variablesArray = vArray;
  head->reordering = 1;
  head->nVars = nVars;
  head->nCls = nCls;
  head->bddLimit = 5000;
  head->bddAndLimit = 10000;

  head->elemHead = ALLOC(satLinearElem_t, nCls);
  memset(head->elemHead, 0, sizeof(satLinearElem_t)*nCls);
  head->varHead = ALLOC(satLinearVar_t, nVars);
  memset(head->varHead, 0, sizeof(satLinearVar_t)*nVars);

  head->elemArray = sat_ArrayAlloc(nCls);
  head->varArray = sat_ArrayAlloc(nVars);
  head->latestClusterArray = sat_ArrayAlloc(32);
  head->deadArray = sat_ArrayAlloc(nVars);

  head->id2edge = ALLOC(long, nVars+1);
  head->edge2id = ALLOC(int, cm->initNumVariables+1);
  head->edge2vid = ALLOC(int, cm->initNumVariables+1);

  varIndex = 0;
  for(i=0; i<vArray->num; i++) {
    v = vArray->space[i];
    SATflags(v) &= ResetVisitedMask;
    lvar = &(head->varHead[varIndex]);
    head->edge2vid[SATnodeID(v)] = varIndex;
    sat_ArrayInsert(head->varArray, (long)lvar);
    lvar->order = varIndex++;
    lvar->node = v;
    lvar->bQuantified = 1;
    lvar->clauses = sat_ArrayAlloc(4);
  }

  elemIndex = 0;
  for(i=0; i<cArray->num; i++) {
    v = cArray->space[i];
    SATflags(v) &= ResetVisitedMask;
    elem = &(head->elemHead[elemIndex]);
    sat_ArrayInsert(head->elemArray, (long)elem);
    elem->node = v;
    elem->order = elemIndex++;

    size = SATnumLits(v);
    elem->support = sat_ArrayAlloc(size);
    plit = (long *)SATfirstLit(v);
    for(j=0; j<size; j++, plit++) {
      v = SATgetNode(*plit);
      inverted = SATisInverted(v);
      v = SATnormalNode(v);
      value = SATvalue(v) ^ inverted;
      if(value == 0)    {
        continue;
      }
      varId = head->edge2vid[SATnodeID(v)];
      lvar = &(head->varHead[varId]);

      sat_ArrayInsert(lvar->clauses, (long)elem);
      if(inverted)      lvar = (satLinearVar_t *)SATnot((unsigned long)lvar);
      sat_ArrayInsert(elem->support, (long)lvar);
    }
  }
  return(head);
}


satLinearCluster_t *
sat_CreateCluster(
        satLinearHead_t *head,
        satLinearElem_t *e1,
        satLinearElem_t *e2,
        int flagIndex,
        int *idArr)
{
satLinearCluster_t *clu;
satLinearVar_t *var;
satArray_t *support, *deadArray;
int from, to, nDead;
int nv, bddid;
int overlap, bddsize, j;

  memset(idArr, 0, sizeof(int)*(head->nVars));
  clu = ALLOC(satLinearCluster_t, 1);
  clu->elem1 = e1;
  clu->elem2 = e2;
  clu->deadArray = 0;
  from = e1->order;
  to = e2->order;
  nDead = 0;
  support = e1->support;
  for(j=0; j<support->num; j++) {
    var = (satLinearVar_t *)support->space[j];
    var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
    nv = var->node;
    bddid = head->edge2id[SATnodeID(nv)];
    idArr[bddid] = 1;

    if(var->bQuantified && from <= var->from && var->to <= to) {
      nDead++;
      if(clu->deadArray == 0) {
        deadArray = sat_ArrayAlloc(2);
        clu->deadArray = deadArray;
      }
      else
        deadArray = clu->deadArray;
      sat_ArrayInsert(deadArray, (long)var);
    }
  }

  overlap = 0;
  support = e2->support;
  for(j=0; j<support->num; j++) {
    var = (satLinearVar_t *)support->space[j];
    var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
    nv = var->node;
    bddid = head->edge2id[SATnodeID(nv)];
    if(idArr[bddid]) {
      if(from <= var->from && var->to <= to);
      else
        overlap++;
    }
    else {
      if(var->bQuantified && from <= var->from && var->to <= to) {
        nDead++;
        if(clu->deadArray == 0) {
          deadArray = sat_ArrayAlloc(2);
          clu->deadArray = deadArray;
        }
        else
          deadArray = clu->deadArray;
        sat_ArrayInsert(deadArray, (long)var);
      }
    }
  }

  bddsize = Cudd_DagSize(e1->bdd) + Cudd_DagSize(e2->bdd);
  clu->overlap = overlap;
  clu->cost = (nDead<<7) + (overlap*(1024/bddsize)) + 10000/bddsize;
  clu->flag = flagIndex;

  return(clu);
}

static void
sat_PrintSupportVariable(
        satLinearHead_t *head,
        satLinearElem_t *e1)
{
satArray_t *support;
satLinearVar_t *var;
int j;
long nv;


  support = e1->support;
  for(j=0; j<support->num; j++) {
    var = (satLinearVar_t *)support->space[j];
    var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
    nv = var->node;
    fprintf(stdout, " %ld", nv);
  }
  fprintf(stdout, "\n");
}

static int
heapCostCompare(const void *c1, const void *c2)
{
satLinearCluster_t *clu1, *clu2;

  clu1 = (satLinearCluster_t *)c1;
  clu2 = (satLinearCluster_t *)c2;
  return(clu1->cost < clu2->cost);
}

static void
sat_ClusteringGetCandidate(
        satManager_t *cm,
        satLinearHead_t *head)
{
int i, *idArr;
satArray_t *eArr;
satLinearElem_t *e1, *e2;
satLinearCluster_t *clu;

  eArr = head->elemArray;
  head->heap = Heap_HeapInitCompare(eArr->num+2, heapCostCompare);

  idArr = ALLOC(int, head->nVars);
  for(i=0; i<eArr->num; i++) {

    e1 = (satLinearElem_t *)eArr->space[i];
    if(i == eArr->num-1)
      continue;
    else
      e2 = (satLinearElem_t *)eArr->space[i+1];

    e1->flag = 1;
    e2->flag = 1;
    clu = sat_CreateCluster(head, e1, e2, 1, idArr);

    Heap_HeapInsertCompare(head->heap, (void *)clu, (long)clu);
  }

  free(idArr);

}

static DdNode *
sat_SmoothWithDeadVariable(
        DdManager *mgr,
        satArray_t *deadArray,
        DdNode *bdd1,
        DdNode *bdd2,
        int bddAndLimit)
{
satLinearVar_t *var;
DdNode *cube, *ncube;
DdNode *result;
int i;


  cube = DD_ONE(mgr);
  cuddRef(cube);
  for(i=0; i<deadArray->num; i++) {
    var = (satLinearVar_t *)deadArray->space[i];
    ncube = Cudd_bddAnd(mgr,cube,var->bdd);
    if(ncube == NULL) {
      Cudd_RecursiveDeref(mgr, cube);
      return(NULL);
    }
    cuddRef(ncube);
    Cudd_RecursiveDeref(mgr, cube);
    cube = ncube;
  }


  result = Cudd_bddAndAbstractLimit(
              mgr,bdd1,bdd2,cube,bddAndLimit);
  if(result == NULL) {
    Cudd_RecursiveDeref(mgr, cube);
    return(NULL);
  }
  cuddRef(result);
  Cudd_RecursiveDeref(mgr, cube);
  cuddDeref(result);

  return(result);
}

static int
sat_ClusteringElement(
        satManager_t *cm,
        satLinearHead_t *head)
{
int modified, total, size;
int found, i, vid, index;
long v;
int *idArr, *idSupport;
int limit, nElem;
satLinearElem_t *e1, *e2;
satLinearVar_t *lvar;
satLinearCluster_t *clu, *tclu;
satArray_t *support, *deadArray;
satArray_t *neArr, *eArr;
DdManager *mgr;
DdNode *result, *zero;
Heap_t *heap;
long dummy;

  heap = head->heap;
  modified = 0;

  idArr = ALLOC(int, head->nVars);

  mgr = head->mgr;
  eArr = head->elemArray;
  zero = Cudd_Not(DD_ONE(mgr));
  limit = ((eArr->num)>>1);
  nElem = eArr->num;

  if(cm->option->verbose > 3)
    fprintf(cm->stdOut, " ------- %d element\n", nElem);

  while(Heap_HeapExtractMin(heap, &clu, &dummy)) {
    if(modified > limit) {
      sat_FreeCluster(mgr, clu);
      continue;
    }
    e1 = clu->elem1;
    e2 = clu->elem2;
    if(e1->flag == 0 || e2->flag == 0) {
      sat_FreeCluster(mgr, clu);
      continue;
    }
    if(e1->flag > clu->flag || e2->flag > clu->flag) {
      sat_FreeCluster(mgr, clu);
      continue;
    }
    deadArray = clu->deadArray;
    if(deadArray) {
      cuddRef(e1->bdd);
      cuddRef(e2->bdd);
      result = sat_SmoothWithDeadVariable(
              mgr, deadArray, e1->bdd, e2->bdd, head->bddAndLimit);
      if(result)
        cuddRef(result);
      Cudd_RecursiveDeref(mgr, e1->bdd);
      Cudd_RecursiveDeref(mgr, e2->bdd);
      for(i=0; i<deadArray->num; i++) {
        lvar = (satLinearVar_t *)deadArray->space[i];
        sat_ArrayInsert(head->deadArray, (long)lvar);
      }
    }
    else {
      result = Cudd_bddAndLimit(mgr,e1->bdd,e2->bdd,head->bddAndLimit);
      if(result)
        cuddRef(result);
    }

    total = Cudd_ReadKeys(mgr) - Cudd_ReadDead(mgr);
    if(total > 100000 && head->reordering) {
      head->reordering = 0;
      Cudd_AutodynDisable(mgr);
    }

    if(result) {
      nElem--;
      if(cm->option->verbose > 3) {
        fprintf(cm->stdOut, " (%4d %4d) %4d(%3d, %3ld): %d X %d = %d\n",
              e1->order, e2->order,
              clu->cost, clu->overlap, deadArray ? deadArray->num : 0,
              Cudd_DagSize(e1->bdd), Cudd_DagSize(e2->bdd),
              Cudd_DagSize(result));
        sat_PrintSupportVariable(head, e1);
        sat_PrintSupportVariable(head, e2);
        if(deadArray) {
        for(i=0; i<deadArray->num; i++) {
          lvar = (satLinearVar_t *)deadArray->space[i];
          fprintf(cm->stdOut, "%ld ", lvar->node);
        }
        }
        fprintf(cm->stdOut, "\n");
      }
      modified++;
      e1->flag += 1;
      e2->flag = 0;

      if(nElem < 50) {
        sat_ArrayInsert(head->latestClusterArray, (long)(e1->bdd));
        cuddRef(e1->bdd);
        sat_ArrayInsert(head->latestClusterArray, (long)(e2->bdd));
        cuddRef(e2->bdd);
      }

      Cudd_RecursiveDeref(mgr, e1->bdd);
      Cudd_RecursiveDeref(mgr, e2->bdd);
      e1->bdd = result;
      e2->bdd = 0;
      sat_ArrayFree(e1->support);
      e1->support = 0;
      support = e2->support;
      for(i=0; i<support->num; i++) {
        lvar = (satLinearVar_t *)support->space[i];
        if(lvar->to == e2->order)
          lvar->to = e1->order;
        if(lvar->from == e2->order)
          lvar->from = e1->order;
      }
      sat_ArrayFree(e2->support);
      e2->support = 0;

      size = (unsigned int)Cudd_ReadSize(mgr);
      idSupport = Cudd_SupportIndex(mgr,result);
      e1->support = support = sat_ArrayAlloc(10);
      for (i = 0; i < size; i++) {
        if(idSupport[i]) {
          v = head->id2edge[i];
          vid = head->edge2vid[SATnodeID(v)];
          lvar = &(head->varHead[vid]);
          sat_ArrayInsert(support, (long)lvar);
        }
      }
      free(idSupport);

      found = 0;
      for(i=e1->order-1; i>=0; i--)  {
        e2 = (satLinearElem_t *)eArr->space[i];
        if(e2->flag)    {
          found = 1;
          break;
        }
      }
      if(found) {
        tclu = sat_CreateCluster(head, e2, e1, e1->flag, idArr);
        Heap_HeapInsertCompare(head->heap, (void *)tclu, (long)tclu);
      }

      found = 0;
      for(i=e1->order+1; i<eArr->num; i++)  {
        e2 = (satLinearElem_t *)eArr->space[i];
        if(e2->flag)    {
          found = 1;
          break;
        }
      }
      if(found) {
        tclu = sat_CreateCluster(head, e1, e2, e1->flag, idArr);
        Heap_HeapInsertCompare(head->heap, (void *)tclu, (long)tclu);
      }
    }
    sat_FreeCluster(mgr, clu);
  }

  Heap_HeapFree(heap);
  head->heap = 0;

  free(idArr);

  if(modified) {
    eArr = head->elemArray;
    neArr = sat_ArrayAlloc(eArr->num);
    index = 0;
    for(i=0; i<eArr->num; i++) {
      e1 = (satLinearElem_t *)eArr->space[i];
      if(e1->flag == 0) continue;

      e1->order = index++;
      sat_ArrayInsert(neArr, (long)e1);
    }
    sat_ArrayFree(eArr);
    head->elemArray = neArr;
  }

  if(head->elemArray->num == 1)
    modified = 0;

  return(modified);
}


static void
sat_FreeCluster(DdManager *mgr, satLinearCluster_t *clu)
{
satArray_t *deadArray;

  deadArray = clu->deadArray;
  if(deadArray) {
    sat_ArrayFree(deadArray);
  }
  free(clu);
}


static void
sat_CheckDeadNode(
        satLinearHead_t *head,
        satLinearCluster_t *clu)
{
satArray_t *deadArray, *eArr;
satArray_t *support;
satLinearVar_t *var, *tvar;
satLinearElem_t *elem;
int i, j, k;


  if(clu->deadArray) {
    deadArray = clu->deadArray;
    for(i=0; i<deadArray->num; i++) {
      var = (satLinearVar_t *)deadArray->space[i];
      eArr = head->elemArray;
      for(j=0; j<var->from; j++) {
        elem = (satLinearElem_t *)eArr->space[j];
        if(elem->flag == 0)     continue;
        support = elem->support;
        for(k=0; k<support->num; k++) {
          tvar = (satLinearVar_t *)support->space[k];
          tvar = (satLinearVar_t *)SATnormalNode((unsigned long)tvar);
          if(var == tvar) {
            fprintf(stdout, "Error : wrong variable range\n");
          }
        }
      }
      for(j=var->to+1; j<eArr->num; j++) {
        elem = (satLinearElem_t *)eArr->space[j];
        if(elem->flag == 0)     continue;
        support = elem->support;
        for(k=0; k<support->num; k++) {
          tvar = (satLinearVar_t *)support->space[k];
          tvar = (satLinearVar_t *)SATnormalNode((unsigned long)tvar);
          if(var == tvar) {
            fprintf(stdout, "Error : wrong variable range\n");
          }
        }
      }
    }
  }
}

static int
sat_ConvertCNF2BDD(
        satManager_t *cm,
        DdManager *mgr,
        int conflictFlag)
{
satLinearHead_t *head;
DdNode *result, *cube;
DdNode *l1, *l2;
DdNode *nl1, *nl2;
satArray_t *satArr, *arr;
int limitCut;
int flag, length;
int cut, i;

  head = sat_CreateLinearHead(cm, conflictFlag);

  if(head == 0) return(0);

  head->mgr = mgr;

  sat_GetArrangementByForce(cm, head);

  if(cm->option->verbose > 3)
    cut = sat_PrintCutProfile(cm, head, "final", 1);
  else
    cut = sat_PrintCutProfile(cm, head, "final", 0);

  if(conflictFlag)
    limitCut = cm->option->maxLimitOfCutSizeForBDDDPLL;
  else
    limitCut = cm->option->maxLimitOfCutSizeForMonolithicBDD;
  if(cut > limitCut) {
    sat_FreeLinearHead(head);
    return(SAT_BDD_BACKTRACK);
  }

  flag = sat_ClusteringElementMain(cm, head);

  if(flag == SAT_BDD_SAT) {
    arr = head->latestClusterArray;
    satArr = sat_ArrayAlloc(16);
    for(i=arr->num-1; i>=0; i--) {
      l1 = (DdNode *)arr->space[i];
      i--;
      l2 = (DdNode *)arr->space[i];
      nl1 = sat_CofactorBDDArray(head, mgr, l1, satArr);
      nl2 = sat_CofactorBDDArray(head, mgr, l2, satArr);
      result = Cudd_bddAndLimit(mgr, nl1, nl2, head->bddAndLimit);
      cuddRef(result);
      Cudd_RecursiveDeref(mgr, nl1);
      Cudd_RecursiveDeref(mgr, nl2);
      cube = Cudd_LargestCube(mgr, result, &length);
      cuddRef(cube);
      sat_ExtractAssignmentFromBDD(head, mgr, satArr, cube);
      Cudd_RecursiveDeref(mgr, cube);
      Cudd_RecursiveDeref(mgr, result);
    }
    cm->assignByBDD = satArr;
  }
  sat_FreeLinearHead(head);

  return(flag);
}

static void
sat_FreeLinearHead(satLinearHead_t *head)
{
satLinearElem_t *elem;
satLinearVar_t *var;
satArray_t *eArr, *vArr, *arr;
satArray_t *support, *clauses;
DdNode *bdd;
int i;

  eArr = head->elemArray;
  if(eArr) {
    for(i=0; i<eArr->num; i++) {
      elem = (satLinearElem_t *)(eArr->space[i]);
      support = elem->support;
      if(support)
        sat_ArrayFree(support);
      if(elem->bdd)
        Cudd_RecursiveDeref(head->mgr, elem->bdd);
    }
  }
  vArr = head->varArray;
  if(vArr) {
    for(i=0; i<vArr->num; i++) {
      var = (satLinearVar_t *)vArr->space[i];
      clauses = var->clauses;
      if(clauses)
        sat_ArrayFree(clauses);
      if(var->bdd)
        Cudd_RecursiveDeref(head->mgr, var->bdd);
    }
  }

  if(head->variablesArray)
    sat_ArrayFree(head->variablesArray);
  if(head->clausesArray)
    sat_ArrayFree(head->clausesArray);

  if(head->elemHead)
    free(head->elemHead);
  if(head->varHead)
    free(head->varHead);
  if(head->id2edge)
    free(head->id2edge);
  if(head->edge2id)
    free(head->edge2id);
  if(head->edge2vid)
    free(head->edge2vid);

  if(head->latestClusterArray)  {
    arr = head->latestClusterArray;
    for(i=0; i<arr->num; i++) {
      bdd = (DdNode *)arr->space[i];
      Cudd_RecursiveDeref(head->mgr, bdd);
    }
    sat_ArrayFree(arr);
    head->latestClusterArray = 0;
  }

  if(head->deadArray)
    free(head->deadArray);
  free(head);
}


static int
linearVarCompare(
  const void * node1,
  const void * node2)
{
  satLinearVar_t *d1;
  satLinearVar_t *d2;

  d1 = *(satLinearVar_t **)(node1);
  d2 = *(satLinearVar_t **)(node2);

  return (d1->pos > d2->pos);
}

static int
linearElemCompare(
  const void * node1,
  const void * node2)
{
  satLinearElem_t *d1;
  satLinearElem_t *d2;

  d1 = *(satLinearElem_t **)(node1);
  d2 = *(satLinearElem_t **)(node2);

  return (d1->pos > d2->pos);
}

static void
sat_GetArrangementByForce(
        satManager_t *cm,
        satLinearHead_t *head)
{
int iteration;
double prespan, span;
int from, to, sum;
int i, j, inverted;
satLinearElem_t *elem;
satLinearVar_t *var;
satArray_t *eArr, *vArr;
satArray_t *support, *clauses;

  iteration = 0;
  prespan = MAXINT;
  eArr = head->elemArray;
  vArr = head->varArray;
  while(1) {
    iteration++;
    if(iteration > 200) break;

    span = 0;
    for(i=0; i<eArr->num; i++) {
      elem = (satLinearElem_t *)(eArr->space[i]);
      support = elem->support;
      sum = 0;
      from = MAXINT;
      to = -1;
      for(j=0; j<support->num; j++) {
        var = (satLinearVar_t *)(support->space[j]);
        inverted = SATisInverted((unsigned long)var);
        var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
        sum += var->order;
        if(var->order < from)   from = var->order;
        if(to < var->order)     to = var->order;
      }
      if(from != MAXINT && to != -1)
        span += (double)(to - from);
      elem->pos = sum / (double)(support->num);
    }

    if(iteration > 2 && (prespan * 0.9999) < span)
      break;
    prespan = span;

    qsort(eArr->space, eArr->num, sizeof(satLinearElem_t *), linearElemCompare);
    for(i=0; i<eArr->num; i++) {
      elem = (satLinearElem_t *)eArr->space[i];
      elem->order = i;
    }

    for(i=0; i<vArr->num; i++) {
      var = (satLinearVar_t *)vArr->space[i];
      clauses = var->clauses;
      sum = 0;
      for(j=0; j<clauses->num; j++) {
        elem = (satLinearElem_t *)clauses->space[j];
        sum += elem->order;
      }
      var->pos = sum / (double)(clauses->num);
    }

    qsort(vArr->space, vArr->num, sizeof(satLinearVar_t *), linearVarCompare);
    for(i=0; i<vArr->num; i++) {
      var = (satLinearVar_t *)vArr->space[i];
      var->order = i;
    }
  }
  if(cm->option->verbose > 3)
    fprintf(cm->stdOut, "NOTICE : %d iteration for force based arrangement\n", iteration);
}

static int
sat_PrintCutProfile(
        satManager_t *cm,
        satLinearHead_t *head,
        char *baseName,
        int printFlag)
{
st_table *cutTable;
st_generator *gen;
FILE *fout = NIL(FILE);
int i, j, cut, sum;
int to, from;
char filename[1024];
satArray_t *support, *clauses, *eArr, *vArr;
satLinearElem_t *elem;
satLinearVar_t *var;
double span;

  eArr = head->elemArray;
  span = 0;
  for(i=0; i<eArr->num; i++) {
    elem = (satLinearElem_t *)eArr->space[i];
    support = elem->support;
    sum = 0;
    to = -1;
    from = MAXINT;
    for(j=0; j<support->num; j++) {
      var = (satLinearVar_t *)support->space[j];
      var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
      sum += var->order;
      if(to < var->order)       to = var->order;
      if(var->order < from)     from = var->order;
    }
    elem->to = to;
    if(from != MAXINT && to != -1)
      span += (double)(to - from);
  }

  cut = 0;
  if(printFlag) {
    sprintf(filename, "%s.data", baseName);
    fout = fopen(filename, "w");
  }
  cutTable = st_init_table(st_ptrcmp, st_ptrhash);
  vArr = head->varArray;
  for(i=0; i<vArr->num; i++) {
    var = (satLinearVar_t *)vArr->space[i];
    clauses = var->clauses;
    for(j=0; j<clauses->num; j++) {
      elem = (satLinearElem_t *)clauses->space[j];
      st_insert(cutTable, (char *)elem, (char *)elem);
    }
    st_foreach_item(cutTable, gen, &elem, &elem) {
      if(elem->to <= i)
        st_delete(cutTable, &elem, NIL(char *));
    }
    if(cut < cutTable->num_entries)
      cut = cutTable->num_entries;
    if(printFlag)
      fprintf(fout, "%d %d\n", i, cutTable->num_entries);
  }
  st_free_table(cutTable);

  if(printFlag) {
    fclose(fout);
    sprintf(filename, "%s.gnu", baseName);
    fout = fopen(filename, "w");
    fprintf(fout, "set terminal postscript \n");
    fprintf(fout, "set output \"%s.ps\"\n", baseName);
    fprintf(fout, "set title \"profile of live variable span %f cut %d\"\n",
            span, cut);
    fprintf(fout, "plot \"%s.data\" using 1:2 title \"%s\" with lines\n", baseName, "cut");
    fclose(fout);
  }

  return cut;

}

static int
sat_ClusteringElementMain(
        satManager_t *cm,
        satLinearHead_t *head)
{
int modified;
satLinearElem_t *elem;
DdNode *one;

  Cudd_AutodynEnable(head->mgr, CUDD_REORDER_SIFT);

  sat_InitClusteringElement(cm, head);

  while(1) {
    sat_ComputeVariableRange(cm, head);
    sat_ClusteringGetCandidate(cm, head);
    modified = sat_ClusteringElement(cm, head);
    if(modified == 0)   break;
  }

  if(head->elemArray->num == 1) {
    one = DD_ONE(head->mgr);
    elem = (satLinearElem_t *)(head->elemArray->space[0]);
    if(elem->bdd == one)                return(SAT_BDD_SAT);
    else if(elem->bdd == Cudd_Not(one)) return(SAT_BDD_UNSAT);
    else                                return(SAT_BDD_BACKTRACK);
  }
  else {
    return(SAT_BDD_BACKTRACK);
  }
}

static void
sat_ComputeVariableRange(
        satManager_t *cm,
        satLinearHead_t *head)
{
satArray_t *support, *vArr, *eArr;
satLinearElem_t *elem;
satLinearVar_t *var;
int i, j;

  vArr = head->varArray;
  eArr = head->elemArray;

  for(i=0; i<vArr->num; i++) {
    var = (satLinearVar_t *)vArr->space[i];
    var->from = MAXINT;
    var->to = -1;
  }

  for(i=0; i<eArr->num; i++) {
    elem = (satLinearElem_t *)eArr->space[i];
    support = elem->support;
    for(j=0; j<support->num; j++) {
      var = (satLinearVar_t *)support->space[j];
      var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
      if(elem->order < var->from)       var->from = elem->order;
      if(var->to < elem->order)         var->to = elem->order;
    }
  }
}

static void
sat_InitClusteringElement(
        satManager_t *cm,
        satLinearHead_t *head)
{
DdNode *sum, *nsum, *one;
DdManager *mgr;
satLinearElem_t *elem;
satLinearVar_t *var;
satArray_t *support, *vArr, *eArr;
int i, j, index;
long nv;
int inverted;

  mgr = head->mgr;
  vArr = head->varArray;
  eArr = head->elemArray;
  index = 0;
  one = DD_ONE(mgr);

  for(i=0; i<vArr->num; i++) {
    var = (satLinearVar_t *)vArr->space[i];
    nv = var->node;
    head->id2edge[index] = nv;
    head->edge2id[SATnodeID(nv)] = index;
    var->bdd = cuddUniqueInter(mgr,index,one,Cudd_Not(one));
    cuddRef(var->bdd);
    index++;
  }

  for(i=0; i<eArr->num; i++) {
    elem = (satLinearElem_t *)eArr->space[i];
    support = elem->support;
    sum = Cudd_Not(one);
    cuddRef(sum);
    for(j=0; j<support->num; j++) {
      var = (satLinearVar_t *)support->space[j];
      inverted = SATisInverted((unsigned long)var);
      var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
      nsum = Cudd_bddAnd(mgr,Cudd_Not(sum),
                             (inverted ? var->bdd : Cudd_Not(var->bdd)));
      nsum = Cudd_Not(nsum);
      cuddRef(nsum);

      Cudd_RecursiveDeref(mgr,sum);
      sum = nsum;
    }
    elem->bdd = sum;
  }
}

#endif
#ifndef BDDcu

void
sat_TryToBuildMonolithicBDD(satManager_t *cm)
{
  fprintf(stderr, "Warning : This feature is only availabe with CUDD package\n");
  return;
}
#endif