source: vis_dev/vis-2.3/src/sat/satMain.c

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

vis2.3

File size: 22.2 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [satMain.c]
4
5  PackageName [sat]
6
7  Synopsis    [Routines for sat main 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: satMain.c,v 1.30 2009/04/11 18:26:37 fabio Exp $";
22
23/*---------------------------------------------------------------------------*/
24/* Constant declarations                                                     */
25/*---------------------------------------------------------------------------*/
26
27/**AutomaticStart*************************************************************/
28
29/*---------------------------------------------------------------------------*/
30/* Static function prototypes                                                */
31/*---------------------------------------------------------------------------*/
32
33
34/**AutomaticEnd***************************************************************/
35
36
37/*---------------------------------------------------------------------------*/
38/* Definition of exported functions                                          */
39/*---------------------------------------------------------------------------*/
40
41
42/**Function********************************************************************
43
44  Synopsis    [ Pre-processing to run CirCUs ]
45
46  Description [ Pre-processing to run CirCUs ]
47
48  SideEffects [ One has to run sat_PostProcessing after running CirCUs]
49
50  SeeAlso     [ sat_PostProcessing ]
51
52******************************************************************************/
53void
54sat_PreProcessing(satManager_t *cm)
55{
56satLevel_t *d;
57
58
59  /** create implication queue **/
60  cm->queue = sat_CreateQueue(1024);
61  cm->BDDQueue = sat_CreateQueue(1024);
62  cm->unusedAigQueue = sat_CreateQueue(1024);
63
64  /**
65  create variable array : one can reduce size of variable array using
66  mapping. for fanout free internal node....
67  **/
68
69  if(cm->variableArray == 0) {
70    cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
71    memset(cm->variableArray, 0,
72            sizeof(satVariable_t) * (cm->initNumVariables+1));
73  }
74
75  cm->auxArray = sat_ArrayAlloc(1024);
76  cm->nonobjUnitLitArray = sat_ArrayAlloc(128);
77  cm->objUnitLitArray = sat_ArrayAlloc(128);
78
79  /** compact fanout of AIG node **/
80  //sat_CompactFanout(cm);
81
82  //Bing:
83  if(cm->option->AbRf == 0)
84    sat_CompactFanout(cm);
85
86  /** Initial score **/
87  sat_InitScore(cm);
88
89  /** create decision stack **/
90  if(cm->decisionHeadSize == 0) {
91    cm->decisionHeadSize = 32;
92    cm->decisionHead = ALLOC(satLevel_t, cm->decisionHeadSize);
93    memset(cm->decisionHead, 0, sizeof(satLevel_t) * cm->decisionHeadSize);
94  }
95  cm->currentDecision = -1;
96
97  /** to avoid purify warning **/
98  SATvalue(2) = 2;
99  SATflags(0) = 0;
100
101  cm->initNodesArraySize = cm->nodesArraySize;
102  cm->beginConflict = cm->nodesArraySize;
103
104  /** incremental SAT.... **/
105  if(cm->option->incTraceObjective) {
106    sat_RestoreForwardedClauses(cm, 0);
107  }
108  else if(cm->option->incAll) {
109    sat_RestoreForwardedClauses(cm, 1);
110  }
111
112  if(cm->option->incTraceObjective) {
113    sat_MarkObjectiveFlagToArray(cm, cm->obj);
114    sat_MarkObjectiveFlagToArray(cm, cm->objCNF);
115  }
116
117
118  /** Level 0 decision.... **/
119  d = sat_AllocLevel(cm);
120
121  sat_ApplyForcedAssignmentMain(cm, d);
122
123  if(cm->status == SAT_UNSAT)
124    return;
125
126
127  //Bing:
128  if(cm->option->coreGeneration && cm->option->IP){
129    cm->rm = ALLOC(RTManager_t, 1);
130    memset(cm->rm,0,sizeof(RTManager_t));
131  }
132  //Bing
133  if(!(cm->option->SSS==1 && cm->option->coreGeneration==1))
134    sat_ImplyArray(cm, d, cm->pureLits);
135
136  sat_ImplyArray(cm,d,cm->assertArray);
137  sat_ImplyArray(cm, d, cm->assertion);
138  sat_ImplyArray(cm, d, cm->unitLits);
139  sat_ImplyArray(cm, d, cm->auxObj);
140  sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
141  sat_ImplyArray(cm, d, cm->obj);
142
143  sat_ImplicationMain(cm, d);
144  if(d->conflict) {
145    cm->status = SAT_UNSAT;
146  }
147
148  if(cm->status == 0) {
149    if(cm->option->incDistill) {
150      sat_IncrementalUsingDistill(cm);
151    }
152  }
153
154}
155
156/**Function********************************************************************
157
158  Synopsis    [ Pre-processing to run CirCUs with AIG and CNF]
159
160  Description [ Pre-processing to run CirCUs with AIG and CNF]
161
162  SideEffects [ One has to run sat_PostProcessing for AllSat enumeration after running CirCUs]
163
164  SeeAlso     [ sat_PostProcessing ]
165
166******************************************************************************/
167void
168sat_PreProcessingForMixed(satManager_t *cm)
169{
170satLevel_t *d;
171
172
173  /** create implication queue **/
174  cm->queue = sat_CreateQueue(1024);
175  cm->BDDQueue = sat_CreateQueue(1024);
176  cm->unusedAigQueue = sat_CreateQueue(1024);
177
178  /**
179  create variable array : one can reduce size of variable array using
180  mapping. for fanout free internal node....
181  **/
182
183  if(cm->variableArray == 0) {
184    cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
185    memset(cm->variableArray, 0,
186            sizeof(satVariable_t) * (cm->initNumVariables+1));
187  }
188
189  cm->auxArray = sat_ArrayAlloc(1024);
190  cm->nonobjUnitLitArray = sat_ArrayAlloc(128);
191  cm->objUnitLitArray = sat_ArrayAlloc(128);
192
193  /** compact fanout of AIG node **/
194  sat_CompactFanout(cm);
195
196  cm->initNodesArraySize = cm->nodesArraySize;
197  cm->beginConflict = cm->nodesArraySize;
198
199  if(cm->option->allSatMode) {
200    sat_RestoreFrontierClauses(cm);
201    sat_RestoreBlockingClauses(cm);
202  }
203
204  /** Initial score **/
205  sat_InitScoreForMixed(cm);
206
207  /** create decision stack **/
208  if(cm->decisionHeadSize == 0) {
209    cm->decisionHeadSize = 32;
210    cm->decisionHead = ALLOC(satLevel_t, cm->decisionHeadSize);
211    memset(cm->decisionHead, 0, sizeof(satLevel_t) * cm->decisionHeadSize);
212  }
213  cm->currentDecision = -1;
214
215  /** to avoid purify warning **/
216  SATvalue(2) = 2;
217  SATflags(0) = 0;
218
219  /** incremental SAT.... **/
220  if(cm->option->incTraceObjective) {
221    sat_RestoreForwardedClauses(cm, 0);
222  }
223  else if(cm->option->incAll) {
224    sat_RestoreForwardedClauses(cm, 1);
225  }
226
227  if(cm->option->incTraceObjective) {
228    sat_MarkObjectiveFlagToArray(cm, cm->obj);
229    sat_MarkObjectiveFlagToArray(cm, cm->objCNF);
230  }
231
232  /** Level 0 decision.... **/
233  d = sat_AllocLevel(cm);
234
235  sat_ApplyForcedAssignmentMain(cm, d);
236
237  if(cm->status == SAT_UNSAT)
238    return;
239
240  sat_ImplyArray(cm, d, cm->assertion);
241  sat_ImplyArray(cm, d, cm->unitLits);
242  sat_ImplyArray(cm, d, cm->pureLits);
243  sat_ImplyArray(cm, d, cm->auxObj);
244  sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
245  sat_ImplyArray(cm, d, cm->obj);
246
247  sat_ImplicationMain(cm, d);
248  if(d->conflict) {
249    cm->status = SAT_UNSAT;
250  }
251
252  if(cm->status == 0) {
253    if(cm->option->incDistill) {
254      sat_IncrementalUsingDistill(cm);
255    }
256  }
257
258}
259
260/**Function********************************************************************
261
262  Synopsis    [ Pre-processing to run CirCUs with AIG and CNF]
263
264  Description [ Pre-processing to run CirCUs with AIG and CNF]
265
266  SideEffects [ One has to run sat_PostProcessing for AllSat enumeration after running CirCUs]
267
268  SeeAlso     [ sat_PostProcessing ]
269
270******************************************************************************/
271void
272sat_PreProcessingForMixedNoCompact(satManager_t *cm)
273{
274satLevel_t *d;
275
276
277  /** create implication queue **/
278  cm->queue = sat_CreateQueue(1024);
279  cm->BDDQueue = sat_CreateQueue(1024);
280  cm->unusedAigQueue = sat_CreateQueue(1024);
281
282  /**
283  create variable array : one can reduce size of variable array using
284  mapping. for fanout free internal node....
285  **/
286
287  if(cm->variableArray == 0) {
288    cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
289    memset(cm->variableArray, 0,
290            sizeof(satVariable_t) * (cm->initNumVariables+1));
291  }
292
293  if(cm->auxArray == 0)
294    cm->auxArray = sat_ArrayAlloc(1024);
295  if(cm->nonobjUnitLitArray == 0)
296    cm->nonobjUnitLitArray = sat_ArrayAlloc(128);
297  if(cm->objUnitLitArray == 0)
298    cm->objUnitLitArray = sat_ArrayAlloc(128);
299
300  /** compact fanout of AIG node
301  sat_CompactFanout(cm);
302  **/
303
304  cm->initNodesArraySize = cm->nodesArraySize;
305  cm->beginConflict = cm->nodesArraySize;
306
307  if(cm->option->allSatMode) {
308    sat_RestoreFrontierClauses(cm);
309    sat_RestoreBlockingClauses(cm);
310  }
311
312  /** Initial score **/
313  sat_InitScoreForMixed(cm);
314
315  /** create decision stack **/
316  if(cm->decisionHeadSize == 0) {
317    cm->decisionHeadSize = 32;
318    cm->decisionHead = ALLOC(satLevel_t, cm->decisionHeadSize);
319    memset(cm->decisionHead, 0, sizeof(satLevel_t) * cm->decisionHeadSize);
320  }
321  cm->currentDecision = -1;
322
323  /** to avoid purify warning **/
324  SATvalue(2) = 2;
325  SATflags(0) = 0;
326
327  /** incremental SAT.... **/
328  if(cm->option->incTraceObjective) {
329    sat_RestoreForwardedClauses(cm, 0);
330  }
331  else if(cm->option->incAll) {
332    sat_RestoreForwardedClauses(cm, 1);
333  }
334
335  if(cm->option->incTraceObjective) {
336    sat_MarkObjectiveFlagToArray(cm, cm->obj);
337    sat_MarkObjectiveFlagToArray(cm, cm->objCNF);
338  }
339
340  /** Level 0 decision.... **/
341  d = sat_AllocLevel(cm);
342
343  sat_ApplyForcedAssignmentMain(cm, d);
344
345  if(cm->status == SAT_UNSAT)
346    return;
347
348  sat_ImplyArray(cm, d, cm->assertion);
349  sat_ImplyArray(cm, d, cm->unitLits);
350  sat_ImplyArray(cm, d, cm->pureLits);
351  sat_ImplyArray(cm, d, cm->auxObj);
352  sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
353  sat_ImplyArray(cm, d, cm->obj);
354
355  sat_ImplicationMain(cm, d);
356  if(d->conflict) {
357    cm->status = SAT_UNSAT;
358  }
359
360  if(cm->status == 0) {
361    if(cm->option->incDistill) {
362      sat_IncrementalUsingDistill(cm);
363    }
364  }
365
366}
367
368/**Function********************************************************************
369
370  Synopsis    [ Mark objective flag to given AIG node or CNF clauses]
371
372  Description [ To use incremental SAT algorithm based on trace objective,
373                the objective has to be identified before starting the
374                SAT process.]
375
376  SideEffects [ One has to run sat_PostProcessing after running CirCUs]
377
378  SeeAlso     [ sat_PostProcessing ]
379
380******************************************************************************/
381void
382sat_MarkObjectiveFlagToArray(
383        satManager_t *cm,
384        satArray_t *objArr)
385{
386int i;
387long v;
388
389  if(objArr == 0)       return;
390
391  for(i=0; i<objArr->num; i++) {
392    v = objArr->space[i];
393    v = SATnormalNode(v);
394    SATflags(v) |= ObjMask;
395  }
396}
397
398/**Function********************************************************************
399
400  Synopsis    [ Post-processing after running CirCUs]
401
402  Description [ Post-processing after running CirCUs]
403
404  SideEffects [ ]
405
406  SeeAlso     [ sat_PreProcessing ]
407
408******************************************************************************/
409void
410sat_PostProcessing(satManager_t *cm)
411{
412
413  sat_Verify(cm);
414
415  if(cm->option->incTraceObjective) {
416    sat_SaveNonobjClauses(cm);
417  }
418
419  if(cm->option->incAll) {
420    sat_SaveAllClauses(cm);
421  }
422
423  if(cm->option->allSatMode) {
424    sat_CollectBlockingClause(cm);
425  }
426
427  //Bing:
428  //sat_RestoreFanout(cm);
429  if(cm->option->AbRf == 0)
430    sat_RestoreFanout(cm);
431
432  if(cm->mgr) {
433#ifdef BDDcu
434    Cudd_Quit(cm->mgr);
435#endif
436    cm->mgr = 0;
437  }
438
439}
440
441/**Function********************************************************************
442
443  Synopsis    [ main function for SAT solving]
444
445  Description [ main function for SAT solving]
446
447  SideEffects [ ]
448
449  SeeAlso     [ ]
450
451******************************************************************************/
452void
453sat_Main(satManager_t *cm)
454{
455long btime, etime;
456
457  btime = util_cpu_time();
458  sat_PreProcessing(cm);
459
460  if(cm->status == 0)
461    sat_Solve(cm);
462
463  /** Bing: UNSAT core generation **/
464  if(cm->option->coreGeneration && cm->status == SAT_UNSAT){
465    //Bing
466    if(cm->option->RT)
467      sat_GenerateCore_All(cm);
468    else
469      sat_GenerateCore(cm);
470  }
471
472  sat_PostProcessing(cm);
473
474  etime = util_cpu_time();
475  cm->each->satTime = (double)(etime - btime) / 1000.0 ;
476
477}
478
479/**Function********************************************************************
480
481  Synopsis    [ DPLL procedure for SAT solving]
482
483  Description [ DPLL procedure for SAT solving]
484
485  SideEffects [ ]
486
487  SeeAlso     [ sat_Main ]
488
489******************************************************************************/
490
491void
492sat_Solve(satManager_t *cm)
493{
494satLevel_t *d;
495satOption_t *option;
496satVariable_t *var;
497int level;
498
499  d = SATgetDecision(0);
500  cm->implicatedSoFar = d->implied->num;
501  cm->currentTopConflict = 0;
502
503  option = cm->option;
504  if(option->BDDMonolithic) {
505    sat_TryToBuildMonolithicBDD(cm);
506  }
507
508  if(cm->status == SAT_UNSAT) {
509    sat_Undo(cm, SATgetDecision(0));
510    return;
511  }
512
513  while(1) {
514    sat_PeriodicFunctions(cm);
515
516    if(cm->currentDecision == 0)
517      sat_BuildLevelZeroHyperImplicationGraph(cm);
518
519    d = sat_MakeDecision(cm);
520
521    if(d == 0)  {
522      cm->status = SAT_SAT;
523      return;
524    }
525
526    while(1) {
527      sat_ImplicationMain(cm, d);
528
529      if(d->conflict == 0)      {
530        if(cm->option->verbose > 2) {
531          var = SATgetVariable(d->decisionNode);
532          fprintf(cm->stdOut, "decision at %3d on %6ld <- %ld score(%d %d) %d %ld implied %.3f %%\n",
533            d->level, d->decisionNode, SATvalue(d->decisionNode),
534            var->scores[0], var->scores[1],
535            cm->each->nDecisions, d->implied->num,
536            (double)cm->implicatedSoFar/(double)cm->initNumVariables * 100);
537          fflush(cm->stdOut);
538        }
539
540        break;
541      }
542
543        if(cm->option->verbose > 2) {
544          var = SATgetVariable(d->decisionNode);
545          fprintf(cm->stdOut, "decision at %3d on %6ld <- %ld score(%d %d) %d %ld implied  %.3f %% Conflict\n",
546            d->level, d->decisionNode, SATvalue(d->decisionNode),
547            var->scores[0], var->scores[1],
548            cm->each->nDecisions, d->implied->num,
549            (double)cm->implicatedSoFar/(double)cm->initNumVariables * 100);
550          fflush(cm->stdOut);
551        }
552
553      if(cm->option->useStrongConflictAnalysis)
554        level = sat_StrongConflictAnalysis(cm, d);
555      else
556        level = sat_ConflictAnalysis(cm, d);
557
558      if(cm->currentDecision == -1) {
559        if(cm->option->incDistill) {
560          sat_BuildTrieForDistill(cm);
561        }
562        sat_Undo(cm, SATgetDecision(0));
563        cm->status = SAT_UNSAT;
564        return;
565      }
566
567      d = SATgetDecision(cm->currentDecision);
568    }
569
570  }
571}
572
573/**Function********************************************************************
574
575  Synopsis    [ Periodic functions for SAT solving]
576
577  Description [ Periodically, score aging and conflict clause deletion
578                are invoked ]
579
580  SideEffects [ ]
581
582  SeeAlso     [ sat_Solve ]
583
584******************************************************************************/
585void
586sat_PeriodicFunctions(satManager_t *cm)
587{
588satStatistics_t *stats;
589satOption_t *option;
590int nDecisions;
591int gap;
592
593  /** need to review restart mechanism **/
594  stats = cm->each;
595  option = cm->option;
596  nDecisions = stats->nDecisions-stats->nShrinkDecisions;
597  if(nDecisions && !(nDecisions % option->decisionAgeInterval)) {
598    if(option->decisionAgeRestart) {
599      gap = stats->nConflictCl-stats->nOldConflictCl;
600      if(gap > option->decisionAgeInterval>>2)  {
601        sat_UpdateScore(cm);
602        sat_Backtrack(cm, cm->lowestBacktrackLevel);
603        cm->currentTopConflict = cm->literals->last-1;
604        cm->currentTopConflictCount = 0;
605        cm->lowestBacktrackLevel = MAXINT;
606      }
607      stats->nOldConflictCl = stats->nConflictCl;
608    }
609    else {
610      sat_UpdateScore(cm);
611    }
612
613  }
614
615  if(option->clauseDeletionHeuristic & LATEST_ACTIVITY_DELETION &&
616          stats->nBacktracks > option->nextClauseDeletion &&
617     cm->implicatedSoFar > cm->initNumVariables/3) {
618    option->nextClauseDeletion += option->clauseDeletionInterval;
619    sat_ClauseDeletionLatestActivity(cm);
620  }
621  else if(option->clauseDeletionHeuristic & MAX_UNRELEVANCE_DELETION &&
622          stats->nBacktracks > option->nextClauseDeletion) {
623    option->nextClauseDeletion += option->clauseDeletionInterval;
624    sat_ClauseDeletion(cm);
625  }
626
627}
628
629/**Function********************************************************************
630
631  Synopsis    [ Interface function for pure CNF based SAT solver]
632
633  Description [ Interface function for pure CNF based SAT solver ]
634
635  SideEffects [ ]
636
637  SeeAlso     [ sat_Main ]
638
639******************************************************************************/
640void
641sat_CNFMain(satOption_t *option, char *filename)
642{
643satManager_t *cm;
644int maxSize;
645
646  cm = sat_InitManager(0);
647  cm->comment = ALLOC(char, 2);
648  cm->comment[0] = ' ';
649  cm->comment[1] = '\0';
650  if(option->outFilename) {
651    if(!(cm->stdOut = fopen(option->outFilename, "w"))) {
652      fprintf(stdout, "ERROR : Can't open file %s\n", option->outFilename);
653      cm->stdOut = stdout;
654      cm->stdErr = stderr;
655    }
656    else {
657      cm->stdErr = cm->stdOut;
658    }
659  }
660  else {
661    cm->stdOut = stdout;
662    cm->stdErr = stderr;
663  }
664
665  cm->option = option;
666  cm->each = sat_InitStatistics();
667
668  cm->unitLits = sat_ArrayAlloc(16);
669  cm->pureLits = sat_ArrayAlloc(16);
670
671  maxSize = 1024 << 8;
672  cm->nodesArray = ALLOC(long, maxSize);
673  cm->maxNodesArraySize = maxSize;
674  cm->nodesArraySize = satNodeSize;
675
676  sat_AllocLiteralsDB(cm);
677
678  if(!sat_ReadCNF(cm, filename)) {
679    sat_FreeManager(cm);
680    return;
681  }
682
683  /** trigerring strong conflict analysis **/
684  if(cm->option->coreGeneration==0)
685    cm->option->useStrongConflictAnalysis = 1;
686
687  sat_Main(cm);
688
689  //Bing:change
690  //unsat core
691  if(cm->option->coreGeneration)
692    fclose(cm->fp);
693
694  if(cm->status == SAT_UNSAT) {
695    if(cm->option->forcedAssignArr)
696      fprintf(cm->stdOut, "%s UNSAT under given assignment\n",
697              cm->comment);
698    fprintf(cm->stdOut, "%s UNSATISFIABLE\n", cm->comment);
699    fflush(cm->stdOut);
700    sat_ReportStatistics(cm, cm->each);
701    sat_FreeManager(cm);
702  }
703  else if(cm->status == SAT_SAT) {
704    fprintf(cm->stdOut, "%s SATISFIABLE\n", cm->comment);
705    fflush(cm->stdOut);
706    sat_PrintSatisfyingAssignment(cm);
707    sat_ReportStatistics(cm, cm->each);
708    sat_FreeManager(cm);
709  }
710  if(cm->stdOut != stdout)
711    fclose(cm->stdOut);
712  if(cm->stdErr != stderr && cm->stdErr != cm->stdOut)
713    fclose(cm->stdErr);
714}
715
716/**Function********************************************************************
717
718  Synopsis    [ Interface function for pure CNF based SAT solver from array of CNF]
719
720  Description [ Interface function for pure CNF based SAT solver  from array of CNF]
721
722  SideEffects [ ]
723
724  SeeAlso     [ sat_Main ]
725
726******************************************************************************/
727int
728sat_CNFMainWithArray(
729        satOption_t *option,
730        satArray_t *cnfArray,
731        int unsatCoreFlag,
732        satArray_t *coreArray,
733        st_table *mappedTable)
734{
735satManager_t *cm;
736int maxSize;
737int flag;
738int i;
739long v;
740
741  cm = sat_InitManager(0);
742  cm->comment = ALLOC(char, 2);
743  cm->comment[0] = ' ';
744  cm->comment[1] = '\0';
745  if(option->outFilename) {
746    if(!(cm->stdOut = fopen(option->outFilename, "w"))) {
747      fprintf(stdout, "ERROR : Can't open file %s\n", option->outFilename);
748      cm->stdOut = stdout;
749      cm->stdErr = stderr;
750    }
751    else {
752      cm->stdErr = cm->stdOut;
753    }
754  }
755  else {
756    cm->stdOut = stdout;
757    cm->stdErr = stderr;
758  }
759
760  cm->option = option;
761  cm->each = sat_InitStatistics();
762
763  cm->unitLits = sat_ArrayAlloc(16);
764  cm->pureLits = sat_ArrayAlloc(16);
765
766  maxSize = 1024 << 8;
767  cm->nodesArray = ALLOC(long, maxSize);
768  cm->maxNodesArraySize = maxSize;
769  cm->nodesArraySize = satNodeSize;
770
771  sat_AllocLiteralsDB(cm);
772
773  if(unsatCoreFlag) {
774    cm->option->useStrongConflictAnalysis = 0;
775    cm->option->coreGeneration = 1;
776    cm->dependenceTable = st_init_table(st_ptrcmp, st_ptrhash);
777    cm->anteTable = st_init_table(st_numcmp, st_numhash);
778  }
779
780  if(!sat_ReadCNFFromArray(cm, cnfArray, mappedTable)) {
781    sat_FreeManager(cm);
782    return(SAT_UNSAT);
783  }
784
785  sat_Main(cm);
786
787  if(cm->status == SAT_UNSAT) {
788    if(cm->option->forcedAssignArr)
789      fprintf(cm->stdOut, "%s UNSAT under given assignment\n",
790              cm->comment);
791    fprintf(cm->stdOut, "%s UNSATISFIABLE\n", cm->comment);
792    fflush(cm->stdOut);
793    sat_ReportStatistics(cm, cm->each);
794    flag = SAT_UNSAT;
795
796    if(unsatCoreFlag) {
797      for(i=0; i<cm->clauseIndexInCore->num; i++) {
798        v = cm->clauseIndexInCore->space[i];
799        sat_ArrayInsert(coreArray, v);
800      }
801    }
802  }
803  else if(cm->status == SAT_SAT) {
804    fprintf(cm->stdOut, "%s SATISFIABLE\n", cm->comment);
805    fflush(cm->stdOut);
806    sat_PrintSatisfyingAssignment(cm);
807    sat_ReportStatistics(cm, cm->each);
808    flag = SAT_SAT;
809  }
810  if(cm->stdOut != stdout)
811    fclose(cm->stdOut);
812  if(cm->stdErr != stderr && cm->stdErr != cm->stdOut)
813    fclose(cm->stdErr);
814
815  sat_FreeManager(cm);
816
817  return(flag);
818}
819
820/**Function********************************************************************
821
822  Synopsis    [ Print satisfying assignment]
823
824  Description [ Print satisfying assignment ]
825
826  SideEffects [ ]
827
828  SeeAlso     [ sat_CNFMain ]
829
830******************************************************************************/
831int
832sat_PrintSatisfyingAssignment(satManager_t *cm)
833{
834int i, size, index, value;
835
836  index = 0;
837  size = cm->initNumVariables * satNodeSize;
838  for(i=satNodeSize; i<=size; i+=satNodeSize) {
839    if(!(SATflags(i) & CoiMask))        continue;
840    index ++;
841    value = SATvalue(i);
842    if(value == 1) {
843      fprintf(cm->stdOut, "%ld ", SATnodeID(i));
844    }
845    else if(value == 0) {
846      fprintf(cm->stdOut, "%ld ", -(SATnodeID(i)));
847    }
848    else {
849      fprintf(cm->stdOut, "\n%s ERROR : unassigned variable %d\n", cm->comment, i);
850      fflush(cm->stdOut);
851      return(0);
852    }
853
854    if(((index % 10) == 0) && (i+satNodeSize <= size))
855      fprintf(cm->stdOut, "\n ");
856  }
857  fprintf(cm->stdOut, "\n");
858  return(1);
859}
860
861/**Function********************************************************************
862
863  Synopsis    [ Verify satisfying assignment]
864
865  Description [ Verify satisfying assignment when the instance is satisfiable]
866
867  SideEffects [ ]
868
869  SeeAlso     [ sat_Main ]
870
871******************************************************************************/
872void
873sat_Verify(satManager_t *cm)
874{
875int value, size, i;
876int v, flag;
877satArray_t *arr;
878satLevel_t *d;
879
880  if(cm->status != SAT_SAT)     return;
881
882  size = cm->initNumVariables * satNodeSize;
883  arr = sat_ArrayAlloc(cm->initNumVariables);
884  for(i=satNodeSize; i<=size; i+=satNodeSize) {
885    if(!(SATflags(i) & CoiMask))
886      continue;
887    value = SATvalue(i);
888    if(value > 1) {
889      fprintf(cm->stdOut, "%s ERROR : unassigned variable %d\n", cm->comment, i);
890      fflush(cm->stdOut);
891    }
892    else {
893      v = value ? i : SATnot(i);
894      sat_ArrayInsert(arr, v);
895    }
896  }
897
898  sat_Backtrack(cm, -1);
899
900  d = sat_AllocLevel(cm);
901  flag = sat_ApplyForcedAssigment(cm, arr, d);
902  sat_ArrayFree(arr);
903  if(flag == 1) {
904    fprintf(cm->stdOut,
905           "%s ERROR : Wrong satisfying assignment\n", cm->comment);
906    fflush(cm->stdOut);
907    exit(0);
908  }
909}
Note: See TracBrowser for help on using the repository browser.