source: vis_dev/vis-2.3/src/sat/satInc.c @ 23

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

vis2.3

File size: 18.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [satInc.c]
4
5  PackageName [sat]
6
7  Synopsis    [Routines for sat incremental function.]
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
21static char rcsid[] UNUSED = "$Id: satInc.c,v 1.16 2009/04/11 18:26:37 fabio Exp $";
22static satManager_t *SatCm;
23
24/*---------------------------------------------------------------------------*/
25/* Constant declarations                                                     */
26/*---------------------------------------------------------------------------*/
27
28/**AutomaticStart*************************************************************/
29
30/*---------------------------------------------------------------------------*/
31/* Static function prototypes                                                */
32/*---------------------------------------------------------------------------*/
33
34static int ScoreDistillCompare(const void *x, const void *y);
35
36/**AutomaticEnd***************************************************************/
37
38
39/*---------------------------------------------------------------------------*/
40/* Definition of exported functions                                          */
41/*---------------------------------------------------------------------------*/
42
43
44/**Function********************************************************************
45
46  Synopsis    [ Apply distillation method to find
47                the clauses that can be forwarded]
48
49  Description [ Apply distillation method to find
50                the clauses that can be forwarded]
51
52  SideEffects []
53
54  SeeAlso     []
55
56******************************************************************************/
57void
58sat_IncrementalUsingDistill(satManager_t *cm)
59{
60  sat_TrieBasedImplication(cm, cm->trieArray, 1);
61  sat_FreeTrie(cm, cm->trieArray);
62  cm->trieArray = 0;
63  fprintf(cm->stdOut, "%s %d conflicts are forwarded from distillation,\n",
64          cm->comment,
65          cm->each->nDistillObjConflictCl + cm->each->nDistillNonobjConflictCl);
66}
67
68/**Function********************************************************************
69
70  Synopsis    [ Make decision based on trie when applying distillation ]
71
72  Description [ Make decision based on trie when applying distillation ]
73
74  SideEffects []
75
76  SeeAlso     []
77
78******************************************************************************/
79satLevel_t *
80sat_DecisionBasedOnTrie(
81        satManager_t *cm,
82        long v,
83        int value)
84{
85satLevel_t *d;
86
87  d = sat_AllocLevel(cm);
88  d->decisionNode = v;
89
90  SATvalue(v) = value;
91  SATmakeImplied(v, d);
92
93  sat_Enqueue(cm->queue, v);
94  SATflags(v) |= InQueueMask;
95
96  return(d);
97}
98
99/**Function********************************************************************
100
101  Synopsis    [ Apply implication based on trie]
102
103  Description [ Apply implication based on trie]
104
105  SideEffects []
106
107  SeeAlso     []
108
109******************************************************************************/
110void
111sat_TrieBasedImplication(
112        satManager_t *cm,
113        satArray_t *trieArray,
114        int depth)
115{
116int i;
117satTrie_t *t;
118satLevel_t *d;
119satArray_t *tArray;
120
121  if(trieArray == 0)    return;
122
123  for(i=0; i<trieArray->num; i++) {
124    t = (satTrie_t *)(trieArray->space[i]);
125    if(SATvalue(t->id) < 2)     continue;
126
127    tArray = t->child[0];
128    if(tArray) {
129      d = sat_DecisionBasedOnTrie(cm, t->id, 0);
130      sat_ImplicationMain(cm, d);
131      if(d->conflict) {
132        sat_ConflictAnalysisOnTrie(cm, d);
133      }
134      else if(cm->status == 0) {
135        sat_TrieBasedImplication(cm, tArray, depth+1);
136      }
137      sat_Backtrack(cm, depth-1);
138    }
139
140    tArray = t->child[1];
141    if(tArray && cm->status == 0) {
142      d = sat_DecisionBasedOnTrie(cm, t->id, 1);
143      sat_ImplicationMain(cm, d);
144      if(d->conflict) {
145        sat_ConflictAnalysisOnTrie(cm, d);
146      }
147      else if(cm->status == 0) {
148        sat_TrieBasedImplication(cm, tArray, depth+1);
149      }
150      sat_Backtrack(cm, depth-1);
151    }
152
153    if(cm->status == SAT_BACKTRACK && depth == 1) {
154      cm->status = 0;
155      d = SATgetDecision(0);
156      sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
157      sat_ImplyArray(cm, d, cm->objUnitLitArray);
158      sat_MarkObjectiveFlagToArray(cm, cm->objUnitLitArray);
159      sat_ImplicationMain(cm, d);
160      if(d->conflict) {
161        cm->status = SAT_UNSAT;
162        return;
163      }
164      i--;
165    }
166  }
167}
168
169/**Function********************************************************************
170
171  Synopsis    [ Conflict analysis based on trie]
172
173  Description [  Conflict analysis based on trie]
174
175  SideEffects []
176
177  SeeAlso     []
178
179******************************************************************************/
180void
181sat_ConflictAnalysisOnTrie(
182        satManager_t *cm,
183        satLevel_t *d)
184{
185int bLevel;
186long v, learned, unitLit;
187int objectFlag;
188satArray_t *clauseArray;
189satStatistics_t *stats;
190
191  bLevel = 0;
192  unitLit = -1;
193  clauseArray = cm->auxArray;
194  sat_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &unitLit);
195
196  if(clauseArray->num > (int)(cm->currentDecision*2)) {
197    sat_GetConflictAsConflictClause(cm, clauseArray);
198  }
199
200  if(clauseArray->num == 1) {
201    cm->status = SAT_BACKTRACK;
202    v = clauseArray->space[0];
203    if(objectFlag)
204      sat_ArrayInsert(cm->objUnitLitArray, SATnot(v));
205    else
206      sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(v));
207  }
208  else {
209    learned = sat_AddClauseIncremental(cm, clauseArray, objectFlag, 1);
210  }
211
212  stats = cm->each;
213  if(objectFlag) {
214    stats->nInitObjConflictCl++;
215    stats->nInitObjConflictLit += clauseArray->num;
216    stats->nObjConflictCl++;
217    stats->nObjConflictLit += clauseArray->num;
218    stats->nDistillObjConflictCl++;
219    stats->nDistillObjConflictLit += clauseArray->num;
220  }
221  else {
222    stats->nInitNonobjConflictCl++;
223    stats->nInitNonobjConflictLit += clauseArray->num;
224    stats->nObjConflictCl++;
225    stats->nObjConflictLit += clauseArray->num;
226    stats->nDistillNonobjConflictCl++;
227    stats->nDistillNonobjConflictLit += clauseArray->num;
228  }
229  stats->nConflictCl++;
230  stats->nConflictLit += clauseArray->num;
231}
232
233/**Function********************************************************************
234
235  Synopsis    [ Get conflict clauses from the decision variables]
236
237  Description [ When applying distillation,
238                get conflict clauses from the decision variables
239                to create conflict clause ]
240
241  SideEffects [ ]
242
243  SeeAlso     [ ]
244
245******************************************************************************/
246void
247sat_GetConflictAsConflictClause(
248        satManager_t *cm,
249        satArray_t *clauseArray)
250{
251int i;
252satLevel_t *d;
253
254  clauseArray->num = 0;
255  for(i=1; i<=cm->currentDecision; i++) {
256    d = SATgetDecision(i);
257    sat_ArrayInsert(clauseArray,
258            (d->decisionNode)^(!(SATvalue(d->decisionNode))));
259  }
260}
261
262/**Function********************************************************************
263
264  Synopsis    [ Restore conflict clauses to use them for current run]
265
266  Description [ Restore conflict clauses to use them for current run]
267
268  SideEffects [ ]
269
270  SeeAlso     [ sat_SaveNonobjClauses sat_SaveAllClauses ]
271
272******************************************************************************/
273void
274sat_RestoreForwardedClauses(satManager_t *cm, int objectFlag)
275{
276int i, size;
277int total;
278long *space, c, *start;
279satArray_t *saved;
280satArray_t *clause;
281//Bing
282 int NotCoi = 0, ct=0;
283
284
285  if(cm->option->checkNonobjForwarding) {
286    sat_CheckForwardedClauses(cm);
287  }
288
289  saved = cm->savedConflictClauses;
290  if(saved == 0)
291    return;
292
293  clause = sat_ArrayAlloc(50);
294
295  total = 0;
296  for(i=0, space=saved->space; i<saved->num; i++, space++){
297    if(*space < 0) {
298      space++;
299      i++;
300      start = space;
301      size = 0;
302      clause->num = 0;
303      //Bing:
304      NotCoi = 0;
305      while(*space > 0) {
306        sat_ArrayInsert(clause, SATnot((*space)));
307        //Bing:
308        if(!(SATflags(*space)&CoiMask)){
309          NotCoi = 1;
310        }
311        size++;
312        i++;
313        space++;
314      }
315
316
317      //Bing:
318      if(cm->option->AbRf){
319        if(!NotCoi){
320          c = sat_AddClauseIncremental(cm, clause, objectFlag, 0);
321          total++;
322        }
323        else
324          ct++;
325      }
326      else{
327        c = sat_AddClauseIncremental(cm, clause, objectFlag, 0);
328        total++;
329      }
330    }
331  }
332  sat_ArrayFree(clause);
333  sat_ArrayFree(saved);
334  cm->savedConflictClauses = 0;
335
336/**  fprintf(cm->stdOut, "%s %d clauses are forwarded by reststoring
337     non-objective\n", cm->comment, total) ; **/
338}
339
340/**Function********************************************************************
341
342  Synopsis    [ Check whether the given conflict clauses can be forwared ]
343
344  Description [ Check whether the given conflict clauses can be forwared ]
345
346  SideEffects [ ]
347
348  SeeAlso     [ ]
349
350******************************************************************************/
351void
352sat_CheckForwardedClauses(satManager_t *cm)
353{
354long *space, *start;
355long nv;
356int size, i;
357int total;
358int conflictFlag, inverted;
359int j, value, level;
360satLevel_t *d;
361satArray_t *saved;
362satArray_t *clause;
363
364  d = 0;
365  saved = cm->savedConflictClauses;
366  if(saved == 0)
367    return;
368
369  clause = sat_ArrayAlloc(50);
370
371  total = 0;
372  for(i=0, space=saved->space; i<saved->num; i++, space++){
373    if(*space < 0) {
374      start = space;
375      space++;
376      i++;
377      size = 0;
378      clause->num = 0;
379      conflictFlag = 0;
380      while(*space > 0) {
381        sat_ArrayInsert(clause, SATnot((*space)));
382        if(conflictFlag == 0) {
383          nv = *space;
384          inverted = (SATisInverted(nv));
385          nv = SATnormalNode(nv);
386
387          d = sat_AllocLevel(cm);
388          d->decisionNode = nv;
389          SATvalue(nv) = inverted;
390          SATmakeImplied(nv, d);
391
392          sat_Enqueue(cm->queue, nv);
393          SATflags(nv) |= InQueueMask;
394
395          sat_ImplicationMain(cm, d);
396          if(d->conflict)       conflictFlag = 1;
397        }
398        size++;
399        i++;
400        space++;
401      }
402
403      if(d->conflict == 0) {
404        fprintf(cm->stdOut, "%s ERROR : %ld does not result in conflict\n",
405            cm->comment, *start);
406        for(j=0; j<clause->num; j++) {
407          nv = clause->space[j];
408          inverted = SATisInverted(nv);
409          nv = SATnormalNode(nv);
410          value = SATvalue(nv);
411          level = value>1 ? -1 : SATlevel(nv);
412          fprintf(cm->stdOut, "%6ld%c@%d=%c%c ",
413                  nv, inverted ? '\'' : ' ', level, SATgetValueChar(value),
414                  ' ');
415        }
416        fprintf(cm->stdOut, "\n");
417      }
418      sat_Backtrack(cm, -1);
419
420      total++;
421    }
422  }
423  sat_ArrayFree(clause);
424}
425
426/**Function********************************************************************
427
428  Synopsis    [ Save objective independent conflict clauses]
429
430  Description [ When applying incremental SAT, one has to save objective
431                independent conflict clause  They are restored by
432                sat_RestoreForwardedClauses ]
433
434  SideEffects [ ]
435
436  SeeAlso     [ sat_RestoreForwardedClauses ]
437
438******************************************************************************/
439void
440sat_SaveNonobjClauses(satManager_t *cm)
441{
442int limit, total, passed;
443int size, j;
444long *plit, nv, v, i;
445satArray_t *savedArray;
446
447  savedArray = sat_ArrayAlloc(1024);
448
449  total = passed = 0;
450  limit = cm->option->incNumNonobjLitsLimit;
451  for(i=cm->beginConflict; i<cm->nodesArraySize; i+= satNodeSize) {
452    if(SATreadInUse(i) == 0)            continue;
453    if(!(SATflags(i) & NonobjMask))     {
454      continue;
455    }
456    size = SATnumLits(i);
457    if(size > limit) {
458      total++;
459    }
460    else {
461      total++;
462      passed++;
463      plit = (long*)SATfirstLit(i);
464      nv = (*(plit-1));
465      sat_ArrayInsert(savedArray, nv);
466      for(j=0; j<size; j++, plit++) {
467        v = SATgetNode(*plit);
468        sat_ArrayInsert(savedArray, v);
469      }
470      sat_ArrayInsert(savedArray, nv);
471    }
472  }
473  if(cm->option->verbose > 1) {
474    fprintf(cm->stdOut, "%s %d NonObjective Clauses forwarded out of %d\n",
475            cm->comment, passed, total);
476  }
477  cm->savedConflictClauses = savedArray;
478}
479
480/**Function********************************************************************
481
482  Synopsis    [ Save all conflict clauses]
483
484  Description [ When applying incremental SAT for BMC,
485                one can forward all the clauses
486                They are restored by sat_RestoreForwardedClauses ]
487
488  SideEffects [ ]
489
490  SeeAlso     [ sat_RestoreForwardedClauses ]
491
492******************************************************************************/
493void
494sat_SaveAllClauses(satManager_t *cm)
495{
496int limit, total, passed;
497int size, j;
498long *plit, nv, v, i;
499satArray_t *savedArray;
500
501  savedArray = sat_ArrayAlloc(1024);
502
503  total = passed = 0;
504  limit = cm->option->incNumNonobjLitsLimit;
505  for(i=cm->beginConflict; i<cm->nodesArraySize; i+= satNodeSize) {
506    if(SATreadInUse(i) == 0)            continue;
507    size = SATnumLits(i);
508    total++;
509    plit = (long*)SATfirstLit(i);
510    nv = (*(plit-1));
511    sat_ArrayInsert(savedArray, nv);
512    for(j=0; j<size; j++, plit++) {
513      v = SATgetNode(*plit);
514      sat_ArrayInsert(savedArray, v);
515    }
516    sat_ArrayInsert(savedArray, nv);
517  }
518  /**
519  if(cm->option->verbose > 1) {
520    fprintf(cm->stdOut, "%s %d clauses are forwarded\n",
521            cm->comment, total);
522  }
523  **/
524  cm->savedConflictClauses = savedArray;
525}
526
527/**Function********************************************************************
528
529  Synopsis    [ Build Trie with objective dependent conflict clauses]
530
531  Description [ When applying incremental SAT based on distillation
532                build Trie with objective dependent conflict clauses.]
533
534  SideEffects [ ]
535
536  SeeAlso     [ sat_BuildTrie ]
537
538******************************************************************************/
539void
540sat_BuildTrieForDistill(satManager_t *cm)
541{
542int limit, nCl, nLit;
543int j, n;
544int size, inverted;
545long v, *plit, i;
546int findFlag;
547satVariable_t *var;
548satArray_t *trieArray;
549satArray_t *unitArray;
550satTrie_t *t;
551
552  size = cm->initNumVariables * satNodeSize;
553  for(i=satNodeSize; i<size; i+= satNodeSize) {
554    var = SATgetVariable(i);
555    var->scores[0] = 0;
556    var->scores[1] = 0;
557  }
558
559  nCl = nLit = 0;
560  limit = cm->option->incNumObjLitsLimit;
561  for(i=cm->beginConflict; i<cm->nodesArraySize; i+= satNodeSize) {
562    if(SATreadInUse(i) == 0)            continue;
563    if(SATflags(i) & NonobjMask)        continue;
564
565    size = SATnumLits(i);
566    if(size > limit)    continue;
567    n = 0;
568    for(j=0, plit = (long*)SATfirstLit(i); j<size; j++, plit++) {
569      v = SATgetNode(*plit);
570      inverted = SATisInverted(v);
571      v = SATnormalNode(v);
572      var = SATgetVariable(v);
573      var->scores[inverted] += 1;
574      if(SATvalue(v) < 2)       continue;
575      n++;
576    }
577    if(n > 0) {
578      nCl++;
579      nLit += n;
580    }
581  }
582  if(cm->option->verbose > 1) {
583    fprintf(cm->stdOut, "%s Candidates for Distill %d clauses %d literals\n",
584            cm->comment, nCl, nLit);
585  }
586
587  trieArray = sat_ArrayAlloc(64);
588  cm->trieArray = trieArray;
589  unitArray = cm->objUnitLitArray;
590  if(unitArray) {
591    for(i=0; i<unitArray->num; i++) {
592      v = unitArray->space[i];
593      inverted = SATisInverted(v);
594      v = SATnormalNode(v);
595
596      findFlag = 0;
597      for(j=0;  j<trieArray->num; j++) {
598        t = (satTrie_t *)(trieArray->space[j]);
599        if(t->id == v) {
600          if(t->child[inverted] == 0)
601            t->child[inverted] = sat_ArrayAlloc(2);
602          findFlag = 1;
603        }
604      }
605
606      if(findFlag == 0) {
607        t = ALLOC(satTrie_t, 1);
608        memset(t, 0, sizeof(satTrie_t));
609        t->id = v;
610        if(t->child[inverted] == 0)
611          t->child[inverted] = sat_ArrayAlloc(2);
612        sat_ArrayInsert(trieArray, (long)t);
613      }
614    }
615  }
616
617  for(i=cm->beginConflict; i<cm->nodesArraySize; i+=satNodeSize) {
618    if(SATreadInUse(i) == 0)            continue;
619    if(SATflags(i) & NonobjMask)        continue;
620
621    size = SATnumLits(i);
622    if(size > limit)    continue;
623
624    plit = (long*)SATfirstLit(i);
625    SatCm = cm;
626    qsort(plit, size, sizeof(long), ScoreDistillCompare);
627    sat_BuildTrie(cm, trieArray, plit, 1);
628  }
629}
630
631/**Function********************************************************************
632
633  Synopsis    [ Build Trie with objective dependent conflict clauses]
634
635  Description [ When applying incremental SAT based on distillation
636                build Trie with objective dependent conflict clauses.]
637
638  SideEffects [ ]
639
640  SeeAlso     [ sat_BuildTrieForDistill ]
641
642******************************************************************************/
643void
644sat_BuildTrie(
645        satManager_t *cm,
646        satArray_t *trieArray,
647        long *plit,
648        int depth)
649{
650int i, inverted;
651long v;
652satTrie_t *t;
653
654  while(1) {
655    if(*plit <= 0)      return;
656    v = SATgetNode(*plit);
657    inverted = SATisInverted(v);
658    v = SATnormalNode(v);
659    if(SATvalue(v) < 2)plit++;
660    else                break;
661  }
662
663  for(i=0; i<trieArray->num; i++) {
664    t = (satTrie_t *)(trieArray->space[i]);
665    if(t->id == v) {
666      if(t->child[inverted] == 0)
667        t->child[inverted] = sat_ArrayAlloc(2);
668      plit++;
669      sat_BuildTrie(cm, t->child[inverted], plit, depth+1);
670      return;
671    }
672  }
673
674  t = ALLOC(satTrie_t, 1);
675  memset(t, 0, sizeof(satTrie_t));
676  t->id = v;
677  t->depth = depth;
678  sat_ArrayInsert(trieArray, (long)t);
679
680  if(t->child[inverted] == 0)
681    t->child[inverted] = sat_ArrayAlloc(2);
682  plit++;
683  sat_BuildTrie(cm, t->child[inverted], plit, depth+1);
684}
685
686
687
688/**Function********************************************************************
689
690  Synopsis    [ Free trie structure ]
691
692  Description [ Free trie structure ]
693
694  SideEffects [ ]
695
696  SeeAlso     [ sat_BuildTrieForDistill ]
697
698******************************************************************************/
699void
700sat_FreeTrie(satManager_t *cm, satArray_t *arr)
701{
702int i;
703satTrie_t *t;
704
705  if(arr == 0)  return;
706
707  for(i=0; i<arr->num; i++) {
708    t = (satTrie_t *)(arr->space[i]);
709    if(t->child[0]) {
710      sat_FreeTrie(cm, t->child[0]);
711      sat_ArrayFree(t->child[0]);
712    }
713    if(t->child[1]) {
714      sat_FreeTrie(cm, t->child[1]);
715      sat_ArrayFree(t->child[1]);
716    }
717    free(t);
718  }
719
720}
721/**Function********************************************************************
722
723  Synopsis    [ sort variable order based on occurrence to build Trie ]
724
725  Description [ sort variable order based on occurrence to build Trie ]
726
727  SideEffects [ ]
728
729  SeeAlso     [ sat_BuildTrieForDistill ]
730
731******************************************************************************/
732static int
733ScoreDistillCompare(const void *x, const void *y)
734{
735int n1, n2;
736int i1, i2;
737satVariable_t  v1, v2;
738
739  n1 = *(int *)x;
740  n2 = *(int *)y;
741  n1 >>= 2;
742  n2 >>= 2;
743  i1 = SATisInverted(n1);
744  n1 = SATnormalNode(n1);
745  i2 = SATisInverted(n2);
746  n2 = SATnormalNode(n2);
747  v1 = SatCm->variableArray[SATnodeID(n1)];
748  v2 = SatCm->variableArray[SATnodeID(n2)];
749
750  if(v1.scores[i1] == v2.scores[i2]) {
751    return(n1 > n2);
752  }
753  return(v1.scores[i1] < v2.scores[i2]);
754}
Note: See TracBrowser for help on using the repository browser.