source: vis_dev/vis-2.3/src/sat/satConflict.c @ 43

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

vis2.3
File size: 62.8 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [satConflict.c]
4
5  PackageName [sat]
6
7  Synopsis    [Routines for sat conflict analysism and unsat proof generation
8  for both CNF format and AIG format]
9
10  Author      [HoonSang Jin,  Bing Li]
11
12  Copyright [ This file was created at the University of Colorado at
13  Boulder.  The University of Colorado at Boulder makes no warranty
14  about the suitability of this software for any purpose.  It is
15  presented on an AS IS basis.]
16
17
18******************************************************************************/
19
20#include "satInt.h"
21#include "puresatInt.h"
22
23static char rcsid[] UNUSED = "$Id: satConflict.c,v 1.31 2009/04/11 18:26:37 fabio Exp $";
24
25static  satManager_t *SATcm;
26
27/*---------------------------------------------------------------------------*/
28/* Constant declarations                                                     */
29/*---------------------------------------------------------------------------*/
30
31/**AutomaticStart*************************************************************/
32
33/*---------------------------------------------------------------------------*/
34/* Static function prototypes                                                */
35/*---------------------------------------------------------------------------*/
36
37static int levelCompare( const void * node1, const void * node2);
38
39/**AutomaticEnd***************************************************************/
40
41
42/*---------------------------------------------------------------------------*/
43/* Definition of exported functions                                          */
44/*---------------------------------------------------------------------------*/
45
46
47/**Function********************************************************************
48
49  Synopsis    [ Conflict Analysis]
50
51  Description [ Conflict Analysis]
52
53  SideEffects []
54
55  SeeAlso     []
56
57******************************************************************************/
58
59int
60sat_ConflictAnalysis(
61        satManager_t *cm,
62        satLevel_t *d)
63{
64satStatistics_t *stats;
65satOption_t *option;
66satArray_t *clauseArray;
67int objectFlag;
68int bLevel;
69long fdaLit, conflicting;
70
71
72  conflicting = d->conflict;
73
74  if(d->level == 0) {
75      /** Bing : UNSAT core generation */
76    if(cm->option->coreGeneration)
77      sat_ConflictAnalysisForCoreGen(cm, d);
78    cm->currentDecision--;
79    return (-1);
80  }
81
82  stats = cm->each;
83  option = cm->option;
84
85
86  stats->nBacktracks++;
87
88  clauseArray = cm->auxArray;
89
90  bLevel = 0;
91  fdaLit = -1;
92  clauseArray->num = 0;
93
94  /*  Find Unique Implication Point */
95
96  if(option->RT)
97    sat_FindUIPWithRT(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
98  else
99    sat_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
100  stats->nNonchonologicalBacktracks += (d->level - bLevel);
101
102
103  if(clauseArray->num == 0) {
104    sat_PrintImplicationGraph(cm, d);
105    sat_PrintNode(cm, conflicting);
106  }
107
108  /* If we could find UIP then it is critical error...
109  * at lease the decision node has to be detected as UIP.
110  */
111  if(fdaLit == -1) {
112    fprintf(cm->stdOut, "%s ERROR : Illegal unit literal\n", cm->comment);
113    fflush(cm->stdOut);
114    sat_PrintNode(cm, conflicting);
115    sat_PrintImplicationGraph(cm, d);
116    sat_PrintDotForConflict(cm, d, conflicting, 0);
117    exit(0);
118  }
119
120  if(bLevel && cm->lowestBacktrackLevel > bLevel)
121    cm->lowestBacktrackLevel = bLevel;
122
123  bLevel = sat_AddConflictClauseAndBacktrack(
124          cm, clauseArray, d, fdaLit, bLevel, objectFlag, 0);
125
126  return(bLevel);
127}
128
129/**Function********************************************************************
130
131  Synopsis    [ Conflict Analysis for lifting instance]
132
133  Description [ Conflict Analysis for lifting instance]
134
135  SideEffects []
136
137  SeeAlso     []
138
139******************************************************************************/
140
141int
142sat_ConflictAnalysisForLifting(
143        satManager_t *cm,
144        satLevel_t *d)
145{
146satStatistics_t *stats;
147satOption_t *option;
148satArray_t *clauseArray;
149int objectFlag;
150int bLevel;
151long fdaLit, conflicting;
152
153
154  conflicting = d->conflict;
155
156  if(d->level == 0) {
157    cm->currentDecision--;
158    return (-1);
159  }
160
161  stats = cm->each;
162  option = cm->option;
163
164
165  stats->nBacktracks++;
166
167  clauseArray = cm->auxArray;
168
169  bLevel = 0;
170  fdaLit = -1;
171  clauseArray->num = 0;
172
173  /*  Find Unique Implication Point */
174  sat_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
175  stats->nNonchonologicalBacktracks += (d->level - bLevel);
176
177
178  if(clauseArray->num == 0) {
179    sat_PrintImplicationGraph(cm, d);
180    sat_PrintNode(cm, conflicting);
181  }
182
183  /* If we could find UIP then it is critical error...
184  * at lease the decision node has to be detected as UIP.
185  */
186  if(fdaLit == -1) {
187    fprintf(cm->stdOut, "%s ERROR : Illegal unit literal\n", cm->comment);
188    fflush(cm->stdOut);
189    sat_PrintNode(cm, conflicting);
190    sat_PrintImplicationGraph(cm, d);
191    sat_PrintDotForConflict(cm, d, conflicting, 0);
192    exit(0);
193  }
194
195  if(bLevel && cm->lowestBacktrackLevel > bLevel)
196    cm->lowestBacktrackLevel = bLevel;
197
198  bLevel = sat_AddConflictClauseAndBacktrackForLifting(
199          cm, clauseArray, d, fdaLit, bLevel, objectFlag, 0);
200
201  return(bLevel);
202}
203/**Function********************************************************************
204
205  Synopsis    [ Conflict Analysis on blocking clause]
206
207  Description [ Conflict Analysis on blocking clause]
208
209  SideEffects []
210
211  SeeAlso     []
212
213******************************************************************************/
214
215int
216sat_ConflictAnalysisWithBlockingClause(
217        satManager_t *cm,
218        satLevel_t *d)
219{
220satStatistics_t *stats;
221satOption_t *option;
222satArray_t *clauseArray;
223int objectFlag;
224int bLevel;
225long fdaLit, conflicting;
226
227
228  conflicting = d->conflict;
229
230  if(d->level == 0) {
231    cm->currentDecision--;
232    return (-1);
233  }
234
235  stats = cm->each;
236  option = cm->option;
237
238
239  stats->nBacktracks++;
240
241  clauseArray = cm->auxArray;
242
243  bLevel = 0;
244  fdaLit = -1;
245  clauseArray->num = 0;
246
247  /*  Find Unique Implication Point */
248  sat_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
249  stats->nNonchonologicalBacktracks += (d->level - bLevel);
250
251
252  if(clauseArray->num == 0) {
253    sat_PrintImplicationGraph(cm, d);
254    sat_PrintNode(cm, conflicting);
255  }
256
257  /* If we could find UIP then it is critical error...
258  * at lease the decision node has to be detected as UIP.
259  */
260  if(fdaLit == -1) {
261    fprintf(cm->stdOut, "%s ERROR : Illegal unit literal\n", cm->comment);
262    fflush(cm->stdOut);
263    sat_PrintNode(cm, conflicting);
264    sat_PrintImplicationGraph(cm, d);
265    sat_PrintDotForConflict(cm, d, conflicting, 0);
266    exit(0);
267  }
268
269  if(bLevel && cm->lowestBacktrackLevel > bLevel)
270    cm->lowestBacktrackLevel = bLevel;
271
272  bLevel = sat_AddConflictClauseWithNoScoreAndBacktrack(
273          cm, clauseArray, d, fdaLit, bLevel, objectFlag, 0);
274
275  return(bLevel);
276}
277
278/**Function********************************************************************
279
280  Synopsis    [ Strong Conflict Analysis.]
281
282  Description [ Strong Conflict Analysis.]
283
284  SideEffects []
285
286  SeeAlso     []
287
288******************************************************************************/
289int
290sat_StrongConflictAnalysis(
291        satManager_t *cm,
292        satLevel_t *d)
293{
294satStatistics_t *stats;
295satOption_t *option;
296satArray_t *clauseArray;
297int objectFlag;
298int bLevel;
299long fdaLit, conflicting;
300
301
302  conflicting = d->conflict;
303
304  if(d->level == 0) {
305      /** Bing : UNSAT core generation */
306    if(cm->option->coreGeneration)
307      sat_ConflictAnalysisForCoreGen(cm, d);
308    cm->currentDecision--;
309    return (-1);
310  }
311
312  stats = cm->each;
313  option = cm->option;
314
315
316  stats->nBacktracks++;
317
318  if(SATflags(conflicting) & IsCNFMask) {
319    SATnumConflict(conflicting) += 1;
320  }
321
322  clauseArray = cm->auxArray;
323
324  bLevel = 0;
325  fdaLit = -1;
326  clauseArray->num = 0;
327
328  /*  Find Unique Implication Point */
329  sat_FindUIPAndNonUIP(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
330  stats->nNonchonologicalBacktracks += (d->level - bLevel);
331
332
333  if(clauseArray->num == 0) {
334    sat_PrintImplicationGraph(cm, d);
335    sat_PrintNode(cm, conflicting);
336  }
337
338  /* If we could find UIP then it is critical error...
339  * at lease the decision node has to be detected as UIP.
340  */
341  if(fdaLit == -1) {
342    fprintf(cm->stdOut, "%s ERROR : Illegal unit literal\n", cm->comment);
343    fflush(cm->stdOut);
344    sat_PrintNode(cm, conflicting);
345    sat_PrintImplicationGraph(cm, d);
346    sat_PrintDotForConflict(cm, d, conflicting, 0);
347    exit(0);
348  }
349
350  if(bLevel && cm->lowestBacktrackLevel > bLevel)
351    cm->lowestBacktrackLevel = bLevel;
352
353  bLevel = sat_AddConflictClauseAndBacktrack(
354          cm, clauseArray, d, fdaLit, bLevel, objectFlag, 1);
355
356  return(bLevel);
357}
358
359/**Function********************************************************************
360
361  Synopsis    [ Add conflict clause and backtrack.]
362
363  Description [ Add conflict clause and backtrack.]
364
365  SideEffects []
366
367  SeeAlso     []
368
369******************************************************************************/
370int
371sat_AddConflictClauseAndBacktrack(
372        satManager_t *cm,
373        satArray_t *clauseArray,
374        satLevel_t *d,
375        long fdaLit,
376        int bLevel,
377        int objectFlag,
378        int strongFlag)
379{
380int inverted;
381long conflicting, learned;
382satOption_t *option;
383satStatistics_t *stats;
384satArray_t *nClauseArray;
385
386 RTManager_t * rm = cm->rm;
387
388  option = cm->option;
389  stats = cm->each;
390
391  inverted = SATisInverted(fdaLit);
392  fdaLit = SATnormalNode(fdaLit);
393
394  conflicting = d->conflict;
395
396  if(option->verbose > 2) {
397    if(option->verbose > 4)
398      sat_PrintNode(cm, conflicting);
399    fprintf(cm->stdOut, "conflict at %3d on %6ld  bLevel %d UnitLit ",
400            d->level, conflicting, bLevel);
401    sat_PrintNodeAlone(cm, fdaLit);
402    fprintf(cm->stdOut, "\n");
403  }
404
405  d->conflict = 0;
406
407  /* unit literal conflict clause */
408  if(clauseArray->num == 1) {
409    learned = sat_AddUnitConflictClause(cm, clauseArray, objectFlag);
410    stats->nUnitConflictCl++;
411    cm->currentTopConflict = cm->literals->last-1;
412    cm->currentTopConflictCount = 0;
413
414    sat_Backtrack(cm, 0);
415
416    if(SATlevel(fdaLit) == 0) {
417      if(cm->option->coreGeneration){
418        if(cm->option->RT){
419          st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
420
421          st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
422          RT_oriClsIdx(rm->root) = learned;
423        }
424        else{
425          st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
426          st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
427        }
428      }
429      cm->currentDecision = -1;
430      return (-1);
431    }
432
433    d = SATgetDecision(cm->currentDecision);
434    cm->implicatedSoFar -= d->implied->num;
435    SATante(fdaLit) = 0;
436
437    SATvalue(fdaLit) = inverted;
438    SATmakeImplied(fdaLit, d);
439
440    if((SATflags(fdaLit) & InQueueMask)  == 0) {
441      sat_Enqueue(cm->queue, fdaLit);
442      SATflags(fdaLit) |= InQueueMask;
443    }
444
445    clauseArray->num = 0;
446
447    if(option->incTraceObjective && objectFlag == 0)
448      sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(fdaLit));
449
450    if(option->incDistill && objectFlag)
451      sat_ArrayInsert(cm->objUnitLitArray, SATnot(fdaLit));
452
453    if(objectFlag)
454      SATflags(fdaLit) |= ObjMask;
455
456    /* Bing: UNSAT core generation */
457    if(cm->option->coreGeneration){
458      if(cm->option->RT){
459        st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
460
461        st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
462        RT_oriClsIdx(rm->root) = learned;
463         }
464      else{
465        st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
466        st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
467      }
468    }
469    return(bLevel);
470  }
471
472  if(strongFlag && (SATnumConflict(conflicting) % 5) == 0 &&
473          clauseArray->num > 4) {
474    nClauseArray = sat_ArrayAlloc(clauseArray->num);
475    memcpy(nClauseArray->space, clauseArray->space, sizeof(long)*clauseArray->num);
476    nClauseArray->num = clauseArray->num;
477    clauseArray->num = 0;
478    bLevel = sat_ConflictAnalysisUsingAuxImplication(cm, nClauseArray);
479    sat_ArrayFree(nClauseArray);
480  }
481  else {
482    /* add conflict learned clause */
483    learned = sat_AddConflictClause(cm, clauseArray, objectFlag);
484    cm->currentTopConflict = cm->literals->last-1;
485    cm->currentTopConflictCount = 0;
486
487     /* Bing: UNSAT core generation */
488    if(cm->option->coreGeneration){
489
490      if(cm->option->RT){
491        st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
492        RT_oriClsIdx(rm->root) = learned;
493        }
494      else{
495        st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
496      }
497    }
498
499    if(option->verbose > 2) {
500      sat_PrintNode(cm, learned);
501      fflush(cm->stdOut);
502    }
503
504
505    /* apply Deepest Variable Hike decision heuristic */
506    if(option->decisionHeuristic & DVH_DECISION)
507      sat_UpdateDVH(cm, d, clauseArray, bLevel, fdaLit);
508
509    /* Backtrack and failure driven assertion */
510    sat_Backtrack(cm, bLevel);
511
512    d = SATgetDecision(bLevel);
513    cm->implicatedSoFar -= d->implied->num;
514
515    SATante(fdaLit) = learned;
516    SATvalue(fdaLit) = inverted;
517    SATmakeImplied(fdaLit, d);
518
519    if((SATflags(fdaLit) & InQueueMask)  == 0) {
520      sat_Enqueue(cm->queue, fdaLit);
521      SATflags(fdaLit) |= InQueueMask;
522    }
523
524    clauseArray->num = 0;
525    if(objectFlag)
526      SATflags(fdaLit) |= ObjMask;
527
528  }
529
530  return(bLevel);
531}
532
533/**Function********************************************************************
534
535  Synopsis    [ Add conflict clause and backtrack.]
536
537  Description [ Add conflict clause and backtrack.]
538
539  SideEffects []
540
541  SeeAlso     []
542
543******************************************************************************/
544int
545sat_AddConflictClauseAndBacktrackForLifting(
546        satManager_t *cm,
547        satArray_t *clauseArray,
548        satLevel_t *d,
549        long fdaLit,
550        int bLevel,
551        int objectFlag,
552        int strongFlag)
553{
554int inverted;
555long conflicting, learned;
556satOption_t *option;
557satStatistics_t *stats;
558satArray_t *nClauseArray;
559
560  option = cm->option;
561  stats = cm->each;
562
563  inverted = SATisInverted(fdaLit);
564  fdaLit = SATnormalNode(fdaLit);
565
566  conflicting = d->conflict;
567
568  if(option->verbose > 2) {
569    if(option->verbose > 4)
570      sat_PrintNode(cm, conflicting);
571    fprintf(cm->stdOut, "conflict at %3d on %6ld  bLevel %d UnitLit ",
572            d->level, conflicting, bLevel);
573    sat_PrintNodeAlone(cm, fdaLit);
574    fprintf(cm->stdOut, "\n");
575  }
576
577  d->conflict = 0;
578
579  /* unit literal conflict clause */
580  if(clauseArray->num == 1) {
581    learned = sat_AddUnitConflictClause(cm, clauseArray, objectFlag);
582    stats->nUnitConflictCl++;
583    cm->currentTopConflict = cm->literals->last-1;
584    cm->currentTopConflictCount = 0;
585
586    sat_Backtrack(cm, 0);
587
588    if(SATlevel(fdaLit) == 0) {
589      if(cm->option->coreGeneration){
590        st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
591        st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
592      }
593      cm->currentDecision = -1;
594      return (-1);
595    }
596
597    d = SATgetDecision(cm->currentDecision);
598    cm->implicatedSoFar -= d->implied->num;
599    SATante(fdaLit) = 0;
600
601    SATvalue(fdaLit) = inverted;
602    SATmakeImplied(fdaLit, d);
603
604    if((SATflags(fdaLit) & InQueueMask)  == 0) {
605      sat_Enqueue(cm->queue, fdaLit);
606      SATflags(fdaLit) |= InQueueMask;
607    }
608
609    clauseArray->num = 0;
610
611    if(option->incTraceObjective && objectFlag == 0)
612      sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(fdaLit));
613
614    if(option->incDistill && objectFlag)
615      sat_ArrayInsert(cm->objUnitLitArray, SATnot(fdaLit));
616
617    if(objectFlag)
618      SATflags(fdaLit) |= ObjMask;
619
620    /* Bing: UNSAT core generation */
621    if(cm->option->coreGeneration){
622      st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
623      st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
624    }
625    return(0);
626  }
627
628  if(strongFlag && (SATnumConflict(conflicting) % 5) == 0 &&
629          clauseArray->num > 4) {
630    nClauseArray = sat_ArrayAlloc(clauseArray->num);
631    memcpy(nClauseArray->space, clauseArray->space, sizeof(long)*clauseArray->num);
632    nClauseArray->num = clauseArray->num;
633    clauseArray->num = 0;
634    bLevel = sat_ConflictAnalysisUsingAuxImplication(cm, nClauseArray);
635    sat_ArrayFree(nClauseArray);
636  }
637  else {
638    /* add conflict learned clause */
639    learned = sat_AddConflictClause(cm, clauseArray, objectFlag);
640    cm->currentTopConflict = cm->literals->last-1;
641    cm->currentTopConflictCount = 0;
642
643     /* Bing: UNSAT core generation */
644    if(cm->option->coreGeneration){
645      st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
646    }
647
648    if(option->verbose > 2) {
649      sat_PrintNode(cm, learned);
650      fflush(cm->stdOut);
651    }
652
653
654    /* apply Deepest Variable Hike decision heuristic */
655    /**
656    if(option->decisionHeuristic & DVH_DECISION)
657      sat_UpdateDVH(cm, d, clauseArray, bLevel, fdaLit);
658      **/
659
660    /* Backtrack and failure driven assertion */
661    sat_Backtrack(cm, bLevel);
662
663    d = SATgetDecision(bLevel);
664    cm->implicatedSoFar -= d->implied->num;
665
666    SATante(fdaLit) = learned;
667    SATvalue(fdaLit) = inverted;
668    SATmakeImplied(fdaLit, d);
669
670    if((SATflags(fdaLit) & InQueueMask)  == 0) {
671      sat_Enqueue(cm->queue, fdaLit);
672      SATflags(fdaLit) |= InQueueMask;
673    }
674
675    clauseArray->num = 0;
676    if(objectFlag)
677      SATflags(fdaLit) |= ObjMask;
678
679  }
680
681  return(bLevel);
682}
683
684/**Function********************************************************************
685
686  Synopsis    [ Add conflict clause with no score update and backtrack.]
687
688  Description [ Add conflict clause with no score update and backtrack.]
689
690  SideEffects []
691
692  SeeAlso     []
693
694******************************************************************************/
695int
696sat_AddConflictClauseWithNoScoreAndBacktrack(
697        satManager_t *cm,
698        satArray_t *clauseArray,
699        satLevel_t *d,
700        long fdaLit,
701        int bLevel,
702        int objectFlag,
703        int strongFlag)
704{
705int inverted;
706long conflicting, learned;
707satOption_t *option;
708satStatistics_t *stats;
709satArray_t *nClauseArray;
710
711  option = cm->option;
712  stats = cm->each;
713
714  inverted = SATisInverted(fdaLit);
715  fdaLit = SATnormalNode(fdaLit);
716
717  conflicting = d->conflict;
718
719  if(option->verbose > 2) {
720    if(option->verbose > 4)
721      sat_PrintNode(cm, conflicting);
722    fprintf(cm->stdOut, "conflict at %3d on %6ld  bLevel %d UnitLit ",
723            d->level, conflicting, bLevel);
724    sat_PrintNodeAlone(cm, fdaLit);
725    fprintf(cm->stdOut, "\n");
726  }
727
728  d->conflict = 0;
729
730  /* unit literal conflict clause */
731  if(clauseArray->num == 1) {
732    learned = sat_AddUnitConflictClause(cm, clauseArray, objectFlag);
733    stats->nUnitConflictCl++;
734    cm->currentTopConflict = cm->literals->last-1;
735    cm->currentTopConflictCount = 0;
736
737    sat_Backtrack(cm, 0);
738
739    if(SATlevel(fdaLit) == 0) {
740      if(cm->option->coreGeneration){
741        st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
742        st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
743      }
744      cm->currentDecision = -1;
745      return (-1);
746    }
747
748    d = SATgetDecision(cm->currentDecision);
749    cm->implicatedSoFar -= d->implied->num;
750    SATante(fdaLit) = 0;
751
752    SATvalue(fdaLit) = inverted;
753    SATmakeImplied(fdaLit, d);
754
755    if((SATflags(fdaLit) & InQueueMask)  == 0) {
756      sat_Enqueue(cm->queue, fdaLit);
757      SATflags(fdaLit) |= InQueueMask;
758    }
759
760    clauseArray->num = 0;
761
762    if(option->incTraceObjective && objectFlag == 0)
763      sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(fdaLit));
764
765    if(option->incDistill && objectFlag)
766      sat_ArrayInsert(cm->objUnitLitArray, SATnot(fdaLit));
767
768    if(objectFlag)
769      SATflags(fdaLit) |= ObjMask;
770
771    /* Bing: UNSAT core generation */
772    if(cm->option->coreGeneration){
773      st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
774      st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
775    }
776    return(bLevel);
777  }
778
779  if(strongFlag && (SATnumConflict(conflicting) % 5) == 0 &&
780          clauseArray->num > 4) {
781    nClauseArray = sat_ArrayAlloc(clauseArray->num);
782    memcpy(nClauseArray->space, clauseArray->space, sizeof(long)*clauseArray->num);
783    nClauseArray->num = clauseArray->num;
784    clauseArray->num = 0;
785    bLevel = sat_ConflictAnalysisUsingAuxImplication(cm, nClauseArray);
786    sat_ArrayFree(nClauseArray);
787  }
788  else {
789    /* add conflict learned clause */
790    learned = sat_AddConflictClauseNoScoreUpdate(cm, clauseArray, objectFlag);
791    cm->currentTopConflict = cm->literals->last-1;
792    cm->currentTopConflictCount = 0;
793
794     /* Bing: UNSAT core generation */
795    if(cm->option->coreGeneration){
796      st_insert(cm->dependenceTable, (char *)learned, (char *)cm->dependenceArray);
797    }
798
799    if(option->verbose > 2) {
800      sat_PrintNode(cm, learned);
801      fflush(cm->stdOut);
802    }
803
804
805    /* apply Deepest Variable Hike decision heuristic */
806    if(option->decisionHeuristic & DVH_DECISION)
807      sat_UpdateDVH(cm, d, clauseArray, bLevel, fdaLit);
808
809    /* Backtrack and failure driven assertion */
810    sat_Backtrack(cm, bLevel);
811
812    d = SATgetDecision(bLevel);
813    cm->implicatedSoFar -= d->implied->num;
814
815    SATante(fdaLit) = learned;
816    SATvalue(fdaLit) = inverted;
817    SATmakeImplied(fdaLit, d);
818
819    if((SATflags(fdaLit) & InQueueMask)  == 0) {
820      sat_Enqueue(cm->queue, fdaLit);
821      SATflags(fdaLit) |= InQueueMask;
822    }
823
824    clauseArray->num = 0;
825    if(objectFlag)
826      SATflags(fdaLit) |= ObjMask;
827
828  }
829
830  return(bLevel);
831}
832
833/**Function********************************************************************
834
835  Synopsis    [ Minimize conflict clause by rebuilding implication graph.]
836
837  Description [ Minimize conflict clause by rebuilding implication graph.]
838
839  SideEffects []
840
841  SeeAlso     []
842
843******************************************************************************/
844int
845sat_ConflictAnalysisUsingAuxImplication(
846        satManager_t *cm,
847        satArray_t *clauseArray)
848{
849int tLevel, level, bLevel;
850int i, size;
851int value, tvalue;
852int minConflict, maxConflict;
853long v, tv, conflicting;
854satLevel_t *d;
855satArray_t *nClauseArray;
856double aMean, hMean, gMean;
857int objectFlag;
858long fdaLit;
859
860  SATcm = cm;
861  qsort(clauseArray->space, clauseArray->num, sizeof(int), levelCompare);
862  tLevel = cm->currentDecision;
863
864  tv = clauseArray->space[0];
865  v = SATnormalNode(tv);
866  level = SATlevel(v);
867  minConflict = cm->decisionHead[level].nConflict;
868  tv = clauseArray->space[clauseArray->num-1];
869  v = SATnormalNode(tv);
870  level = SATlevel(v);
871  maxConflict = cm->decisionHead[level].nConflict;
872
873  aMean = hMean = 0;
874
875  for(i=0; i<clauseArray->num; i++) {
876    tv = clauseArray->space[i];
877    v = SATnormalNode(tv);
878    level = SATlevel(v);
879    if(level < tLevel) tLevel = level;
880    aMean = aMean + (double)level;
881    hMean = hMean + 1.0/(double)level;
882  }
883  aMean = aMean/(double)clauseArray->num;
884  hMean = (double)clauseArray->num/hMean;
885  gMean = sqrt(aMean*hMean);
886
887  sat_Backtrack(cm, tLevel-1);
888
889  size = clauseArray->num;
890
891  for(i=0; i<size; i++) {
892    tv = clauseArray->space[i];
893    value = !SATisInverted(tv);
894    v = SATnormalNode(tv);
895    tvalue = SATvalue(v);
896
897    if(tvalue != 2)     {
898        /**
899      if(tvalue != value) {
900        fprintf(stdout, "ERROR : Inconsitent value is implied\n");
901        sat_ReportStatistics(cm, cm->each);
902      }
903      **/
904      continue;
905    }
906    d = sat_AllocLevel(cm);
907
908    SATvalue(v) = value;
909    SATmakeImplied(v, d);
910    d->decisionNode = v;
911    d->nConflict = cm->each->nConflictCl;
912    if((SATflags(v) & InQueueMask) == 0) {
913      sat_Enqueue(cm->queue, v);
914      SATflags(v) |= InQueueMask;
915    }
916    sat_ImplicationMain(cm, d);
917
918    if(d->conflict) {
919      conflicting = d->conflict;
920      break;
921    }
922  }
923
924  if(d->conflict) {
925    nClauseArray = cm->auxArray;
926    bLevel = 0;
927    fdaLit = -1;
928    nClauseArray->num = 0;
929    sat_FindUIP(cm, nClauseArray, d, &objectFlag, &bLevel, &fdaLit);
930
931    /**
932    fprintf(stdout, "tLevel %d gLevel %.1lf  %ld -> %ld min %d max %d\n",
933            tLevel, gMean, clauseArray->num, nClauseArray->num,
934            minConflict, maxConflict);
935            **/
936
937    bLevel = sat_AddConflictClauseAndBacktrack(
938            cm, nClauseArray, d, fdaLit, bLevel, objectFlag, 0);
939
940
941  }
942  else {
943    bLevel = cm->currentDecision;
944  }
945  return(bLevel);
946
947}
948
949
950/**Function********************************************************************
951
952  Synopsis    [ Conflict Analysis that is used for UNSAT core generation.]
953
954  Description [ Conflict Analysis that is used for UNSAT core generation.]
955
956  SideEffects []
957
958  SeeAlso     []
959
960******************************************************************************/
961int
962sat_ConflictAnalysisForCoreGen(
963        satManager_t *cm,
964        satLevel_t *d)
965{
966satStatistics_t *stats;
967satOption_t *option;
968satArray_t *clauseArray;
969int objectFlag;
970int bLevel;
971long fdaLit, learned, conflicting;
972int inverted;
973
974RTManager_t * rm = cm->rm;
975
976  if(d->level != 0) {
977    fprintf(stdout, "ERROR : Can't use this function at higher than level 0\n");
978    return(0);
979  }
980
981  conflicting = d->conflict;
982
983  stats = cm->each;
984  option = cm->option;
985
986  stats->nBacktracks++;
987
988  clauseArray = cm->auxArray;
989
990  bLevel = 0;
991  fdaLit = -1;
992  clauseArray->num = 0;
993
994  /* Find Unique Implication Point */
995
996  if(option->RT)
997    sat_FindUIPForCoreGenWithRT(cm, clauseArray, d, &objectFlag, &bLevel,&fdaLit);
998  else
999    sat_FindUIPForCoreGen(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
1000
1001  if(fdaLit < 0 )
1002    fprintf(stdout, "ERROR : critical\n");
1003
1004  inverted = SATisInverted(fdaLit);
1005  fdaLit = SATnormalNode(fdaLit);
1006
1007  d->conflict = 0;
1008
1009  assert(clauseArray->num == 1);
1010  learned = sat_AddUnitConflictClause(cm, clauseArray, objectFlag);
1011
1012  SATante(fdaLit) = 0;
1013
1014  clauseArray->num = 0;
1015
1016  /* Bing: UNSAT core generation */
1017  if(cm->option->coreGeneration){
1018    st_insert(cm->anteTable,(char*)(long)SATnormalNode(fdaLit),(char*)(long)learned);
1019    if(option->RT){
1020      st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
1021      RT_oriClsIdx(rm->root) = learned;
1022    }
1023    else
1024      st_insert(cm->dependenceTable, (char *)(long)learned, (char *)(long)cm->dependenceArray);
1025  }
1026  return 1;
1027}
1028
1029/**Function********************************************************************
1030
1031  Synopsis    [ Find Unique implication point]
1032
1033  Description [ After finding unique implication point, the backtrack level
1034                and failure driven assertion are identified. ]
1035
1036  SideEffects []
1037
1038  SeeAlso     []
1039
1040******************************************************************************/
1041void
1042sat_FindUIP(
1043        satManager_t *cm,
1044        satArray_t *clauseArray,
1045        satLevel_t *d,
1046        int *objectFlag,
1047        int *bLevel,
1048        long *fdaLit)
1049{
1050long conflicting;
1051int nMarked, value;
1052int first, i;
1053long *space, v;
1054satArray_t *implied;
1055satOption_t *option;
1056
1057  conflicting = d->conflict;
1058  nMarked = 0;
1059  option = cm->option;
1060  if(option->incTraceObjective) *objectFlag = 0;
1061  else                          *objectFlag = ObjMask;
1062
1063  (*objectFlag) |= (SATflags(conflicting) & ObjMask);
1064
1065  /* find seed from conflicting clause to find unique implication point.
1066   * */
1067  clauseArray->num = 0;
1068
1069  if(SATflags(conflicting) & IsCNFMask)
1070    SATconflictUsage(conflicting)++;
1071
1072  sat_MarkNodeInConflict(
1073          cm, d, &nMarked, objectFlag, bLevel, clauseArray);
1074
1075  /* Traverse implication graph backward */
1076  first = 1;
1077  implied = d->implied;
1078  space = implied->space+implied->num-1;
1079  /* Bing:  UNSAT core generation */
1080  if(cm->option->coreGeneration){
1081    cm->dependenceArray = sat_ArrayAlloc(1);
1082    sat_ArrayInsert(cm->dependenceArray,conflicting);
1083  }
1084
1085  for(i=implied->num-1; i>=0; i--, space--) {
1086    v = *space;
1087    if(SATflags(v) & VisitedMask) {
1088      SATflags(v) &= ResetVisitedMask;
1089      --nMarked;
1090
1091      if(nMarked == 0 && (!first || i==0))  {
1092        value = SATvalue(v);
1093        *fdaLit = v^(!value);
1094        sat_ArrayInsert(clauseArray, *fdaLit);
1095        break;
1096      }
1097
1098      /* Bing: UNSAT core genration */
1099      if(cm->option->coreGeneration){
1100        int ante = SATante(v);
1101        if(ante!=0 && !(SATflags(ante) & IsCNFMask)){
1102          printf("node %d is not CNF\n", ante);
1103          exit(0);
1104        }
1105        if(ante==0){
1106          if(!st_lookup(cm->anteTable, (char *)SATnormalNode(v), &ante)){
1107            printf("ante = 0 and is not in anteTable %ld\n",v);
1108            exit(0);
1109          }
1110        }
1111        sat_ArrayInsert(cm->dependenceArray,ante);
1112      }
1113
1114      sat_MarkNodeInImpliedNode(
1115              cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
1116    }
1117    first = 0;
1118  }
1119
1120
1121  /* Minimize conflict clause */
1122  if(option->minimizeConflictClause)
1123    sat_MinimizeConflictClause(cm, clauseArray);
1124  else
1125    sat_ResetFlagForClauseArray(cm, clauseArray);
1126
1127  return;
1128}
1129/**Function********************************************************************
1130
1131  Synopsis    [find UIP with resolution generation]
1132
1133  Description []
1134
1135  SideEffects []
1136
1137  SeeAlso     []
1138
1139******************************************************************************/
1140
1141
1142void
1143sat_FindUIPWithRT(
1144        satManager_t *cm,
1145        satArray_t *clauseArray,
1146        satLevel_t *d,
1147        int *objectFlag,
1148        int *bLevel,
1149        long *fdaLit)
1150{
1151long conflicting;
1152int nMarked, value;
1153int first, i,j;
1154long *space, v,left,right,inverted,result,*tmp;
1155satArray_t *implied;
1156satOption_t *option;
1157RTnode_t  tmprt;
1158int size = 0;
1159long *lp,*tmpIP,ante,ante2,node;
1160 RTManager_t * rm = cm->rm;
1161
1162  conflicting = d->conflict;
1163  nMarked = 0;
1164  option = cm->option;
1165  if(option->incTraceObjective) *objectFlag = 0;
1166  else                          *objectFlag = ObjMask;
1167
1168  (*objectFlag) |= (SATflags(conflicting) & ObjMask);
1169
1170  /* find seed from conflicting clause to find unique implication point.
1171   * */
1172  clauseArray->num = 0;
1173  sat_MarkNodeInConflict(
1174          cm, d, &nMarked, objectFlag, bLevel, clauseArray);
1175
1176  /* Traverse implication graph backward */
1177  first = 1;
1178  implied = d->implied;
1179  space = implied->space+implied->num-1;
1180
1181
1182  if(cm->option->coreGeneration){
1183    /*if last conflict is CNF*/
1184    if(SATflags(conflicting)&IsCNFMask){
1185      /*is conflict CNF*/
1186      if(SATflags(conflicting)&IsConflictMask){
1187         if(!st_lookup(cm->RTreeTable,(char*)conflicting,&tmprt)){
1188            printf("RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
1189            exit(0);
1190          }
1191          else{
1192            rm->root = tmprt;
1193#if PR
1194            printf("Get formula for CONFLICT CLAUSE:%d\n",ante);
1195#endif
1196          }
1197      }
1198      /*CNF but not conflict*/
1199      else{
1200        rm->root = RTCreateNode(rm);
1201
1202        size = SATnumLits(conflicting);
1203        RT_fSize(rm->root) = size;
1204        lp = (long*)SATfirstLit(conflicting);
1205        sat_BuildRT(cm,rm->root, lp, tmpIP,size,0);
1206      }
1207    }
1208    /*if last conflict is AIG*/
1209    else{
1210      rm->root = RTCreateNode(rm);
1211      node = SATnormalNode(conflicting);
1212      left = SATleftChild(node);
1213      right = SATrightChild(node);
1214      result = PureSat_IdentifyConflict(cm,left,right,conflicting);
1215      inverted = SATisInverted(left);
1216      left = SATnormalNode(left);
1217      left = inverted ? SATnot(left) : left;
1218
1219      inverted = SATisInverted(right);
1220      right = SATnormalNode(right);
1221      right = inverted ? SATnot(right) : right;
1222
1223      j = node;
1224
1225      if(result == 1){
1226        tmp = ALLOC(long,3);
1227        tmp[0] = left;
1228        tmp[1] = SATnot(j);
1229        size = 2;
1230      }
1231      else if(result == 2){
1232        tmp = ALLOC(long,3);
1233        tmp[0] = right;
1234        tmp[1] = SATnot(j);
1235        size = 2;
1236      }
1237      else if(result == 3){
1238        tmp = ALLOC(long,4);
1239        tmp[0] = SATnot(left);
1240        tmp[1] = SATnot(right);
1241        tmp[2] = j;
1242        size = 3;
1243      }
1244      else{
1245        printf("wrong returned result value, exit\n");
1246        exit(0);
1247      }
1248
1249      lp = tmp;
1250      sat_BuildRT(cm,rm->root, lp, tmpIP,size,1);
1251      FREE(tmp);
1252    }
1253  }
1254
1255
1256  for(i=implied->num-1; i>=0; i--, space--) {
1257    v = *space;
1258    if(SATflags(v) & VisitedMask) {
1259      SATflags(v) &= ResetVisitedMask;
1260      --nMarked;
1261
1262      if(nMarked == 0 && (!first || i==0))  {
1263        value = SATvalue(v);
1264        *fdaLit = v^(!value);
1265        sat_ArrayInsert(clauseArray, *fdaLit);
1266        break;
1267      }
1268
1269
1270      if(cm->option->coreGeneration){
1271        ante = SATante(v);
1272        if(ante==0){
1273          if(!(st_lookup(cm->anteTable, (char *)SATnormalNode(v),&ante))){
1274            printf("ante = 0 and is not in anteTable %ld\n",v);
1275            exit(0);
1276          }
1277        }
1278
1279        /*build non-leaf node*/
1280        tmprt = RTCreateNode(rm);
1281        RT_pivot(tmprt) = SATnormalNode(v);
1282        RT_right(tmprt) = rm->root;
1283        rm->root = tmprt;
1284
1285        if((SATflags(ante)&IsConflictMask)&&(SATflags(ante)&IsCNFMask)){
1286          if(!st_lookup(cm->RTreeTable,(char*)ante,&tmprt)){
1287            printf("RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
1288            exit(0);
1289          }
1290          else{
1291            RT_left(rm->root) = tmprt;
1292#if PR
1293            printf("Get formula for CONFLICT CLAUSE:%d\n",ante);
1294#endif
1295          }
1296        }
1297        else{ /* if not conflict CNF*/
1298          /*left  */
1299          tmprt = RTCreateNode(rm);
1300          RT_left(rm->root) = tmprt;
1301          /*left is AIG*/
1302          if(!(SATflags(ante) & IsCNFMask)){
1303            /*generate formula for left*/
1304            tmp = ALLOC(long,3);
1305            value = SATvalue(v);
1306            node = SATnormalNode(v);
1307            node = value==1?node:SATnot(node);
1308            tmp[0] = node;
1309
1310            size = 1;
1311            if(ante != SATnormalNode(v)){
1312              value = SATvalue(ante);
1313              node = SATnormalNode(ante);
1314              node = value==1?SATnot(node):node;
1315              tmp[1] = node;
1316              size++;
1317              ante2 = SATante2(v);
1318              if(ante2){
1319                value = SATvalue(ante2);
1320                node = SATnormalNode(ante2);
1321                node = value==1?SATnot(node):node;
1322                tmp[2] = node;
1323                size++;
1324              }
1325            }
1326
1327            lp = tmp;
1328            sat_BuildRT(cm,tmprt,lp,tmpIP,size,1);
1329            FREE(tmp);
1330          }
1331          /* left is CNF*/
1332          else{
1333
1334            lp = (long*)SATfirstLit(ante);
1335            size = SATnumLits(ante);
1336            RT_fSize(tmprt) = size;
1337            sat_BuildRT(cm,tmprt, lp, tmpIP,size,0);
1338          }
1339        } /*else{ // if not conflict CNF*/
1340
1341      }/*if(cm->option->coreGeneration){*/
1342
1343
1344      sat_MarkNodeInImpliedNode(
1345              cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
1346    }
1347    first = 0;
1348  }
1349
1350
1351  /* Minimize conflict clause */
1352  if(option->minimizeConflictClause)
1353    sat_MinimizeConflictClause(cm, clauseArray);
1354  else
1355    sat_ResetFlagForClauseArray(cm, clauseArray);
1356
1357  return;
1358}
1359
1360/**Function********************************************************************
1361
1362  Synopsis    [ Find Unique implication point and find cut to generate additional conflict clause]
1363
1364  Description [ After finding unique implication point, the backtrack level
1365                and failure driven assertion are identified. ]
1366
1367  SideEffects []
1368
1369  SeeAlso     []
1370
1371******************************************************************************/
1372void
1373sat_FindUIPAndNonUIP(
1374        satManager_t *cm,
1375        satArray_t *clauseArray,
1376        satLevel_t *d,
1377        int *objectFlag,
1378        int *bLevel,
1379        long *fdaLit)
1380{
1381long conflicting;
1382int nMarked, value;
1383int first, i, j;
1384int size, oSize;
1385int depth, maxSize;
1386long *space, v, nv, maxV;
1387long ante, ante2;
1388long learned;
1389long *plit;
1390satArray_t *implied;
1391satArray_t *nClauseArray;
1392satOption_t *option;
1393int tLevel, inverted, lBacktrace, uBacktrace;
1394int minLimit, markLimit, tObjectFlag;
1395int inserted;
1396long tFdaLit;
1397
1398/** HSJIN : Need to be update to make it consider UNSAT core generation **/
1399  conflicting = d->conflict;
1400  nMarked = 0;
1401  option = cm->option;
1402  if(option->incTraceObjective) *objectFlag = 0;
1403  else                          *objectFlag = ObjMask;
1404
1405  (*objectFlag) |= (SATflags(conflicting) & ObjMask);
1406
1407  /* find seed from conflicting clause to find unique implication point.
1408   * */
1409  clauseArray->num = 0;
1410
1411  if(SATflags(conflicting) & IsCNFMask)
1412    SATconflictUsage(conflicting)++;
1413
1414  sat_MarkNodeInConflict(
1415          cm, d, &nMarked, objectFlag, bLevel, clauseArray);
1416
1417  /* Traverse implication graph backward */
1418  first = 1;
1419  implied = d->implied;
1420  space = implied->space+implied->num-1;
1421  maxSize = 0;
1422  maxV = 0;
1423  /* Bing:  UNSAT core generation */
1424  if(cm->option->coreGeneration){
1425    cm->dependenceArray = sat_ArrayAlloc(1);
1426    sat_ArrayInsert(cm->dependenceArray,conflicting);
1427  }
1428
1429  for(i=implied->num-1; i>=0; i--, space--) {
1430    v = *space;
1431    if(SATflags(v) & VisitedMask) {
1432      SATflags(v) &= ResetVisitedMask;
1433      --nMarked;
1434
1435      depth = cm->variableArray[SATnodeID(v)].depth;
1436      if(nMarked == 0 && (!first || i==0))  {
1437        value = SATvalue(v);
1438        *fdaLit = v^(!value);
1439        sat_ArrayInsert(clauseArray, *fdaLit);
1440        break;
1441      }
1442
1443      ante = SATante(v);
1444      /* Bing: UNSAT core genration */
1445      if(cm->option->coreGeneration){
1446        if(ante!=0 && !(SATflags(ante) & IsCNFMask)){
1447          printf("node %ld is not CNF\n", ante);
1448          exit(0);
1449        }
1450        if(ante==0){
1451          if(!st_lookup(cm->anteTable, (char *)SATnormalNode(v), &ante)){
1452            printf("ante = 0 and is not in anteTable %ld\n",v);
1453            exit(0);
1454          }
1455        }
1456        sat_ArrayInsert(cm->dependenceArray,ante);
1457      }
1458
1459      /**
1460      sat_MarkNodeInImpliedNode(
1461              cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
1462              **/
1463
1464      if(SATflags(ante) & IsCNFMask) {
1465        SATconflictUsage(ante)++;
1466        size = SATnumLits(ante);
1467        oSize = clauseArray->num;
1468        for(j=0, plit=(long*)SATfirstLit(ante); j<size; j++, plit++) {
1469          nv = SATgetNode(*plit);
1470          if(SATnormalNode(nv) != v)    {
1471            sat_MarkNodeSub(cm, nv, &nMarked, bLevel, d, clauseArray);
1472            if(cm->variableArray[SATnodeID(nv)].depth <= depth) {
1473              cm->variableArray[SATnodeID(nv)].depth = depth+1;
1474            }
1475          }
1476        }
1477        oSize = clauseArray->num-oSize;
1478        if(oSize > maxSize) {
1479          maxSize = oSize;
1480          maxV = v;
1481        }
1482      }
1483      else {
1484        sat_MarkNodeSub(cm, ante, &nMarked, bLevel, d, clauseArray);
1485        ante2 = SATante2(v);
1486        if(ante2)
1487          sat_MarkNodeSub(cm, ante2, &nMarked, bLevel, d, clauseArray);
1488      }
1489
1490    }
1491    first = 0;
1492  }
1493
1494  /* Minimize conflict clause */
1495  if(option->minimizeConflictClause)
1496    sat_MinimizeConflictClause(cm, clauseArray);
1497  else
1498    sat_ResetFlagForClauseArray(cm, clauseArray);
1499
1500  if(maxSize > clauseArray->num/4 && maxSize > 5) {
1501    nClauseArray = sat_ArrayAlloc(clauseArray->num);
1502
1503    nMarked = 0;
1504    tLevel = 0;
1505    tObjectFlag |= (SATflags(conflicting) & ObjMask);
1506
1507    sat_MarkNodeInConflict(
1508          cm, d, &nMarked, &tObjectFlag, &tLevel, nClauseArray);
1509
1510    /* Traverse implication graph backward */
1511    first = 1;
1512    implied = d->implied;
1513    space = implied->space+implied->num-1;
1514    for(i=implied->num-1; i>=0; i--, space--) {
1515      v = *space;
1516      if(v == maxV) {
1517        if(SATflags(v) & VisitedMask) {
1518          SATflags(v) &= ResetVisitedMask;
1519          --nMarked;
1520          value = SATvalue(v);
1521          sat_ArrayInsert(nClauseArray, v^(!value));
1522        }
1523        continue;
1524      }
1525
1526      if(SATflags(v) & VisitedMask) {
1527        SATflags(v) &= ResetVisitedMask;
1528        --nMarked;
1529
1530        if(nMarked == 0 && (!first || i == 0))  {
1531          value = SATvalue(v);
1532          tFdaLit = v^(!value);
1533          sat_ArrayInsert(nClauseArray, tFdaLit);
1534          break;
1535        }
1536
1537        ante= SATante(v);
1538        inverted = SATisInverted(ante);
1539        ante= SATnormalNode(ante);
1540
1541        if(SATflags(ante) & IsCNFMask) {
1542          size = SATnumLits(ante);
1543          for(j=0, plit=(long*)SATfirstLit(ante); j<size; j++, plit++) {
1544            nv = SATgetNode(*plit);
1545            if(SATnormalNode(nv) != v)
1546              sat_MarkNodeSub(cm, nv, &nMarked, &tLevel, d, nClauseArray);
1547          }
1548        }
1549        else {
1550          sat_MarkNodeSub(cm, ante, &nMarked, &tLevel, d, nClauseArray);
1551          ante2 = SATante2(v);
1552          if(ante2)
1553            sat_MarkNodeSub(cm, ante2, &nMarked, &tLevel, d, nClauseArray);
1554        }
1555      }
1556      first = 0;
1557    }
1558    sat_MinimizeConflictClause(cm, nClauseArray);
1559
1560    inserted = 0;
1561    if(clauseArray->num*4/5 > nClauseArray->num) {
1562      learned = sat_AddConflictClauseNoScoreUpdate(cm, nClauseArray, tObjectFlag);
1563      inserted = 1;
1564    }
1565    sat_ArrayFree(nClauseArray);
1566  }
1567  if( inserted == 0 &&
1568      depth > 20) {
1569    nClauseArray = sat_ArrayAlloc(clauseArray->num);
1570
1571    lBacktrace = depth/3;
1572    uBacktrace = depth*2/3;
1573
1574    /** HSJIN : depth, lBacktrace and uBacktrace may affect to
1575     * performance **/
1576    markLimit = 1;
1577    minLimit = 1000;
1578    while(1){
1579      nMarked = 0;
1580      tLevel = 0;
1581      depth = 0;
1582      nClauseArray->num = 0;
1583      markLimit++;
1584      if(markLimit > 3) break;
1585      if(minLimit != 1000 && minLimit > 3)
1586        break;
1587      tObjectFlag |= (SATflags(conflicting) & ObjMask);
1588
1589      sat_MarkNodeInConflict(
1590            cm, d, &nMarked, &tObjectFlag, &tLevel, nClauseArray);
1591
1592      first = 1;
1593      implied = d->implied;
1594      space = implied->space+implied->num-1;
1595      for(i=implied->num-1; i>=0; i--, space--) {
1596        v = *space;
1597        if(uBacktrace < depth) {
1598          sat_ResetFlagForClauseArray(cm, nClauseArray);
1599          nClauseArray->num = 0;
1600          for(; i>=0; i--, space--) {
1601            v = *space;
1602            if(SATflags(v) & VisitedMask) {
1603              SATflags(v) &= ResetVisitedMask;
1604              --nMarked;
1605              if(nMarked == 0)
1606                break;
1607            }
1608          }
1609          break;
1610        }
1611        if(nMarked < minLimit)
1612          minLimit = nMarked;
1613        if(depth > lBacktrace && nMarked < markLimit) {
1614          for(; i>=0; i--, space--) {
1615            v = *space;
1616            if(SATflags(v) & VisitedMask) {
1617              SATflags(v) &= ResetVisitedMask;
1618              --nMarked;
1619              value = SATvalue(v);
1620              sat_ArrayInsert(nClauseArray, v^(!value));
1621              if(nMarked == 0)
1622                break;
1623            }
1624          }
1625        }
1626
1627        if(SATflags(v) & VisitedMask) {
1628          depth = cm->variableArray[SATnodeID(v)].depth;
1629
1630          SATflags(v) &= ResetVisitedMask;
1631          --nMarked;
1632
1633          if(nMarked == 0 && (!first || i == 0))  {
1634            value = SATvalue(v);
1635            tFdaLit = v^(!value);
1636            sat_ArrayInsert(nClauseArray, tFdaLit);
1637            break;
1638          }
1639
1640          ante= SATante(v);
1641          inverted = SATisInverted(ante);
1642          ante= SATnormalNode(ante);
1643
1644          if(SATflags(ante) & IsCNFMask) {
1645            size = SATnumLits(ante);
1646            for(j=0, plit=(long*)SATfirstLit(ante); j<size; j++, plit++) {
1647              nv = SATgetNode(*plit);
1648              if(SATnormalNode(nv) != v)
1649                sat_MarkNodeSub(cm, nv, &nMarked, &tLevel, d, nClauseArray);
1650            }
1651          }
1652          else {
1653            sat_MarkNodeSub(cm, ante, &nMarked, &tLevel, d, nClauseArray);
1654            ante2 = SATante2(v);
1655            if(ante2)
1656              sat_MarkNodeSub(cm, ante2, &nMarked, &tLevel, d, nClauseArray);
1657          }
1658        }
1659        first = 0;
1660      }
1661      if(nClauseArray->num == 0)
1662        continue;
1663      sat_MinimizeConflictClause(cm, nClauseArray);
1664
1665      if(clauseArray->num*4/5 > nClauseArray->num) {
1666
1667        learned = sat_AddConflictClauseNoScoreUpdate(cm, nClauseArray, tObjectFlag);
1668        break;
1669      }
1670    }
1671    sat_ArrayFree(nClauseArray);
1672  }
1673
1674  return;
1675}
1676
1677/**Function********************************************************************
1678
1679  Synopsis    [ UIP Analysis that is used for UNSAT core generation.]
1680
1681  Description [ UIP Analysis that is used for UNSAT core generation.]
1682
1683  SideEffects []
1684
1685  SeeAlso     []
1686
1687******************************************************************************/
1688void
1689sat_FindUIPForCoreGen(
1690        satManager_t *cm,
1691        satArray_t *clauseArray,
1692        satLevel_t *d,
1693        int *objectFlag,
1694        int *bLevel,
1695        long *fdaLit)
1696{
1697long conflicting;
1698int nMarked, value;
1699long v;
1700int first, i;
1701long *space;
1702satArray_t *implied;
1703satOption_t *option;
1704
1705  conflicting = d->conflict;
1706  nMarked = 0;
1707  option = cm->option;
1708  if(option->incTraceObjective) *objectFlag = 0;
1709  else                          *objectFlag = ObjMask;
1710
1711  (*objectFlag) |= (SATflags(conflicting) & ObjMask);
1712
1713  /*  find seed from conflicting clause to find unique implication point. */
1714  clauseArray->num = 0;
1715  sat_MarkNodeInConflict(
1716          cm, d, &nMarked, objectFlag, bLevel, clauseArray);
1717
1718  /* Traverse implication graph backward */
1719  first = 1;
1720  implied = d->implied;
1721  space = implied->space+implied->num-1;
1722  /* Bing: UNSAT core generation */
1723  if(cm->option->coreGeneration){
1724    cm->dependenceArray = sat_ArrayAlloc(1);
1725    sat_ArrayInsert(cm->dependenceArray,conflicting);
1726  }
1727
1728  for(i=implied->num-1; i>=0; i--, space--) {
1729    v = *space;
1730    if(SATflags(v) & VisitedMask) {
1731      SATflags(v) &= ResetVisitedMask;
1732      --nMarked;
1733
1734      if(nMarked == 0 && (!first || i==0))  {
1735        value = SATvalue(v);
1736        *fdaLit = v^(!value);
1737        sat_ArrayInsert(clauseArray, *fdaLit);
1738        break;
1739      }
1740
1741
1742       /* Bing: UNSAT core generation */
1743      if(cm->option->coreGeneration){
1744        int ante = SATante(v);
1745        if(ante!=0 && !(SATflags(ante) & IsCNFMask)){
1746          printf("node %d is not CNF\n", ante);
1747          exit(0);
1748        }
1749        if(ante==0){
1750          if(!st_lookup(cm->anteTable, (char *)SATnormalNode(v), &ante)){
1751            printf("ante = 0 and is not in anteTable %ld\n",v);
1752            exit(0);
1753          }
1754        }
1755        sat_ArrayInsert(cm->dependenceArray,ante);
1756      }
1757
1758
1759      sat_MarkNodeInImpliedNode(
1760              cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
1761    }
1762    first = 0;
1763  }
1764
1765  sat_ResetFlagForClauseArray(cm, clauseArray);
1766
1767  return;
1768}
1769
1770/**Function********************************************************************
1771
1772  Synopsis    [find UIP with resolution generation]
1773
1774  Description []
1775
1776  SideEffects []
1777
1778  SeeAlso     []
1779
1780******************************************************************************/
1781
1782
1783void
1784sat_FindUIPForCoreGenWithRT(
1785        satManager_t *cm,
1786        satArray_t *clauseArray,
1787        satLevel_t *d,
1788        int *objectFlag,
1789        int *bLevel,
1790        long *fdaLit)
1791{
1792long conflicting;
1793int nMarked, value;
1794 long v,left,right,inverted,result;
1795int first, i,size=0;
1796long *space,*tmp;
1797satArray_t *implied;
1798satOption_t *option;
1799RTnode_t tmprt;
1800long  *lp, *tmpIP,ante,ante2,node,j;
1801 RTManager_t * rm = cm->rm;
1802
1803  conflicting = d->conflict;
1804  nMarked = 0;
1805  option = cm->option;
1806  if(option->incTraceObjective) *objectFlag = 0;
1807  else                          *objectFlag = ObjMask;
1808
1809  (*objectFlag) |= (SATflags(conflicting) & ObjMask);
1810
1811  /*  find seed from conflicting clause to find unique implication point. */
1812  clauseArray->num = 0;
1813  sat_MarkNodeInConflict(
1814          cm, d, &nMarked, objectFlag, bLevel, clauseArray);
1815
1816  /* Traverse implication graph backward */
1817  first = 1;
1818  implied = d->implied;
1819  space = implied->space+implied->num-1;
1820
1821
1822  if(cm->option->coreGeneration){
1823    /*if last conflict is CNF*/
1824    if(SATflags(conflicting)&IsCNFMask){
1825      /*is conflict CNF*/
1826      if(SATflags(conflicting)&IsConflictMask){
1827         if(!st_lookup(cm->RTreeTable,(char*)conflicting,&tmprt)){
1828            printf("RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
1829            exit(0);
1830          }
1831          else{
1832            rm->root = tmprt;
1833#if PR
1834            printf("Get formula for CONFLICT CLAUSE:%d\n",ante);
1835#endif
1836          }
1837      }
1838      /*CNF but not conflict*/
1839      else{
1840        rm->root = RTCreateNode(rm);
1841
1842        size = SATnumLits(conflicting);
1843        RT_fSize(rm->root) = size;
1844        lp = (long*)SATfirstLit(conflicting);
1845        sat_BuildRT(cm,rm->root, lp, tmpIP,size,0);
1846      }
1847    }
1848    /*if last conflict is AIG*/
1849    else{
1850      rm->root = RTCreateNode(rm);
1851      node = SATnormalNode(conflicting);
1852      left = SATleftChild(node);
1853      right = SATrightChild(node);
1854      result = PureSat_IdentifyConflict(cm,left,right,conflicting);
1855      inverted = SATisInverted(left);
1856      left = SATnormalNode(left);
1857      left = inverted ? SATnot(left) : left;
1858
1859      inverted = SATisInverted(right);
1860      right = SATnormalNode(right);
1861      right = inverted ? SATnot(right) : right;
1862
1863      j = node;
1864
1865      if(result == 1){
1866        tmp = ALLOC(long,3);
1867        tmp[0] = left;
1868        tmp[1] = SATnot(j);
1869        size = 2;
1870      }
1871      else if(result == 2){
1872        tmp = ALLOC(long,3);
1873        tmp[0] = right;
1874        tmp[1] = SATnot(j);
1875        size = 2;
1876      }
1877      else if(result == 3){
1878        tmp = ALLOC(long,4);
1879        tmp[0] = SATnot(left);
1880        tmp[1] = SATnot(right);
1881        tmp[2] = j;
1882        size = 3;
1883      }
1884      else{
1885        printf("wrong returned result value, exit\n");
1886        exit(0);
1887      }
1888
1889      lp = tmp;
1890      sat_BuildRT(cm,rm->root, lp, tmpIP,size,1);
1891      FREE(tmp);
1892    }
1893  }
1894
1895
1896
1897  for(i=implied->num-1; i>=0; i--, space--) {
1898    v = *space;
1899    if(SATflags(v) & VisitedMask) {
1900      SATflags(v) &= ResetVisitedMask;
1901      --nMarked;
1902
1903      if(nMarked == 0 && (!first || i==0))  {
1904        value = SATvalue(v);
1905        *fdaLit = v^(!value);
1906        sat_ArrayInsert(clauseArray, *fdaLit);
1907        break;
1908      }
1909
1910
1911      if(cm->option->coreGeneration){
1912        ante = SATante(v);
1913        if(ante==0){
1914          if(!(st_lookup(cm->anteTable, (char *)SATnormalNode(v),&ante))){
1915            printf("ante = 0 and is not in anteTable %ld\n",v);
1916            exit(0);
1917          }
1918        }
1919
1920        /*build non-leaf node*/
1921        tmprt = RTCreateNode(rm);
1922        RT_pivot(tmprt) = SATnormalNode(v);
1923        RT_right(tmprt) = rm->root;
1924        rm->root = tmprt;
1925
1926        if((SATflags(ante)&IsConflictMask)&&(SATflags(ante)&IsCNFMask)){
1927          if(!st_lookup(cm->RTreeTable,(char*)ante,&tmprt)){
1928            printf("RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
1929            exit(0);
1930          }
1931          else{
1932            RT_left(rm->root) = tmprt;
1933#if PR
1934            printf("Get formula for CONFLICT CLAUSE:%d\n",ante);
1935#endif
1936          }
1937        }
1938        else{ /* if not conflict CNF*/
1939          /*left */
1940          tmprt = RTCreateNode(rm);
1941          RT_left(rm->root) = tmprt;
1942          /*left is AIG*/
1943          if(!(SATflags(ante) & IsCNFMask)){
1944            /*generate formula for left*/
1945            tmp = ALLOC(long,3);
1946            value = SATvalue(v);
1947            node = SATnormalNode(v);
1948            node = value==1?node:SATnot(node);
1949            tmp[0] = node;
1950
1951            size = 1;
1952            if(ante != SATnormalNode(v)){
1953              value = SATvalue(ante);
1954              node = SATnormalNode(ante);
1955              node = value==1?SATnot(node):node;
1956              tmp[1] = node;
1957              size++;
1958              ante2 = SATante2(v);
1959              if(ante2){
1960                value = SATvalue(ante2);
1961                node = SATnormalNode(ante2);
1962                node = value==1?SATnot(node):node;
1963                tmp[2] = node;
1964                size++;
1965              }
1966            }
1967
1968            lp = tmp;
1969            sat_BuildRT(cm,tmprt,lp,tmpIP,size,1);
1970            FREE(tmp);
1971          }
1972          /* left is CNF*/
1973          else{
1974
1975            lp = (long*)SATfirstLit(ante);
1976            size = SATnumLits(ante);
1977            RT_fSize(tmprt) = size;
1978            sat_BuildRT(cm,tmprt, lp, tmpIP,size,0);
1979          }
1980        } /*else{ // if not conflict CNF*/
1981
1982      }/*if(cm->option->coreGeneration){*/
1983
1984
1985      sat_MarkNodeInImpliedNode(
1986              cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
1987    }
1988    first = 0;
1989  }
1990
1991  sat_ResetFlagForClauseArray(cm, clauseArray);
1992
1993  return;
1994}
1995
1996
1997
1998/**Function********************************************************************
1999
2000  Synopsis    [ Minimize the literals of conflict clause]
2001
2002  Description [ If the literal can be implied by other literals in
2003                conflict clause then we can delete it from conflict clause.]
2004
2005  SideEffects []
2006
2007  SeeAlso     []
2008
2009******************************************************************************/
2010void
2011sat_MinimizeConflictClause(
2012        satManager_t *cm,
2013        satArray_t *clauseArray)
2014{
2015int i, j, size, all, tsize;
2016int inverted;
2017long v, tv;
2018long ante, ante2;
2019long *plit;
2020satArray_t *newArray;
2021satVariable_t *var;
2022
2023  size = clauseArray->num;
2024  newArray = sat_ArrayAlloc(size);
2025  for(i=0; i<size; i++) {
2026    v = clauseArray->space[i];
2027    inverted = SATisInverted(v);
2028    v = SATnormalNode(v);
2029
2030    ante = SATante(v);
2031    ante = SATnormalNode(ante);
2032    if(SATflags(ante) & IsCNFMask) {
2033      tsize = SATnumLits(ante);
2034      all = 1;
2035      for(j=0, plit=(long*)SATfirstLit(ante); j<tsize; j++, plit++) {
2036        tv = SATgetNode(*plit);
2037        tv = SATnormalNode(tv);
2038        if(tv == v)     continue;
2039        if(!(SATflags(tv) & NewMask)) {
2040          all = 0;
2041          break;
2042        }
2043      }
2044      if(all) {
2045        var = SATgetVariable(v);
2046        if(inverted)    (var->litsCount[1])++;
2047        else            (var->litsCount[0])++;
2048        continue;
2049      }
2050    }
2051    else {
2052      if(SATflags(ante) & NewMask) {
2053        ante2 = SATante2(v);
2054        ante2 = SATnormalNode(ante2);
2055        if((ante2==0) || (SATflags(ante2) & NewMask)) {
2056          var = SATgetVariable(v);
2057          if(inverted)  (var->litsCount[1])++;
2058          else          (var->litsCount[0])++;
2059          continue;
2060        }
2061      }
2062    }
2063    sat_ArrayInsert(newArray, v^inverted);
2064  }
2065  sat_ResetFlagForClauseArray(cm, clauseArray);
2066  memcpy(clauseArray->space, newArray->space, sizeof(long)*(newArray->num));
2067  clauseArray->num = newArray->num;
2068  sat_ArrayFree(newArray);
2069}
2070
2071/**Function********************************************************************
2072
2073  Synopsis    [ Reset flags that are used to indentify conflict clause]
2074
2075  Description [ Reset flags that are used to indentify conflict clause]
2076
2077  SideEffects []
2078
2079  SeeAlso     []
2080
2081******************************************************************************/
2082void
2083sat_ResetFlagForClauseArray(
2084        satManager_t *cm,
2085        satArray_t *clauseArray)
2086{
2087int size, i;
2088long v;
2089
2090  size = clauseArray->num;
2091  for(i=0; i<size; i++) {
2092    v = clauseArray->space[i];
2093    v = SATnormalNode(v);
2094    SATflags(v) &= ResetNewVisitedMask;
2095  }
2096}
2097
2098/**Function********************************************************************
2099
2100  Synopsis    [ Find seed for unique implication point analysis
2101                from conflicting clause]
2102
2103  Description [ Find seed for unique implication point analysis
2104                from conflicting clause]
2105
2106  SideEffects []
2107
2108  SeeAlso     []
2109
2110******************************************************************************/
2111void
2112sat_MarkNodeInConflict(
2113        satManager_t *cm,
2114        satLevel_t *d,
2115        int *nMarked,
2116        int *objectFlag,
2117        int *bLevel,
2118        satArray_t *clauseArray)
2119{
2120satOption_t *option;
2121
2122  option = cm->option;
2123  if(option->incTraceObjective == 0) {
2124    sat_MarkNodeInConflictClauseNoObj(
2125        cm, d, nMarked, objectFlag, bLevel, clauseArray);
2126  }
2127  else if(option->incTraceObjective == 1) { /* conservative */
2128    sat_MarkNodeInConflictClauseObjConservative(
2129        cm, d, nMarked, objectFlag, bLevel, clauseArray);
2130  }
2131}
2132
2133/**Function********************************************************************
2134
2135  Synopsis    [ Traverse the antecedent to find unique implication point]
2136
2137  Description [ Traverse the antecedent to find unique implication point]
2138
2139  SideEffects []
2140
2141  SeeAlso     []
2142
2143******************************************************************************/
2144void
2145sat_MarkNodeInImpliedNode(
2146        satManager_t *cm,
2147        satLevel_t *d,
2148        long v,
2149        int *nMarked,
2150        int *objectFlag,
2151        int *bLevel,
2152        satArray_t *clauseArray)
2153{
2154satOption_t *option;
2155
2156  option = cm->option;
2157  if(option->incTraceObjective == 0) {
2158    sat_MarkNodeInImpliedNodeNoObj(
2159        cm, d, v, nMarked, objectFlag, bLevel, clauseArray);
2160  }
2161  else if(option->incTraceObjective == 1) { /* conservative */
2162    sat_MarkNodeInImpliedNodeObjConservative(
2163        cm, d, v, nMarked, objectFlag, bLevel, clauseArray);
2164  }
2165}
2166
2167/**Function********************************************************************
2168
2169  Synopsis    [ If the node is implied in current level then mark it,
2170                otherwise add it to conflict clause]
2171
2172  Description [ If the node is implied in current level then mark it,
2173                otherwise add it to conflict clause]
2174
2175  SideEffects []
2176
2177  SeeAlso     []
2178
2179******************************************************************************/
2180void
2181sat_MarkNodeSub(
2182        satManager_t *cm,
2183        long v,
2184        int *nMarked,
2185        int *bLevel,
2186        satLevel_t *d,
2187        satArray_t *clauseArray)
2188{
2189satLevel_t *td;
2190satOption_t *option;
2191int value;
2192
2193  v = SATnormalNode(v);
2194
2195  td = SATgetDecision(SATlevel(v));
2196  if(d == td) {
2197    if(!(SATflags(v) & VisitedMask)) {
2198      (*nMarked)++;
2199      SATflags(v) |= VisitedMask;
2200    }
2201  }
2202  else if(td->level < d->level) {
2203    if(!(SATflags(v) & NewMask)) {
2204      option = cm->option;
2205      if((td->level != 0) ||
2206         (td->level == 0 && option->includeLevelZeroLiteral)) {
2207        SATflags(v) |= NewMask;
2208        value = SATvalue(v);
2209        sat_ArrayInsert(clauseArray, v^(!value));
2210        if(*bLevel < td->level)
2211          *bLevel = td->level;
2212      }
2213    }
2214  }
2215  return;
2216}
2217
2218/**Function********************************************************************
2219
2220  Synopsis    [ Traverse the antecedent to find unique implication point]
2221
2222  Description [ Traverse the antecedent to find unique implication point]
2223
2224  SideEffects []
2225
2226  SeeAlso     []
2227
2228******************************************************************************/
2229void
2230sat_MarkNodeInImpliedNodeNoObj(
2231        satManager_t *cm,
2232        satLevel_t *d,
2233        long v,
2234        int *nMarked,
2235        int *oFlag,
2236        int *bLevel,
2237        satArray_t *clauseArray)
2238{
2239long ante, ante2, nv;
2240int inverted, size, i;
2241long *plit;
2242satOption_t *option;
2243
2244  ante= SATante(v);
2245  /* Bing: UNSAT core generation */
2246  if(cm->option->coreGeneration){
2247    if(ante==0){
2248      if(!(st_lookup(cm->anteTable, (char *)(long)SATnormalNode(v), &ante))){
2249        printf("ante = 0 and is not in anteTable %ld\n",v);
2250        exit(0);
2251      }
2252    }
2253  }
2254  inverted = SATisInverted(ante);
2255  ante= SATnormalNode(ante);
2256
2257  option = cm->option;
2258  if(SATflags(ante) & IsCNFMask) {
2259    SATconflictUsage(ante)++;
2260    size = SATnumLits(ante);
2261    for(i=0, plit=(long*)SATfirstLit(ante); i<size; i++, plit++) {
2262      nv = SATgetNode(*plit);
2263      if((int)(SATnormalNode(nv)) == v) continue;
2264      sat_MarkNodeSub(cm, nv, nMarked, bLevel, d, clauseArray);
2265    }
2266  }
2267  else {
2268    /*Bing: very inmportant for level zero conflict analysis*/
2269    if(ante != SATnormalNode(v))
2270      sat_MarkNodeSub(cm, ante, nMarked, bLevel, d, clauseArray);
2271
2272    ante2 = SATante2(v);
2273    if(ante2)
2274      sat_MarkNodeSub(cm, ante2, nMarked, bLevel, d, clauseArray);
2275  }
2276}
2277
2278
2279/**Function********************************************************************
2280
2281  Synopsis    [ Traverse the antecedent to find unique implication point]
2282
2283  Description [ Traverse the antecedent to find unique implication point]
2284
2285  SideEffects []
2286
2287  SeeAlso     []
2288
2289******************************************************************************/
2290void
2291sat_MarkNodeInImpliedNodeObjConservative(
2292        satManager_t *cm,
2293        satLevel_t *d,
2294        long v,
2295        int *nMarked,
2296        int *oFlag,
2297        int *bLevel,
2298        satArray_t *clauseArray)
2299{
2300long ante, ante2, nv;
2301int inverted, size, i;
2302int objectFlag;
2303long *plit;
2304satOption_t *option;
2305
2306  ante= SATante(v);
2307  /* Bing: UNSAT core generation */
2308  if(cm->option->coreGeneration){
2309    if(ante==0){
2310      if(!(st_lookup(cm->anteTable, (char *)SATnormalNode(v), &ante))){
2311        printf("ante = 0 and is not in anteTable %ld\n",v);
2312        exit(0);
2313      }
2314    }
2315  }
2316  inverted = SATisInverted(ante);
2317  ante= SATnormalNode(ante);
2318
2319  objectFlag = 0;
2320  option = cm->option;
2321  if(SATflags(ante) & IsCNFMask) {
2322    SATconflictUsage(ante)++;
2323    size = SATnumLits(ante);
2324    for(i=0, plit=(long*)SATfirstLit(ante); i<size; i++, plit++) {
2325      nv = SATgetNode(*plit);
2326      nv = SATnormalNode(nv);
2327      if(nv == v)       continue;
2328      sat_MarkNodeSub(cm, nv, nMarked, bLevel, d, clauseArray);
2329    }
2330    objectFlag |= SATflags(ante) & ObjMask;
2331  }
2332  else {
2333    /*Bing: very inmportant for level zero conflict analysis*/
2334    if(ante != SATnormalNode(v))
2335      sat_MarkNodeSub(cm, ante, nMarked, bLevel, d, clauseArray);
2336
2337    ante2 = SATante2(v);
2338    if(ante2) {
2339      ante2 = SATnormalNode(ante2);
2340      sat_MarkNodeSub(cm, ante2, nMarked, bLevel, d, clauseArray);
2341    }
2342  }
2343  *oFlag |= objectFlag;
2344}
2345
2346
2347/**Function********************************************************************
2348
2349  Synopsis    [ Find seed for unique implication point analysis
2350                from conflicting clause]
2351
2352  Description [ Find seed for unique implication point analysis
2353                from conflicting clause]
2354
2355  SideEffects []
2356
2357  SeeAlso     []
2358
2359******************************************************************************/
2360void
2361sat_MarkNodeInConflictClauseNoObj(
2362        satManager_t *cm,
2363        satLevel_t *d,
2364        int *nMarked,
2365        int *oFlag,
2366        int *bLevel,
2367        satArray_t *clauseArray)
2368{
2369long conflict, left, right, nv;
2370int inverted, size, value, i;
2371long *plit;
2372satOption_t *option;
2373
2374  conflict = d->conflict;
2375  inverted = SATisInverted(conflict);
2376  conflict = SATnormalNode(conflict);
2377
2378  option = cm->option;
2379  if(SATflags(conflict) & IsCNFMask) {
2380    size = SATnumLits(conflict);
2381    for(i=0, plit=(long*)SATfirstLit(conflict); i<size; i++, plit++) {
2382      nv = SATgetNode(*plit);
2383      sat_MarkNodeSub(cm, nv, nMarked, bLevel, d, clauseArray);
2384    }
2385  }
2386  else {
2387    value = SATvalue(conflict);
2388    if(value == 1) {
2389      sat_MarkNodeSub(cm, conflict, nMarked, bLevel, d, clauseArray);
2390
2391      left = SATleftChild(conflict);
2392      inverted = SATisInverted(left);
2393      left = SATnormalNode(left);
2394      value = SATvalue(left) ^ inverted;
2395      if(value == 0) {
2396        sat_MarkNodeSub(cm, left, nMarked, bLevel, d, clauseArray);
2397        return;
2398      }
2399
2400      right = SATrightChild(conflict);
2401      inverted = SATisInverted(right);
2402      right = SATnormalNode(right);
2403      value = SATvalue(right) ^ inverted;
2404      if(value == 0) {
2405        sat_MarkNodeSub(cm, right, nMarked, bLevel, d, clauseArray);
2406        return;
2407      }
2408    }
2409    else if(value == 0) {
2410      left = SATleftChild(conflict);
2411      right = SATrightChild(conflict);
2412      sat_MarkNodeSub(cm, conflict, nMarked, bLevel, d, clauseArray);
2413      sat_MarkNodeSub(cm, left, nMarked, bLevel, d, clauseArray);
2414      sat_MarkNodeSub(cm, right, nMarked, bLevel, d, clauseArray);
2415    }
2416  }
2417}
2418
2419/**Function********************************************************************
2420
2421  Synopsis    [ Find seed for unique implication point analysis
2422                from conflicting clause]
2423
2424  Description [ Find seed for unique implication point analysis
2425                from conflicting clause]
2426
2427  SideEffects []
2428
2429  SeeAlso     []
2430
2431******************************************************************************/
2432void
2433sat_MarkNodeInConflictClauseObjConservative(
2434        satManager_t *cm,
2435        satLevel_t *d,
2436        int *nMarked,
2437        int *oFlag,
2438        int *bLevel,
2439        satArray_t *clauseArray)
2440{
2441long conflict, left, right, nv;
2442int inverted, size, value, i;
2443long *plit;
2444satOption_t *option;
2445
2446  conflict = d->conflict;
2447  inverted = SATisInverted(conflict);
2448  conflict = SATnormalNode(conflict);
2449
2450  option = cm->option;
2451  if(SATflags(conflict) & IsCNFMask) {
2452    size = SATnumLits(conflict);
2453    for(i=0, plit=(long*)SATfirstLit(conflict); i<size; i++, plit++) {
2454      nv = SATgetNode(*plit);
2455      *oFlag |= (SATflags(nv) & ObjMask);
2456      sat_MarkNodeSub(cm, nv, nMarked, bLevel, d, clauseArray);
2457    }
2458  }
2459  else {
2460    value = SATvalue(conflict);
2461    if(value == 1) {
2462      *oFlag |= (SATflags(conflict) & ObjMask);
2463      sat_MarkNodeSub(cm, conflict, nMarked, bLevel, d, clauseArray);
2464
2465      left = SATleftChild(conflict);
2466      inverted = SATisInverted(left);
2467      left = SATnormalNode(left);
2468      value = SATvalue(left) ^ inverted;
2469      if(value == 0) {
2470        *oFlag |= (SATflags(left) & ObjMask);
2471        sat_MarkNodeSub(cm, left, nMarked, bLevel, d, clauseArray);
2472        return;
2473      }
2474
2475      right = SATrightChild(conflict);
2476      inverted = SATisInverted(right);
2477      right = SATnormalNode(right);
2478      value = SATvalue(right) ^ inverted;
2479      if(value == 0) {
2480        *oFlag |= (SATflags(right) & ObjMask);
2481        sat_MarkNodeSub(cm, right, nMarked, bLevel, d, clauseArray);
2482        return;
2483      }
2484    }
2485    else if(value == 0) {
2486      *oFlag |= (SATflags(conflict) & ObjMask);
2487
2488      left = SATleftChild(conflict);
2489      inverted = SATisInverted(left);
2490      left = SATnormalNode(left);
2491      *oFlag |= (SATflags(left) & ObjMask);
2492
2493      right = SATrightChild(conflict);
2494      inverted = SATisInverted(right);
2495      right = SATnormalNode(right);
2496      *oFlag |= (SATflags(right) & ObjMask);
2497
2498      sat_MarkNodeSub(cm, conflict, nMarked, bLevel, d, clauseArray);
2499      sat_MarkNodeSub(cm, left, nMarked, bLevel, d, clauseArray);
2500      sat_MarkNodeSub(cm, right, nMarked, bLevel, d, clauseArray);
2501    }
2502  }
2503}
2504
2505
2506/**Function********************************************************************
2507
2508  Synopsis    [ Backtrack to given decision level ]
2509
2510  Description [ Backtrack to given decision level ]
2511
2512  SideEffects []
2513
2514  SeeAlso     []
2515
2516******************************************************************************/
2517void
2518sat_Backtrack(
2519        satManager_t *cm,
2520        int level)
2521{
2522satLevel_t *d;
2523
2524/*Bing*/
2525 if(cm->option->ForceFinish == 0)
2526   if(level < 0)        return;
2527
2528  d = SATgetDecision(cm->currentDecision);
2529  while(1) {
2530    if(d->level <= level)
2531      break;
2532
2533    sat_Undo(cm, d);
2534    cm->currentDecision--;
2535    if(cm->currentDecision == -1)
2536      break;
2537    d = SATgetDecision(cm->currentDecision);
2538  }
2539  return;
2540}
2541
2542
2543/**Function********************************************************************
2544
2545  Synopsis    [ Undo implication]
2546
2547  Description [ Undo implication]
2548
2549  SideEffects []
2550
2551  SeeAlso     []
2552
2553******************************************************************************/
2554void
2555sat_Undo(
2556        satManager_t *cm,
2557        satLevel_t *d)
2558{
2559satArray_t *implied, *satisfied;
2560satVariable_t *var;
2561int size, i;
2562long *space, v;
2563
2564  implied = d->implied;
2565  space = implied->space;
2566  size = implied->num;
2567  for(i=0; i<size; i++, space++) {
2568    v = *space;
2569
2570    SATvalue(v) = 2;
2571    SATflags(v) &= ResetNewVisitedObjInQueueMask;
2572    var = &(cm->variableArray[SATnodeID(v)]);
2573    var->antecedent = 0;
2574    var->antecedent2 = 0;
2575    var->level = -1;
2576    var->depth = 0;
2577  }
2578
2579  cm->implicatedSoFar -= size;
2580
2581  if(d->satisfied) {
2582    satisfied = d->implied;
2583    space = satisfied->space;
2584    size = satisfied->num;
2585    for(i=0; i<size; i++, space++) {
2586      v = *space;
2587
2588      SATflags(v) &= ResetBDDSatisfiedMask;
2589    }
2590    d->satisfied->num = 0;
2591  }
2592  if(d->level > 0) {
2593    if((cm->decisionHead[d->level-1]).currentVarPos < cm->currentVarPos)
2594      cm->currentVarPos = (cm->decisionHead[d->level-1]).currentVarPos;
2595  }
2596  else
2597    cm->currentVarPos = d->currentVarPos;
2598
2599  d->implied->num = 0;
2600  d->currentVarPos = 0;
2601  d->conflict = 0;
2602
2603
2604}
2605
2606/**Function********************************************************************
2607
2608  Synopsis    [ Compare decision level of variable ]
2609
2610  Description [ Compare decision level of variable ]
2611
2612  SideEffects []
2613
2614  SeeAlso     []
2615
2616******************************************************************************/
2617
2618static int
2619levelCompare(
2620  const void * node1,
2621  const void * node2)
2622{
2623  long v1, v2;
2624  int l1, l2;
2625
2626  v1 = *(int *)(node1);
2627  v2 = *(int *)(node2);
2628  l1 = SATcm->variableArray[SATnodeID(v1)].level;
2629  l2 = SATcm->variableArray[SATnodeID(v2)].level;
2630
2631  if(l1 == l2)  return(v1 > v2);
2632  return (l1 > l2);
2633}
Note: See TracBrowser for help on using the repository browser.