source: vis_dev/vis-2.3/src/sat/satBDD.c @ 40

Last change on this file since 40 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 35.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [satBDD.c]
4
5  PackageName [sat]
6
7  Synopsis    [Routines for using BDD.]
8
9  Author      [HoonSang Jin]
10
11  Copyright [ This file was created at the University of Colorado at
12  Boulder.  The University of Colorado at Boulder makes no warranty
13  about the suitability of this software for any purpose.  It is
14  presented on an AS IS basis.]
15
16
17******************************************************************************/
18
19#include "satInt.h"
20#ifdef BDDcu
21#include "cuddInt.h"
22#endif
23
24static char rcsid[] UNUSED = "$Id: satBDD.c,v 1.30 2009/04/11 18:26:37 fabio Exp $";
25
26/*---------------------------------------------------------------------------*/
27/* Constant declarations                                                     */
28/*---------------------------------------------------------------------------*/
29
30#ifdef BDDcu
31/**AutomaticStart*************************************************************/
32
33/*---------------------------------------------------------------------------*/
34/* Static function prototypes                                                */
35/*---------------------------------------------------------------------------*/
36
37static int heapCostCompare(const void *c1, const void *c2);
38static int sat_ConvertCNF2BDD(satManager_t *cm, DdManager *mgr, int conflictFlag);
39static void sat_FreeLinearHead(satLinearHead_t *head);
40static int linearVarCompare(const void * node1, const void * node2);
41static int linearElemCompare(const void * node1, const void * node2);
42static void sat_GetArrangementByForce(satManager_t *cm, satLinearHead_t *head);
43static int sat_PrintCutProfile(satManager_t *cm, satLinearHead_t *head, char *baseName, int printFlag);
44static int sat_ClusteringElementMain(satManager_t *cm, satLinearHead_t *head);
45static void sat_ComputeVariableRange(satManager_t *cm, satLinearHead_t *head);
46static void sat_InitClusteringElement(satManager_t *cm, satLinearHead_t *head);
47static void sat_PrintSupportVariable(satLinearHead_t *head, satLinearElem_t *e1);
48static void sat_ClusteringGetCandidate(satManager_t *cm, satLinearHead_t *head);
49static DdNode *sat_SmoothWithDeadVariable(DdManager *mgr, satArray_t *deadArray, DdNode *bdd1, DdNode *bdd2, int bddAndLimit);
50static int sat_ClusteringElement(satManager_t *cm, satLinearHead_t *head);
51static void sat_FreeCluster(DdManager *mgr, satLinearCluster_t *clu);
52static void sat_CheckDeadNode(satLinearHead_t *head, satLinearCluster_t *clu);
53
54/**AutomaticEnd***************************************************************/
55#endif
56
57
58/*---------------------------------------------------------------------------*/
59/* Definition of exported functions                                          */
60/*---------------------------------------------------------------------------*/
61
62#ifdef BDDcu
63
64/**Function********************************************************************
65
66  Synopsis    [Build monolithic BDD.]
67
68  Description [Try to build a monolithic BDD from the set of clauses.
69               If it is succeeded then we can conclude whether given CNF is
70               satisfiable of not.]
71
72  SideEffects []
73
74  SeeAlso     []
75
76******************************************************************************/
77void
78sat_TryToBuildMonolithicBDD(satManager_t *cm)
79{
80DdManager *mgr;
81int nVariables, flag;
82
83  nVariables = cm->initNumVariables - cm->implicatedSoFar;
84
85  if(nVariables
86          > cm->option->maxLimitOfVariablesForMonolithicBDD)    return;
87
88  mgr = Cudd_Init((unsigned int)(nVariables+1), 0, CUDD_UNIQUE_SLOTS,
89                   CUDD_CACHE_SLOTS, getSoftDataLimit() / 10 * 9);
90  cm->mgr = mgr;
91  flag = sat_ConvertCNF2BDD(cm, mgr, 0);
92
93  Cudd_Quit(mgr);
94  cm->mgr = 0;
95
96  if(flag == SAT_BDD_UNSAT)
97    cm->status = SAT_UNSAT;
98
99  return;
100}
101
102
103/**Function********************************************************************
104
105  Synopsis    [Apply cofactoring to the set of BDDs.]
106
107  Description [Apply cofactoring to the set of BDDs.]
108
109  SideEffects []
110
111  SeeAlso     []
112
113******************************************************************************/
114DdNode *
115sat_CofactorBDDArray(
116        satLinearHead_t *head,
117        DdManager *mgr,
118        DdNode *l1,
119        satArray_t *satArr)
120{
121int i, vid, inverted;
122long v;
123DdNode *bdd, *result, *nresult;
124satLinearVar_t *var;
125
126  result = l1;
127  cuddRef(result);
128  for(i=0; i<satArr->num; i++) {
129    v = satArr->space[i];
130    inverted = SATisInverted(v);
131    v = SATnormalNode(v);
132    vid = head->edge2vid[SATnodeID(v)];
133    var = &(head->varHead[vid]);
134    bdd = inverted ? Cudd_Not(var->bdd) : var->bdd;
135
136    nresult = Cudd_bddConstrain(mgr, result, bdd);
137    cuddRef(nresult);
138    Cudd_RecursiveDeref(mgr, result);
139    result = nresult;
140  }
141  return(result);
142}
143
144/**Function********************************************************************
145
146  Synopsis    [Extract satisfying assignment from BDD.]
147
148  Description [Since we quantify the variables if they are isolated,
149               the resulting BDD is ONE or ZERO. If BDD is ONE then the satisfying
150               assignments are extracted from the set of BDDs saved during clustering.]
151
152  SideEffects []
153
154  SeeAlso     []
155
156******************************************************************************/
157void
158sat_ExtractAssignmentFromBDD(
159        satLinearHead_t *head,
160        DdManager *mgr,
161        satArray_t *arr,
162        DdNode *cube)
163{
164DdNode *C, *T, *E, *zero;
165
166  C = Cudd_Regular(cube);
167  zero = Cudd_Not(DD_ONE(mgr));
168  if (!cuddIsConstant(C)) {
169    while (!cuddIsConstant(C)) {
170      T = cuddT(C);
171      E = cuddE(C);
172      if (Cudd_IsComplement(cube)) {
173        T = Cudd_Not(T);
174        E = Cudd_Not(E);
175      }
176      if (T == zero)  { /** T == 0 **/
177          sat_ArrayInsert(arr, ((head->id2edge[C->index]) + 1));
178          cube = E;
179      }
180      else {                   /** E == 0 **/
181          sat_ArrayInsert(arr, (head->id2edge[C->index]));
182          cube = T;
183      }
184      C = Cudd_Regular(cube);
185    }
186  }
187  return;
188}
189
190
191/**Function********************************************************************
192
193  Synopsis    [Create  satLinearHead_t structure.]
194
195  Description [Build initial data structure for linear arrangement and clustering.]
196
197  SideEffects []
198
199  SeeAlso     []
200
201******************************************************************************/
202satLinearHead_t *
203sat_CreateLinearHead(
204        satManager_t *cm,
205        int conflictFlag)
206{
207satLinearHead_t *head;
208satLinearElem_t *elem;
209satLinearVar_t *lvar;
210satArray_t *cArray, *vArray;
211int nVars, nCls, varId;
212int j, size, satisfied, inverted;
213int value;
214long v, *plit, i;
215int elemIndex, varIndex;
216int clauseLimit;
217
218  nVars = 0;
219  nCls = 0;
220  cArray = sat_ArrayAlloc(1024);
221  vArray = sat_ArrayAlloc(1024);
222  for(i=satNodeSize; i<cm->initNodesArraySize; i+=satNodeSize) {
223    if(!(SATflags(i) & IsCNFMask))      continue;
224    if(SATreadInUse(i) == 0)    continue;
225  /**  CONSIDER conflict clause...   **/
226    size = SATnumLits(i);
227    satisfied = 0;
228    plit = (long *)SATfirstLit(i);
229    for(j=0; j<size; j++, plit++) {
230      v = SATgetNode(*plit);
231      inverted = SATisInverted(v);
232      v = SATnormalNode(v);
233      value = SATvalue(v) ^ inverted;
234      if(value == 1) {
235        satisfied = 1;
236        break;
237      }
238    }
239    if(satisfied)       continue;
240
241    nCls++;
242    SATflags(i) |= VisitedMask;
243    sat_ArrayInsert(cArray, i);
244
245    plit = (long *)SATfirstLit(i);
246    for(j=0; j<size; j++, plit++) {
247      v = SATgetNode(*plit);
248      v = SATnormalNode(v);
249      if(SATvalue(v) < 2)       continue;
250      if(!(SATflags(v) & VisitedMask)) {
251        nVars++;
252        SATflags(v) |= VisitedMask;
253        sat_ArrayInsert(vArray, v);
254      }
255    }
256  }
257
258  if(conflictFlag)
259    clauseLimit = cm->option->maxLimitOfClausesForBDDDPLL;
260  else
261    clauseLimit = cm->option->maxLimitOfClausesForMonolithicBDD;
262
263  if(nCls > clauseLimit) {
264    if(nVars > 100) {
265      for(i=0; i<cArray->num; i++) {
266        v = cArray->space[i];
267        SATflags(v) &= ResetVisitedMask;
268      }
269      sat_ArrayFree(cArray);
270      for(i=0; i<vArray->num; i++) {
271        v = vArray->space[i];
272        SATflags(v) &= ResetVisitedMask;
273      }
274      sat_ArrayFree(vArray);
275      return(0);
276    }
277  }
278
279  if(cm->option->verbose > 1) {
280    fprintf(cm->stdOut, "NOTICE : Apply BDD based method at level %d with %d vars %d cls\n", cm->currentDecision, nVars, nCls);
281    fflush(cm->stdOut);
282  }
283  head = ALLOC(satLinearHead_t, 1);
284  memset(head, 0, sizeof(satLinearHead_t));
285  head->clausesArray = cArray;
286  head->variablesArray = vArray;
287  head->reordering = 1;
288  head->nVars = nVars;
289  head->nCls = nCls;
290  head->bddLimit = 5000;
291  head->bddAndLimit = 10000;
292
293  head->elemHead = ALLOC(satLinearElem_t, nCls);
294  memset(head->elemHead, 0, sizeof(satLinearElem_t)*nCls);
295  head->varHead = ALLOC(satLinearVar_t, nVars);
296  memset(head->varHead, 0, sizeof(satLinearVar_t)*nVars);
297
298  head->elemArray = sat_ArrayAlloc(nCls);
299  head->varArray = sat_ArrayAlloc(nVars);
300  head->latestClusterArray = sat_ArrayAlloc(32);
301  head->deadArray = sat_ArrayAlloc(nVars);
302
303  head->id2edge = ALLOC(long, nVars+1);
304  head->edge2id = ALLOC(int, cm->initNumVariables+1);
305  head->edge2vid = ALLOC(int, cm->initNumVariables+1);
306
307  varIndex = 0;
308  for(i=0; i<vArray->num; i++) {
309    v = vArray->space[i];
310    SATflags(v) &= ResetVisitedMask;
311    lvar = &(head->varHead[varIndex]);
312    head->edge2vid[SATnodeID(v)] = varIndex;
313    sat_ArrayInsert(head->varArray, (long)lvar);
314    lvar->order = varIndex++;
315    lvar->node = v;
316    lvar->bQuantified = 1;
317    lvar->clauses = sat_ArrayAlloc(4);
318  }
319
320  elemIndex = 0;
321  for(i=0; i<cArray->num; i++) {
322    v = cArray->space[i];
323    SATflags(v) &= ResetVisitedMask;
324    elem = &(head->elemHead[elemIndex]);
325    sat_ArrayInsert(head->elemArray, (long)elem);
326    elem->node = v;
327    elem->order = elemIndex++;
328
329    size = SATnumLits(v);
330    elem->support = sat_ArrayAlloc(size);
331    plit = (long *)SATfirstLit(v);
332    for(j=0; j<size; j++, plit++) {
333      v = SATgetNode(*plit);
334      inverted = SATisInverted(v);
335      v = SATnormalNode(v);
336      value = SATvalue(v) ^ inverted;
337      if(value == 0)    {
338        continue;
339      }
340      varId = head->edge2vid[SATnodeID(v)];
341      lvar = &(head->varHead[varId]);
342
343      sat_ArrayInsert(lvar->clauses, (long)elem);
344      if(inverted)      lvar = (satLinearVar_t *)SATnot((unsigned long)lvar);
345      sat_ArrayInsert(elem->support, (long)lvar);
346    }
347  }
348  return(head);
349}
350
351
352/**Function********************************************************************
353
354  Synopsis    [Create  satLinearCluster_t  for each clutering candidate]
355
356  Description [Create  satLinearCluster_t  for each clutering candidate]
357
358  SideEffects []
359
360  SeeAlso     []
361
362******************************************************************************/
363satLinearCluster_t *
364sat_CreateCluster(
365        satLinearHead_t *head,
366        satLinearElem_t *e1,
367        satLinearElem_t *e2,
368        int flagIndex,
369        int *idArr)
370{
371satLinearCluster_t *clu;
372satLinearVar_t *var;
373satArray_t *support, *deadArray;
374int from, to, nDead;
375int nv, bddid;
376int overlap, bddsize, j;
377
378  memset(idArr, 0, sizeof(int)*(head->nVars));
379  clu = ALLOC(satLinearCluster_t, 1);
380  clu->elem1 = e1;
381  clu->elem2 = e2;
382  clu->deadArray = 0;
383  from = e1->order;
384  to = e2->order;
385  nDead = 0;
386  support = e1->support;
387  for(j=0; j<support->num; j++) {
388    var = (satLinearVar_t *)support->space[j];
389    var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
390    nv = var->node;
391    bddid = head->edge2id[SATnodeID(nv)];
392    idArr[bddid] = 1;
393
394    if(var->bQuantified && from <= var->from && var->to <= to) {
395      nDead++;
396      if(clu->deadArray == 0) {
397        deadArray = sat_ArrayAlloc(2);
398        clu->deadArray = deadArray;
399      }
400      else
401        deadArray = clu->deadArray;
402      sat_ArrayInsert(deadArray, (long)var);
403    }
404  }
405
406  overlap = 0;
407  support = e2->support;
408  for(j=0; j<support->num; j++) {
409    var = (satLinearVar_t *)support->space[j];
410    var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
411    nv = var->node;
412    bddid = head->edge2id[SATnodeID(nv)];
413    if(idArr[bddid]) {
414      if(from <= var->from && var->to <= to);
415      else
416        overlap++;
417    }
418    else {
419      if(var->bQuantified && from <= var->from && var->to <= to) {
420        nDead++;
421        if(clu->deadArray == 0) {
422          deadArray = sat_ArrayAlloc(2);
423          clu->deadArray = deadArray;
424        }
425        else
426          deadArray = clu->deadArray;
427        sat_ArrayInsert(deadArray, (long)var);
428      }
429    }
430  }
431
432  bddsize = Cudd_DagSize(e1->bdd) + Cudd_DagSize(e2->bdd);
433  clu->overlap = overlap;
434  clu->cost = (nDead<<7) + (overlap*(1024/bddsize)) + 10000/bddsize;
435  clu->flag = flagIndex;
436
437  return(clu);
438}
439
440/**Function********************************************************************
441
442  Synopsis    [Print support variables of element(clause).]
443
444  Description [Print support variables of element(clause).]
445
446  SideEffects []
447
448  SeeAlso     []
449
450******************************************************************************/
451static void
452sat_PrintSupportVariable(
453        satLinearHead_t *head,
454        satLinearElem_t *e1)
455{
456satArray_t *support;
457satLinearVar_t *var;
458int j;
459long nv;
460
461
462  support = e1->support;
463  for(j=0; j<support->num; j++) {
464    var = (satLinearVar_t *)support->space[j];
465    var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
466    nv = var->node;
467/**    bddid = head->edge2id[SATnodeID(nv)]; **/
468    fprintf(stdout, " %ld", nv);
469  }
470  fprintf(stdout, "\n");
471}
472
473/**Function********************************************************************
474
475  Synopsis    [Compare function for heapify]
476
477  Description [Compare function for heapify]
478
479  SideEffects []
480
481  SeeAlso     []
482
483******************************************************************************/
484static int
485heapCostCompare(const void *c1, const void *c2)
486{
487satLinearCluster_t *clu1, *clu2;
488
489  clu1 = (satLinearCluster_t *)c1;
490  clu2 = (satLinearCluster_t *)c2;
491  return(clu1->cost < clu2->cost);
492}
493
494/**Function********************************************************************
495
496  Synopsis    [Create initial clustering candidates]
497
498  Description [Create initial clustering candidates]
499
500  SideEffects []
501
502  SeeAlso     []
503
504******************************************************************************/
505static void
506sat_ClusteringGetCandidate(
507        satManager_t *cm,
508        satLinearHead_t *head)
509{
510int i, *idArr;
511satArray_t *eArr;
512satLinearElem_t *e1, *e2;
513satLinearCluster_t *clu;
514
515  eArr = head->elemArray;
516  head->heap = Heap_HeapInitCompare(eArr->num+2, heapCostCompare);
517
518  idArr = ALLOC(int, head->nVars);
519  for(i=0; i<eArr->num; i++) {
520
521    e1 = (satLinearElem_t *)eArr->space[i];
522    if(i == eArr->num-1)
523      continue;
524    else
525      e2 = (satLinearElem_t *)eArr->space[i+1];
526
527    e1->flag = 1;
528    e2->flag = 1;
529    clu = sat_CreateCluster(head, e1, e2, 1, idArr);
530
531    Heap_HeapInsertCompare(head->heap, (void *)clu, (long)clu);
532  }
533
534  free(idArr);
535
536}
537
538/**Function********************************************************************
539
540  Synopsis    [Apply existential qunatification for cluster.]
541
542  Description [Apply existential qunatification for cluster.]
543
544  SideEffects []
545
546  SeeAlso     []
547
548******************************************************************************/
549static DdNode *
550sat_SmoothWithDeadVariable(
551        DdManager *mgr,
552        satArray_t *deadArray,
553        DdNode *bdd1,
554        DdNode *bdd2,
555        int bddAndLimit)
556{
557satLinearVar_t *var;
558DdNode *cube, *ncube;
559DdNode *result;
560int i;
561
562
563  cube = DD_ONE(mgr);
564  cuddRef(cube);
565  for(i=0; i<deadArray->num; i++) {
566    var = (satLinearVar_t *)deadArray->space[i];
567    ncube = Cudd_bddAnd(mgr,cube,var->bdd);
568    if(ncube == NULL) {
569      Cudd_RecursiveDeref(mgr, cube);
570      return(NULL);
571    }
572    cuddRef(ncube);
573    Cudd_RecursiveDeref(mgr, cube);
574    cube = ncube;
575  }
576
577
578  result = Cudd_bddAndAbstractLimit(
579              mgr,bdd1,bdd2,cube,bddAndLimit);
580  if(result == NULL) {
581    Cudd_RecursiveDeref(mgr, cube);
582    return(NULL);
583  }
584  cuddRef(result);
585  Cudd_RecursiveDeref(mgr, cube);
586  cuddDeref(result);
587
588  return(result);
589}
590
591/**Function********************************************************************
592
593  Synopsis    [Apply clustering.]
594
595  Description [Apply clustering.]
596
597  SideEffects []
598
599  SeeAlso     []
600
601******************************************************************************/
602static int
603sat_ClusteringElement(
604        satManager_t *cm,
605        satLinearHead_t *head)
606{
607int modified, total, size;
608int found, i, vid, index;
609long v;
610int *idArr, *idSupport;
611int limit, nElem;
612satLinearElem_t *e1, *e2;
613satLinearVar_t *lvar;
614satLinearCluster_t *clu, *tclu;
615satArray_t *support, *deadArray;
616satArray_t *neArr, *eArr;
617DdManager *mgr;
618DdNode *result, *zero;
619Heap_t *heap;
620long dummy;
621
622  heap = head->heap;
623  modified = 0;
624
625  idArr = ALLOC(int, head->nVars);
626
627  mgr = head->mgr;
628  eArr = head->elemArray;
629  /**
630  if(eArr->num <= 5 && head->reordering)
631    Cudd_ReduceHeap(mgr,mgr->autoMethod,10);
632    **/
633
634  zero = Cudd_Not(DD_ONE(mgr));
635  limit = ((eArr->num)>>1);
636  nElem = eArr->num;
637
638  if(cm->option->verbose > 3)
639    fprintf(cm->stdOut, " ------- %d element\n", nElem);
640
641  while(Heap_HeapExtractMin(heap, &clu, &dummy)) {
642    if(modified > limit) {
643      sat_FreeCluster(mgr, clu);
644      continue;
645    }
646    e1 = clu->elem1;
647    e2 = clu->elem2;
648    if(e1->flag == 0 || e2->flag == 0) {
649      sat_FreeCluster(mgr, clu);
650      continue;
651    }
652    if(e1->flag > clu->flag || e2->flag > clu->flag) {
653      sat_FreeCluster(mgr, clu);
654      continue;
655    }
656    deadArray = clu->deadArray;
657    if(deadArray) {
658      cuddRef(e1->bdd);
659      cuddRef(e2->bdd);
660      result = sat_SmoothWithDeadVariable(
661              mgr, deadArray, e1->bdd, e2->bdd, head->bddAndLimit);
662      if(result)
663        cuddRef(result);
664      Cudd_RecursiveDeref(mgr, e1->bdd);
665      Cudd_RecursiveDeref(mgr, e2->bdd);
666      for(i=0; i<deadArray->num; i++) {
667        lvar = (satLinearVar_t *)deadArray->space[i];
668        sat_ArrayInsert(head->deadArray, (long)lvar);
669      }
670    }
671    else {
672      result = Cudd_bddAndLimit(mgr,e1->bdd,e2->bdd,head->bddAndLimit);
673      if(result)
674        cuddRef(result);
675    }
676
677    total = Cudd_ReadKeys(mgr) - Cudd_ReadDead(mgr);
678    if(total > 100000 && head->reordering) {
679      head->reordering = 0;
680      Cudd_AutodynDisable(mgr);
681    }
682
683    if(result) {
684        /**  CONSIDER the case that result is DD_ZERO... **/
685      nElem--;
686      if(cm->option->verbose > 3) {
687        fprintf(cm->stdOut, " (%4d %4d) %4d(%3d, %3ld): %d X %d = %d\n",
688              e1->order, e2->order,
689              clu->cost, clu->overlap, deadArray ? deadArray->num : 0,
690              Cudd_DagSize(e1->bdd), Cudd_DagSize(e2->bdd),
691              Cudd_DagSize(result));
692        sat_PrintSupportVariable(head, e1);
693        sat_PrintSupportVariable(head, e2);
694        if(deadArray) {
695        for(i=0; i<deadArray->num; i++) {
696          lvar = (satLinearVar_t *)deadArray->space[i];
697          fprintf(cm->stdOut, "%ld ", lvar->node);
698        }
699        }
700        fprintf(cm->stdOut, "\n");
701      }
702      modified++;
703      e1->flag += 1;
704      e2->flag = 0;
705
706      if(nElem < 50) {
707        sat_ArrayInsert(head->latestClusterArray, (long)(e1->bdd));
708        cuddRef(e1->bdd);
709        sat_ArrayInsert(head->latestClusterArray, (long)(e2->bdd));
710        cuddRef(e2->bdd);
711      }
712
713      Cudd_RecursiveDeref(mgr, e1->bdd);
714      Cudd_RecursiveDeref(mgr, e2->bdd);
715      e1->bdd = result;
716      e2->bdd = 0;
717      sat_ArrayFree(e1->support);
718      e1->support = 0;
719      support = e2->support;
720      for(i=0; i<support->num; i++) {
721        lvar = (satLinearVar_t *)support->space[i];
722        if(lvar->to == e2->order)
723          lvar->to = e1->order;
724        if(lvar->from == e2->order)
725          lvar->from = e1->order;
726      }
727      sat_ArrayFree(e2->support);
728      e2->support = 0;
729
730      size = (unsigned int)Cudd_ReadSize(mgr);
731      idSupport = Cudd_SupportIndex(mgr,result);
732      e1->support = support = sat_ArrayAlloc(10);
733      for (i = 0; i < size; i++) {
734        if(idSupport[i]) {
735          v = head->id2edge[i];
736          vid = head->edge2vid[SATnodeID(v)];
737          lvar = &(head->varHead[vid]);
738          sat_ArrayInsert(support, (long)lvar);
739          /**
740          if(lvar->to == e2->order)
741            lvar->to = e1->order;
742          if(lvar->from == e2->order)
743            lvar->from = e1->order;
744            **/
745        }
746      }
747      free(idSupport);
748
749      found = 0;
750      for(i=e1->order-1; i>=0; i--)  {
751        e2 = (satLinearElem_t *)eArr->space[i];
752        if(e2->flag)    {
753          found = 1;
754          break;
755        }
756      }
757      if(found) {
758        tclu = sat_CreateCluster(head, e2, e1, e1->flag, idArr);
759        Heap_HeapInsertCompare(head->heap, (void *)tclu, (long)tclu);
760      }
761
762      found = 0;
763      for(i=e1->order+1; i<eArr->num; i++)  {
764        e2 = (satLinearElem_t *)eArr->space[i];
765        if(e2->flag)    {
766          found = 1;
767          break;
768        }
769      }
770      if(found) {
771        tclu = sat_CreateCluster(head, e1, e2, e1->flag, idArr);
772        Heap_HeapInsertCompare(head->heap, (void *)tclu, (long)tclu);
773      }
774    }
775    sat_FreeCluster(mgr, clu);
776  }
777
778  Heap_HeapFree(heap);
779  head->heap = 0;
780
781  free(idArr);
782
783  if(modified) {
784    eArr = head->elemArray;
785    neArr = sat_ArrayAlloc(eArr->num);
786    index = 0;
787    for(i=0; i<eArr->num; i++) {
788      e1 = (satLinearElem_t *)eArr->space[i];
789      if(e1->flag == 0) continue;
790
791      e1->order = index++;
792      sat_ArrayInsert(neArr, (long)e1);
793    }
794    sat_ArrayFree(eArr);
795    head->elemArray = neArr;
796  }
797
798  if(head->elemArray->num == 1)
799    modified = 0;
800
801  return(modified);
802}
803
804
805/**Function********************************************************************
806
807  Synopsis    [Free satLinearCluster_t]
808
809  Description [Free satLinearCluster_t]
810
811  SideEffects []
812
813  SeeAlso     []
814
815******************************************************************************/
816static void
817sat_FreeCluster(DdManager *mgr, satLinearCluster_t *clu)
818{
819satArray_t *deadArray;
820
821  deadArray = clu->deadArray;
822  if(deadArray) {
823    sat_ArrayFree(deadArray);
824  }
825  free(clu);
826}
827
828
829/**Function********************************************************************
830
831  Synopsis    [Sanity check for dead node]
832
833  Description [Sanity check for dead node]
834
835  SideEffects []
836
837  SeeAlso     []
838
839******************************************************************************/
840static void
841sat_CheckDeadNode(
842        satLinearHead_t *head,
843        satLinearCluster_t *clu)
844{
845satArray_t *deadArray, *eArr;
846satArray_t *support;
847satLinearVar_t *var, *tvar;
848satLinearElem_t *elem;
849int i, j, k;
850
851
852  if(clu->deadArray) {
853    deadArray = clu->deadArray;
854    for(i=0; i<deadArray->num; i++) {
855      var = (satLinearVar_t *)deadArray->space[i];
856      eArr = head->elemArray;
857      for(j=0; j<var->from; j++) {
858        elem = (satLinearElem_t *)eArr->space[j];
859        if(elem->flag == 0)     continue;
860        support = elem->support;
861        for(k=0; k<support->num; k++) {
862          tvar = (satLinearVar_t *)support->space[k];
863          tvar = (satLinearVar_t *)SATnormalNode((unsigned long)tvar);
864          if(var == tvar) {
865            fprintf(stdout, "Error : wrong variable range\n");
866          }
867        }
868      }
869      for(j=var->to+1; j<eArr->num; j++) {
870        elem = (satLinearElem_t *)eArr->space[j];
871        if(elem->flag == 0)     continue;
872        support = elem->support;
873        for(k=0; k<support->num; k++) {
874          tvar = (satLinearVar_t *)support->space[k];
875          tvar = (satLinearVar_t *)SATnormalNode((unsigned long)tvar);
876          if(var == tvar) {
877            fprintf(stdout, "Error : wrong variable range\n");
878          }
879        }
880      }
881    }
882  }
883}
884
885/**Function********************************************************************
886
887  Synopsis    [Convert CNF into BDD.]
888
889  Description [First, the force based clauses arrangement is applied to get
890               a min max -cut arrangement of clauses.
891               Then apply the iterative clustering algorithm to get a monolithic
892               BDD.]
893
894  SideEffects []
895
896  SeeAlso     [sat_TryToBuildMonolithicBDD]
897
898******************************************************************************/
899static int
900sat_ConvertCNF2BDD(
901        satManager_t *cm,
902        DdManager *mgr,
903        int conflictFlag)
904{
905satLinearHead_t *head;
906DdNode *result, *cube;
907DdNode *l1, *l2;
908DdNode *nl1, *nl2;
909satArray_t *satArr, *arr;
910int limitCut;
911int flag, length;
912int cut, i;
913
914  head = sat_CreateLinearHead(cm, conflictFlag);
915
916  if(head == 0) return(0);
917
918  head->mgr = mgr;
919
920  sat_GetArrangementByForce(cm, head);
921
922  if(cm->option->verbose > 3)
923    cut = sat_PrintCutProfile(cm, head, "final", 1);
924  else
925    cut = sat_PrintCutProfile(cm, head, "final", 0);
926
927  if(conflictFlag)
928    limitCut = cm->option->maxLimitOfCutSizeForBDDDPLL;
929  else
930    limitCut = cm->option->maxLimitOfCutSizeForMonolithicBDD;
931  if(cut > limitCut) {
932    sat_FreeLinearHead(head);
933    return(SAT_BDD_BACKTRACK);
934  }
935
936  flag = sat_ClusteringElementMain(cm, head);
937
938  if(flag == SAT_BDD_SAT) {
939    arr = head->latestClusterArray;
940    satArr = sat_ArrayAlloc(16);
941    for(i=arr->num-1; i>=0; i--) {
942      l1 = (DdNode *)arr->space[i];
943      i--;
944      l2 = (DdNode *)arr->space[i];
945      nl1 = sat_CofactorBDDArray(head, mgr, l1, satArr);
946      nl2 = sat_CofactorBDDArray(head, mgr, l2, satArr);
947      result = Cudd_bddAndLimit(mgr, nl1, nl2, head->bddAndLimit);
948      cuddRef(result);
949      Cudd_RecursiveDeref(mgr, nl1);
950      Cudd_RecursiveDeref(mgr, nl2);
951      cube = Cudd_LargestCube(mgr, result, &length);
952      cuddRef(cube);
953      sat_ExtractAssignmentFromBDD(head, mgr, satArr, cube);
954      Cudd_RecursiveDeref(mgr, cube);
955      Cudd_RecursiveDeref(mgr, result);
956    }
957    cm->assignByBDD = satArr;
958  }
959  sat_FreeLinearHead(head);
960
961  return(flag);
962}
963
964/**Function********************************************************************
965
966  Synopsis    [Free  satLinearHead_t structure.]
967
968  Description [Free  satLinearHead_t structure.]
969
970  SideEffects []
971
972  SeeAlso     []
973
974******************************************************************************/
975static void
976sat_FreeLinearHead(satLinearHead_t *head)
977{
978satLinearElem_t *elem;
979satLinearVar_t *var;
980satArray_t *eArr, *vArr, *arr;
981satArray_t *support, *clauses;
982DdNode *bdd;
983int i;
984
985  eArr = head->elemArray;
986  if(eArr) {
987    for(i=0; i<eArr->num; i++) {
988      elem = (satLinearElem_t *)(eArr->space[i]);
989      support = elem->support;
990      if(support)
991        sat_ArrayFree(support);
992      if(elem->bdd)
993        Cudd_RecursiveDeref(head->mgr, elem->bdd);
994    }
995  }
996  vArr = head->varArray;
997  if(vArr) {
998    for(i=0; i<vArr->num; i++) {
999      var = (satLinearVar_t *)vArr->space[i];
1000      clauses = var->clauses;
1001      if(clauses)
1002        sat_ArrayFree(clauses);
1003      if(var->bdd)
1004        Cudd_RecursiveDeref(head->mgr, var->bdd);
1005    }
1006  }
1007
1008  if(head->variablesArray)
1009    sat_ArrayFree(head->variablesArray);
1010  if(head->clausesArray)
1011    sat_ArrayFree(head->clausesArray);
1012
1013  if(head->elemHead)
1014    free(head->elemHead);
1015  if(head->varHead)
1016    free(head->varHead);
1017  if(head->id2edge)
1018    free(head->id2edge);
1019  if(head->edge2id)
1020    free(head->edge2id);
1021  if(head->edge2vid)
1022    free(head->edge2vid);
1023
1024  if(head->latestClusterArray)  {
1025    arr = head->latestClusterArray;
1026    for(i=0; i<arr->num; i++) {
1027      bdd = (DdNode *)arr->space[i];
1028      Cudd_RecursiveDeref(head->mgr, bdd);
1029    }
1030    sat_ArrayFree(arr);
1031    head->latestClusterArray = 0;
1032  }
1033
1034  if(head->deadArray)
1035    free(head->deadArray);
1036  free(head);
1037}
1038
1039
1040/**Function********************************************************************
1041
1042  Synopsis    [Variable comparing function for sorting.]
1043
1044  Description [Variable comparing function for sorting.]
1045
1046  SideEffects []
1047
1048  SeeAlso     []
1049
1050******************************************************************************/
1051static int
1052linearVarCompare(
1053  const void * node1,
1054  const void * node2)
1055{
1056  satLinearVar_t *d1;
1057  satLinearVar_t *d2;
1058
1059  d1 = *(satLinearVar_t **)(node1);
1060  d2 = *(satLinearVar_t **)(node2);
1061
1062  return (d1->pos > d2->pos);
1063}
1064
1065/**Function********************************************************************
1066
1067  Synopsis    [Element comparing function for sorting.]
1068
1069  Description [Element comparing function for sorting.]
1070
1071  SideEffects []
1072
1073  SeeAlso     []
1074
1075******************************************************************************/
1076static int
1077linearElemCompare(
1078  const void * node1,
1079  const void * node2)
1080{
1081  satLinearElem_t *d1;
1082  satLinearElem_t *d2;
1083
1084  d1 = *(satLinearElem_t **)(node1);
1085  d2 = *(satLinearElem_t **)(node2);
1086
1087  return (d1->pos > d2->pos);
1088}
1089
1090/**Function********************************************************************
1091
1092  Synopsis    [Generate linear arrangement by force relaxation.]
1093
1094  Description [Generate linear arrangement by force relaxation.]
1095
1096  SideEffects []
1097
1098  SeeAlso     []
1099
1100******************************************************************************/
1101static void
1102sat_GetArrangementByForce(
1103        satManager_t *cm,
1104        satLinearHead_t *head)
1105{
1106int iteration;
1107double prespan, span;
1108int from, to, sum;
1109int i, j, inverted;
1110satLinearElem_t *elem;
1111satLinearVar_t *var;
1112satArray_t *eArr, *vArr;
1113satArray_t *support, *clauses;
1114
1115  iteration = 0;
1116  prespan = MAXINT;
1117  eArr = head->elemArray;
1118  vArr = head->varArray;
1119  while(1) {
1120    iteration++;
1121    if(iteration > 200) break;
1122
1123    span = 0;
1124    for(i=0; i<eArr->num; i++) {
1125      elem = (satLinearElem_t *)(eArr->space[i]);
1126      support = elem->support;
1127      sum = 0;
1128      from = MAXINT;
1129      to = -1;
1130      for(j=0; j<support->num; j++) {
1131        var = (satLinearVar_t *)(support->space[j]);
1132        inverted = SATisInverted((unsigned long)var);
1133        var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
1134        sum += var->order;
1135        if(var->order < from)   from = var->order;
1136        if(to < var->order)     to = var->order;
1137      }
1138      if(from != MAXINT && to != -1)
1139        span += (double)(to - from);
1140      elem->pos = sum / (double)(support->num);
1141    }
1142
1143    if(iteration > 2 && (prespan * 0.9999) < span)
1144      break;
1145    prespan = span;
1146
1147    qsort(eArr->space, eArr->num, sizeof(satLinearElem_t *), linearElemCompare);
1148    for(i=0; i<eArr->num; i++) {
1149      elem = (satLinearElem_t *)eArr->space[i];
1150      elem->order = i;
1151    }
1152
1153    for(i=0; i<vArr->num; i++) {
1154      var = (satLinearVar_t *)vArr->space[i];
1155      clauses = var->clauses;
1156      sum = 0;
1157      for(j=0; j<clauses->num; j++) {
1158        elem = (satLinearElem_t *)clauses->space[j];
1159        sum += elem->order;
1160      }
1161      var->pos = sum / (double)(clauses->num);
1162    }
1163
1164    qsort(vArr->space, vArr->num, sizeof(satLinearVar_t *), linearVarCompare);
1165    for(i=0; i<vArr->num; i++) {
1166      var = (satLinearVar_t *)vArr->space[i];
1167      var->order = i;
1168    }
1169  }
1170  if(cm->option->verbose > 3)
1171    fprintf(cm->stdOut, "NOTICE : %d iteration for force based arrangement\n", iteration);
1172}
1173
1174/**Function********************************************************************
1175
1176  Synopsis    [Print profile of cur from linear arrangement.]
1177
1178  Description [Print profile of cur from linear arrangement.]
1179
1180  SideEffects []
1181
1182  SeeAlso     []
1183
1184******************************************************************************/
1185static int
1186sat_PrintCutProfile(
1187        satManager_t *cm,
1188        satLinearHead_t *head,
1189        char *baseName,
1190        int printFlag)
1191{
1192st_table *cutTable;
1193st_generator *gen;
1194FILE *fout = NIL(FILE);
1195int i, j, cut, sum;
1196int to, from;
1197char filename[1024];
1198satArray_t *support, *clauses, *eArr, *vArr;
1199satLinearElem_t *elem;
1200satLinearVar_t *var;
1201double span;
1202
1203  eArr = head->elemArray;
1204  span = 0;
1205  for(i=0; i<eArr->num; i++) {
1206    elem = (satLinearElem_t *)eArr->space[i];
1207    support = elem->support;
1208    sum = 0;
1209    to = -1;
1210    from = MAXINT;
1211    for(j=0; j<support->num; j++) {
1212      var = (satLinearVar_t *)support->space[j];
1213      var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
1214      sum += var->order;
1215      if(to < var->order)       to = var->order;
1216      if(var->order < from)     from = var->order;
1217    }
1218    elem->to = to;
1219    if(from != MAXINT && to != -1)
1220      span += (double)(to - from);
1221  }
1222
1223  cut = 0;
1224  if(printFlag) {
1225    sprintf(filename, "%s.data", baseName);
1226    fout = fopen(filename, "w");
1227  }
1228  cutTable = st_init_table(st_ptrcmp, st_ptrhash);
1229  vArr = head->varArray;
1230  for(i=0; i<vArr->num; i++) {
1231    var = (satLinearVar_t *)vArr->space[i];
1232    clauses = var->clauses;
1233    for(j=0; j<clauses->num; j++) {
1234      elem = (satLinearElem_t *)clauses->space[j];
1235      st_insert(cutTable, (char *)elem, (char *)elem);
1236    }
1237    st_foreach_item(cutTable, gen, &elem, &elem) {
1238      if(elem->to <= i)
1239        st_delete(cutTable, &elem, NIL(char *));
1240    }
1241    if(cut < cutTable->num_entries)
1242      cut = cutTable->num_entries;
1243    if(printFlag)
1244      fprintf(fout, "%d %d\n", i, cutTable->num_entries);
1245  }
1246  st_free_table(cutTable);
1247
1248  if(printFlag) {
1249    fclose(fout);
1250    sprintf(filename, "%s.gnu", baseName);
1251    fout = fopen(filename, "w");
1252    fprintf(fout, "set terminal postscript \n");
1253    fprintf(fout, "set output \"%s.ps\"\n", baseName);
1254    fprintf(fout, "set title \"profile of live variable span %f cut %d\"\n",
1255            span, cut);
1256    fprintf(fout, "plot \"%s.data\" using 1:2 title \"%s\" with lines\n", baseName, "cut");
1257    fclose(fout);
1258  }
1259
1260  return cut;
1261
1262}
1263
1264/**Function********************************************************************
1265
1266  Synopsis    [Clustering on linear arrangement.]
1267
1268  Description [Clustering on linear arrangement.]
1269
1270  SideEffects []
1271
1272  SeeAlso     []
1273
1274******************************************************************************/
1275static int
1276sat_ClusteringElementMain(
1277        satManager_t *cm,
1278        satLinearHead_t *head)
1279{
1280int modified;
1281satLinearElem_t *elem;
1282DdNode *one;
1283
1284  Cudd_AutodynEnable(head->mgr, CUDD_REORDER_SIFT);
1285
1286  sat_InitClusteringElement(cm, head);
1287
1288  while(1) {
1289    sat_ComputeVariableRange(cm, head);
1290    sat_ClusteringGetCandidate(cm, head);
1291    modified = sat_ClusteringElement(cm, head);
1292    if(modified == 0)   break;
1293  }
1294
1295  if(head->elemArray->num == 1) {
1296    one = DD_ONE(head->mgr);
1297    elem = (satLinearElem_t *)(head->elemArray->space[0]);
1298    if(elem->bdd == one)                return(SAT_BDD_SAT);
1299    else if(elem->bdd == Cudd_Not(one)) return(SAT_BDD_UNSAT);
1300    else                                return(SAT_BDD_BACKTRACK);
1301  }
1302  else {
1303    return(SAT_BDD_BACKTRACK);
1304  }
1305}
1306
1307/**Function********************************************************************
1308
1309  Synopsis    [Compute the range of variables.]
1310
1311  Description [Compute the range of variables.]
1312
1313  SideEffects []
1314
1315  SeeAlso     []
1316
1317******************************************************************************/
1318static void
1319sat_ComputeVariableRange(
1320        satManager_t *cm,
1321        satLinearHead_t *head)
1322{
1323satArray_t *support, *vArr, *eArr;
1324satLinearElem_t *elem;
1325satLinearVar_t *var;
1326int i, j;
1327
1328  vArr = head->varArray;
1329  eArr = head->elemArray;
1330
1331  for(i=0; i<vArr->num; i++) {
1332    var = (satLinearVar_t *)vArr->space[i];
1333    var->from = MAXINT;
1334    var->to = -1;
1335  }
1336
1337  for(i=0; i<eArr->num; i++) {
1338    elem = (satLinearElem_t *)eArr->space[i];
1339    support = elem->support;
1340    for(j=0; j<support->num; j++) {
1341      var = (satLinearVar_t *)support->space[j];
1342      var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
1343      if(elem->order < var->from)       var->from = elem->order;
1344      if(var->to < elem->order)         var->to = elem->order;
1345    }
1346  }
1347}
1348
1349/**Function********************************************************************
1350
1351  Synopsis    [Preparation for the clutering.]
1352
1353  Description [Preparation for the clutering.]
1354
1355  SideEffects []
1356
1357  SeeAlso     []
1358
1359******************************************************************************/
1360static void
1361sat_InitClusteringElement(
1362        satManager_t *cm,
1363        satLinearHead_t *head)
1364{
1365DdNode *sum, *nsum, *one;
1366DdManager *mgr;
1367satLinearElem_t *elem;
1368satLinearVar_t *var;
1369satArray_t *support, *vArr, *eArr;
1370int i, j, index;
1371long nv;
1372int inverted;
1373
1374  mgr = head->mgr;
1375  vArr = head->varArray;
1376  eArr = head->elemArray;
1377  index = 0;
1378  one = DD_ONE(mgr);
1379
1380  for(i=0; i<vArr->num; i++) {
1381    var = (satLinearVar_t *)vArr->space[i];
1382    nv = var->node;
1383    head->id2edge[index] = nv;
1384    head->edge2id[SATnodeID(nv)] = index;
1385    var->bdd = cuddUniqueInter(mgr,index,one,Cudd_Not(one));
1386    cuddRef(var->bdd);
1387    index++;
1388  }
1389
1390  for(i=0; i<eArr->num; i++) {
1391    elem = (satLinearElem_t *)eArr->space[i];
1392    support = elem->support;
1393    sum = Cudd_Not(one);
1394    cuddRef(sum);
1395    for(j=0; j<support->num; j++) {
1396      var = (satLinearVar_t *)support->space[j];
1397      inverted = SATisInverted((unsigned long)var);
1398      var = (satLinearVar_t *)SATnormalNode((unsigned long)var);
1399      nsum = Cudd_bddAnd(mgr,Cudd_Not(sum),
1400                             (inverted ? var->bdd : Cudd_Not(var->bdd)));
1401      nsum = Cudd_Not(nsum);
1402      cuddRef(nsum);
1403
1404      Cudd_RecursiveDeref(mgr,sum);
1405      sum = nsum;
1406    }
1407    elem->bdd = sum;
1408  }
1409}
1410
1411#endif
1412#ifndef BDDcu
1413/**Function********************************************************************
1414
1415  Synopsis    [Build monolithic BDD.]
1416
1417  Description [Try to build a monolithic BDD from the set of clauses.
1418               If it is succeeded then we can conclude whether given CNF is
1419               satisfiable of not.]
1420
1421  SideEffects []
1422
1423  SeeAlso     []
1424
1425******************************************************************************/
1426void
1427sat_TryToBuildMonolithicBDD(satManager_t *cm)
1428{
1429  fprintf(stderr, "Warning : This feature is only availabe with CUDD package\n");
1430  return;
1431}
1432#endif
Note: See TracBrowser for help on using the repository browser.