source: vis_dev/cusp-1.1/src/sat/distill.c @ 106

Last change on this file since 106 was 12, checked in by cecile, 13 years ago

cusp added

File size: 66.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [sat_NewDistill.c]
4
5  PackageName [sat]
6
7  Synopsis    [ Routines for Distillation-based preprocessing ]
8
9  Author      [Hyojung Han]
10
11  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
12
13  All rights reserved.
14
15  Redistribution and use in source and binary forms, with or without
16  modification, are permitted provided that the following conditions
17  are met:
18
19  Redistributions of source code must retain the above copyright
20  notice, this list of conditions and the following disclaimer.
21
22  Redistributions in binary form must reproduce the above copyright
23  notice, this list of conditions and the following disclaimer in the
24  documentation and/or other materials provided with the distribution.
25
26  Neither the name of the University of Colorado nor the names of its
27  contributors may be used to endorse or promote products derived from
28  this software without specific prior written permission.
29
30  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
31  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
32  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
33  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
34  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
35  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
36  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
37  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
38  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
39  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
40  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
41  POSSIBILITY OF SUCH DAMAGE.]
42
43******************************************************************************/
44#include "sat.h"
45#include "stdio.h"
46#include "malloc.h"
47#include "util.h"
48
49/* #define NOBLOCKINGCL */
50/* #define DEBUG */
51/* #define TEST */
52
53#define STATS
54static char rcsid[] UNUSED = "$Id $";
55
56/*---------------------------------------------------------------------------*/
57/* Constant declarations                                                     */
58/*---------------------------------------------------------------------------*/
59
60/*---------------------------------------------------------------------------*/
61/* Structure declarations                                                    */
62/*---------------------------------------------------------------------------*/
63
64/*---------------------------------------------------------------------------*/
65/* Type declarations                                                         */
66/*---------------------------------------------------------------------------*/
67
68/*---------------------------------------------------------------------------*/
69/* Variable declarations                                                     */
70/*---------------------------------------------------------------------------*/
71
72/*---------------------------------------------------------------------------*/
73/* Macro declarations                                                        */
74/*---------------------------------------------------------------------------*/
75
76/**AutomaticStart*************************************************************/
77
78/*---------------------------------------------------------------------------*/
79/* Static function prototypes                                                */
80/*---------------------------------------------------------------------------*/
81static void sat_sort_clause_array_by_length_aux(long *carr, long size);
82/**AutomaticEnd***************************************************************/
83/*---------------------------------------------------------------------------*/
84/* Definition of exported functions                                          */
85/*---------------------------------------------------------------------------*/
86
87/**Function********************************************************************
88
89  Synopsis    [ Initialize options for distillation ]
90
91  Description [ Initialize options for distillation ]
92
93  SideEffects [ This function allows external application to initialize
94                the options of distillation. ]
95
96  SeeAlso     [ sat_init_options_for_varelim, sat_init_options_for_distill]
97
98******************************************************************************/
99void
100sat_init_options_for_distill(satManager_t *m) 
101{
102
103  if (m == 0) 
104    fprintf(stderr, "ERROR : SAT manager is not initialized!\n");
105
106  m->distill = 1;
107  m->simplify = 1;
108  m->nIteratePreprocess = 1; 
109
110  /** set to 1 if periodic distillation
111   *  is requested to be enabled.
112   */
113  m->periodicDistill = 0; 
114}
115
116/**Function********************************************************************
117
118  Synopsis    [ Distill all the clauses ]
119
120  Description [ Distill all the clauses ]
121
122  SideEffects [ ]
123
124  SeeAlso     [ sat_distill_clauses ]
125
126******************************************************************************/
127void
128sat_distill_clauses_with_preprocessing(satManager_t *m)
129{
130double btime;
131 
132  btime = (double)util_cpu_time();
133 
134  m->nInClForDistill = 0;
135  m->nInLitForDistill = 0;
136  m->nInLearnedClForDistill = 0; 
137  m->nInLearnedLitForDistill = 0; 
138
139  m->nLearnedClInDistill = 0;
140  m->nLearnedLitInDistill = 0;
141  m->ternary = 0;
142
143  if (m->nCurClauseLits < 500000) {
144    m->distillMin = 3; 
145    m->distillMax = 15;
146  }
147  else if (m->nCurClauseLits >= 500000 && m->nCurClauseLits < 1000000){
148    m->distillMin = 3;
149    m->distillMax = 8;
150  }
151  else {
152    m->distillMin = (m->minorityClauseLength < m->majorityClauseLength ? m->minorityClauseLength : m->majorityClauseLength);
153    m->distillMin = (m->distillMin > 4 ? 4 : m->distillMin - 1);
154    m->distillMax = (m->distillMin > 8 ? 8 : m->distillMin + 1);
155  }
156 
157  sat_distill_clauses_array(m, m->clauses, 0);
158 
159  if (m->status == 2)
160    sat_reshape_cnf_database_with_distilled_clauses(m, 1);
161  else   return ;
162
163  m->distillTime += ((double)util_cpu_time() - btime) / 1000.0;
164 
165  sat_report_result_for_distillation(m); 
166
167  m->distill++;
168
169  if (m->status != 2) 
170    return;
171}
172
173
174/**Function********************************************************************
175
176  Synopsis    [ Distill set of clauses ]
177
178  Description [ Distill set of clauses ]
179
180  SideEffects [ ]
181
182  SeeAlso     [ ]
183
184******************************************************************************/
185void 
186sat_distill_clauses_array(satManager_t *m, satArray_t* clauses, long learned)
187{
188
189  sat_choose_candidates_for_distillation(m, clauses);
190
191  if (m->status != 2)
192    return ;
193
194#ifdef STATS
195  if (m->nDistill > 0 && learned)
196    fprintf(stdout, "| %9s | %7ld %8ld %8ld | %8s %8ld %6.0f | %8s |\n",
197          "DISTILL", m->variableHeap->size, 
198          m->nInClForDistill, m->nInLitForDistill, 
199          "PERIOD", m->nInLearnedClForDistill, 
200          (double)m->nInLearnedLitForDistill/(double)m->nInLearnedClForDistill,
201          "REDUCED");           
202
203#endif
204
205  sat_build_ternary_tree(m, clauses);
206  sat_ternary_tree_based_implication(m, m->ternary, 1, learned);
207  sat_free_ternary(m->ternary);
208  m->ternary = 0;
209}
210
211/** Choose candidates for distillation with squeezing set of clauses **/
212void 
213sat_choose_candidates_for_distillation(satManager_t *m, satArray_t* clauses)
214{
215long min, max;
216long i, j, k, csize;
217satClause_t *c;
218
219  min = m->distillMin;
220  max = m->distillMax;
221 
222  if (m->limitDistill && (clauses == m->learned)) {
223    for (i = j = 0; i < m->preLearnedPos; i++) {
224      c = (satClause_t*)clauses->space[i];
225
226      if (sat_squeeze_clause(m, c)) {
227        clauses->space[j++] = (long)c;
228        c->size |= SATCIrredundant;
229        csize = SATSizeClause(c);
230        m->nInLearnedClForDistill++; 
231        m->nInLearnedLitForDistill += csize;
232      }
233      else {
234        c->size -= SATCVisited; /* was set by sat_squeeze_clause */ 
235      }
236    } 
237  }
238  else {
239    i = j = 0;
240  }
241
242  for ( ; i < clauses->size; i++) {
243    c = (satClause_t*)clauses->space[i];
244
245    if (sat_squeeze_clause(m, c)) {
246      clauses->space[j++] = (long)c;
247      csize = SATSizeClause(c);
248
249      if (SATClauseLearned(c)) {
250        m->nInLearnedClForDistill++; 
251        m->nInLearnedLitForDistill += csize;
252      }
253      else {
254        m->nInClForDistill++; 
255        m->nInLitForDistill += csize;
256      }
257     
258      /** filter clause with bound of size **/
259      if ((csize >= min) && (csize <= max))  {
260        for (k = 0; k < csize; k++) 
261          m->scores[c->lits[k]]++;
262      }
263      else {
264        c->size |= SATCIrredundant; 
265      }
266    }
267    else 
268      c->size -= SATCVisited; /* was set by sat_squeeze_clause */ 
269  }
270  clauses->size -= (i-j);
271}
272
273void
274sat_reshape_cnf_database_with_distilled_clauses(satManager_t *m, int checkSubsumption)
275{
276satQueue_t *subsumptionQueue;
277
278  subsumptionQueue = m->satQueue;
279 
280  sat_squeeze_clauses_array(m, checkSubsumption);
281 
282  if (checkSubsumption) {
283    sat_build_occurrence_list(m);
284    while (subsumptionQueue->size > 0) {
285      if (sat_backward_subsumption_check(m)) {
286        sat_gather_touched_clauses(m);
287        if (sat_implication_on_all_watched_literals(m)) {
288          m->status = 0;
289          break;
290        }
291      }
292      else break;
293    }
294
295    if (m->status == 2) {
296      /*sat_init_clauses_statistics(m); */
297      sat_reset_all_watched_lists(m);
298      sat_recover_clauses_DB(m);
299      sat_remove_marked_clauses(m, m->clauses); 
300      sat_remove_marked_clauses(m, m->learned); 
301      sat_assert_pure_literals(m);
302
303      m->nOutClForDistill = m->clauses->size;
304      m->nOutLitForDistill = m->nCurClauseLits; 
305      m->nOutLearnedClForDistill = m->learned->size;
306      m->nOutLearnedLitForDistill = m->nCurLearnedLits;
307    }
308  }
309
310  sat_heap_remove_var_assigned_level_zero(m, m->variableHeap);
311}
312
313void 
314sat_squeeze_clauses_array(satManager_t *m, int checkSubsumption)
315{
316long i, j, csize;
317satClause_t *c;
318satArray_t *clauses;
319
320  sat_reset_all_watched_lists(m);
321  /*sat_init_clauses_statistics(m);*/
322
323  clauses = m->clauses;
324  for (i = j = 0; i < clauses->size; i++) {
325    c = (satClause_t*)clauses->space[i];
326    csize = SATSizeClause(c);
327
328    if (csize == 1) {
329      if (SATClauseIrredundant(c))
330        c->size -= SATCIrredundant;
331
332      sat_update_clauses_statistics(m, c);
333      clauses->space[j++] = (long)c;
334      continue;
335    }
336   
337    if (!SATClauseIrredundant(c) || !sat_squeeze_clause(m, c)) {
338      sat_free_clause(c);
339    }
340    else {
341      if (checkSubsumption)
342        sat_sort_clause_literal(c);
343     
344      sat_add_watched_literal(m, c);
345      sat_update_clauses_statistics(m, c);
346      clauses->space[j++] = (long)c;
347      c->size -= SATCIrredundant;
348    }
349  }
350  clauses->size -= (i-j);
351
352  clauses = m->learned;
353  for (i = j = 0; i < clauses->size; i++) {
354    c = (satClause_t*)clauses->space[i];
355    csize = SATSizeClause(c);
356
357    if (csize == 1) {
358      if (SATClauseIrredundant(c)) 
359        c->size -= SATCIrredundant;
360 
361      sat_update_clauses_statistics(m, c);
362      clauses->space[j++] = (long)c;
363      m->nCurLearnedLits++;
364      continue;
365    }
366   
367    if (!SATClauseIrredundant(c) || !sat_squeeze_clause(m, c)) {
368      sat_free_clause(c);
369    }
370    else {
371      /*if (SATClauseVisited(c))
372          c->size -= SATCVisited;
373      else  { */
374     
375        if (checkSubsumption) 
376          sat_sort_clause_literal(c);
377     
378        sat_add_watched_literal(m, c);
379        /*sat_update_clauses_statistics(m, c);*/
380        clauses->space[j++] = (long)c;
381        c->size -= SATCIrredundant;
382      /*} */
383    }
384  }
385  clauses->size -= (i-j); 
386}
387
388void
389sat_free_clause(satClause_t *c)
390{
391  if (c->dependent)
392    free(c->dependent);
393  free(c);
394}
395
396
397/**Function********************************************************************
398
399  Synopsis    [ Shrink a clause ]
400
401  Description [ Shrink a clause
402                Only marked literals are removed if marked == 1, and
403                only unmarked literals are removed otherwise.
404              ]
405
406  SideEffects [ ]
407
408  SeeAlso     [ ]
409
410******************************************************************************/
411void
412sat_strengthen_clause_in_conflict_analysis(satManager_t *m, satClause_t *c, int marked)
413{
414long i, csize, index, maxI;
415long lit, v, flags, abstract;
416long pcsize;
417
418  if (c == 0) return;
419
420  index = 0;
421  csize = SATSizeClause(c);
422  pcsize = csize;
423
424  if (m->marks[SATVar(c->lits[0])] == marked) {
425    lit = c->lits[0];
426    sat_array_delete_elem(m->wls[lit^1], (long)c);
427    c->lits[0] = c->lits[1];
428    if ((--csize) > 1) {
429      c->lits[1] = c->lits[csize];
430      index = 1;
431    }
432    else {
433      lit = c->lits[0];
434      sat_array_delete_elem(m->wls[lit^1], (long)c);
435    }
436  }
437  else if (m->marks[SATVar(c->lits[1])] == marked) {
438    lit = c->lits[1];
439    sat_array_delete_elem(m->wls[lit^1], (long)c);
440    c->lits[1] = c->lits[--csize];
441    if (csize == 1) {
442      lit = c->lits[0];
443      sat_array_delete_elem(m->wls[lit^1], (long)c);
444    }
445    else
446      index = 1;
447  }
448  else {
449    for (i = 2; i < csize; i++) {
450      lit = c->lits[i];
451      v = lit >> 1;
452      if (m->marks[v] == marked) {
453        c->lits[i] = c->lits[--csize];
454        break;
455      }
456    }
457  } 
458 
459  if (index > 0) {
460    maxI = 1;
461    for (i = 2; i < csize; i++) {
462      lit = c->lits[i];
463      v = lit >> 1;
464      if (m->levels[v] > m->levels[(c->lits[maxI]>>1)]) 
465        maxI = i;
466    }
467    lit = c->lits[maxI];
468    c->lits[maxI] = c->lits[1];
469    c->lits[1] = lit;
470
471    index = lit^1;
472    m->wls[index] = sat_array_alloc_insert(m->wls[index], (long)c); 
473  }
474
475  if (!(SATClauseLearned(c) || SATClauseBlock(c))) {
476    abstract = 0;
477    for (i = 0; i < csize; i++) 
478      abstract |= 1 << (SATVar(c->lits[i]) & 31);
479    c->info.abstract = abstract;
480  }
481  flags = c->size & SATCMask;
482  c->size = (csize << SATCsizeShift) | flags;
483}
484
485
486int sat_verify_watched_literal(satManager_t *m, satClause_t *c)
487{
488int found;
489long lit, i;
490satClause_t *ct;
491satArray_t *wls;
492
493  if (SATSizeClause(c) == 1)  return 0;
494 
495  found = 0;
496
497  lit= (c->lits[0])^1; 
498  wls = m->wls[lit];
499
500  /** Verification of watched literals **/
501  for (i = 0; i < wls->size; i++) {
502    ct = (satClause_t*)wls->space[i];
503    if (ct == c) {
504      found = 1;
505      break;
506    }
507  }
508  if (found == 0) {
509    fprintf(stdout, "ERROR : Missing 1-watched literal in CL(");
510    sat_print_clause(m, c);
511    fprintf(stdout, "\n");
512    return 0;
513  }
514
515  if (SATSizeClause(c) > 1) {
516    found = 0;
517 
518    lit= (c->lits[1])^1; 
519    wls = m->wls[lit];
520
521    /** Verification of watched literals **/
522    for (i = 0; i < wls->size; i++) {
523      ct = (satClause_t*)wls->space[i];
524      if (ct == c) {
525        found = 1;
526        break;
527      }
528    }
529    if (found == 0) {
530      fprintf(stdout, "ERROR : Missing 2-watched literal!\n");
531      return 0;
532    }
533  }
534
535  return 1;
536}
537
538/**Function********************************************************************
539
540  Synopsis    [ Strengthen set of clauses in conflict analysis ]
541
542  Description [ Strengthen set of clauses in conflict analysis ]
543
544  SideEffects [ ]
545
546  SeeAlso     [ ]
547
548******************************************************************************/
549void
550sat_strengthen_set_of_clauses_in_conflict_analysis(satManager_t *m)
551{
552long i, v, csize;
553satClause_t *c;
554satArray_t *pivots, *arr;
555satQueue_t *clauses_queue;
556
557  pivots = m->resolvents;
558  clauses_queue = m->satQueue; 
559
560  i = 0;
561  while (clauses_queue->size > 0) {
562    c = (satClause_t*)sat_queue_pop(clauses_queue);
563    v = pivots->space[i++];
564 
565    if (v > 0) {
566      m->marks[v] = 1;
567 
568      sat_strengthen_clause_in_conflict_analysis(m, c, 1);
569      m->marks[v] = 0;
570    }
571    else { 
572      arr = SATClauseLearned(c) ? m->learned : (c->size & SATCTheory ?
573                      m->theory : (SATClauseBlock(c) ? m->blocking :
574                              m->clauses)); 
575     
576      csize = SATSizeClause(c);
577      m->nCurClauseLits -= csize;
578      m->nTotalClauseLits -= csize;
579     
580      sat_array_delete_elem(arr, (long)c);
581      sat_delete_clause(m, c);
582    }
583  }
584  pivots->size = 0;
585}
586
587
588/**Function********************************************************************
589
590  Synopsis    [ Check if clause cp subsumes clause cq ] 
591
592  Description [ Check if clause cp subsumes clause cq, such that cp and cq are
593                the clauses participating in conflict analysis
594               
595                Precondition : All literals in cp and cq are assigned.
596
597                Return 1 if cp subsumes cq, 0 otherwise. ]
598
599  SideEffects [ ]
600
601  SeeAlso     [ ]
602
603******************************************************************************/
604int
605sat_check_subsumption_in_conflict_analysis(satManager_t *m, satClause_t *cp, satClause_t *cq)
606{
607int subsume;
608long i, j, cpsize, cqsize;
609long litp, litq;
610
611  cpsize = SATSizeClause(cp);
612  cqsize = SATSizeClause(cq);
613
614  subsume = 0;
615  for (i = 0; i < cpsize; i++) {
616    subsume = 0;
617    litp = cp->lits[i];
618    if (m->levels[litp>>1] == 0)  continue;
619
620    for (j = 0; j < cqsize; j++) {
621      litq = cq->lits[j];
622      if (m->levels[litq>>1] == 0)  continue;
623      if (litp == litq) {
624        subsume = 1;
625        break;
626      } 
627    }
628  } 
629 
630  return (subsume);
631}
632
633
634int 
635sat_check_subsumption_resolvent_and_clause(satManager_t *m, satClause_t *c, long nMarks)
636{
637long i, csize;
638long lit;
639
640  csize = SATSizeClause(c);
641  for (i = 0; i < csize; i++) {
642    lit = c->lits[i];
643    if (m->levels[lit>>1] == 0)  continue;
644    if (m->marks[lit>>1]) nMarks--;
645  }
646
647  if (nMarks > 0) return 0;
648
649  return 1;
650}
651
652/**Function********************************************************************
653
654  Synopsis    [ Apply distillation method to simplify clauses ]
655
656  Description [ Apply distillation method to simplify clauses ]
657
658  SideEffects [ Doing sat_heap_remove_var_assigned_level_zero()
659                after distillation to remove variables assigned
660                at level zero ]
661
662  SeeAlso     [ ]
663
664******************************************************************************/
665void
666sat_distill_clauses(satManager_t *m)
667{
668int nIterate; 
669double btime, mtime;
670satClause_t *conflicting;
671
672#if 1
673  if ((m->clauses->size > 4000000) || ((m->nCurClauseLits > 10000000))) {
674    sat_report_result_for_distillation(m); 
675    return;
676  }
677#endif
678
679  btime = (double)util_cpu_time();
680 
681  nIterate = 1; 
682  m->nLearnedClInDistill = 0;
683  m->nLearnedLitInDistill = 0;
684
685beginDistill: 
686  nIterate--; 
687  conflicting = sat_implication(m);
688  if(conflicting) {
689    m->status = 0;
690    return;
691  }
692
693  /** In recomputing variable scores,
694   *  pure literals generated due to
695   *  unit propagations at preprocessing.
696   *  If no clause is unsatisfied,
697   *  sat_recompute_var_score returns
698   *  FALSE and the solver turns out
699   *  the problem is SATISFIABLE. 
700   **/
701  if (!sat_recompute_var_score(m)) {
702    m->status = 1;     
703    memset(m->scores, 0, sizeof(long)*((m->nVars+1)<<1)); 
704    sat_report_result_for_distillation(m); 
705    return;
706  }
707  sat_build_ternary_tree(m, m->clauses);
708
709  /** Apply distillation procedure on the trie built **/
710  sat_ternary_tree_based_implication(m, m->ternary, 1, 0);
711  m->nDistill++;
712 
713  if (m->status != 2) {
714    m->distillTime = ((double)util_cpu_time() - btime) / 1000.0;
715    sat_report_result_for_distillation(m); 
716    return;
717  } 
718 
719  /*sat_assert_pure_literals(m);
720  conflicting = sat_implication(m);*/
721  /** Assertion :
722      1. Current level is zero.
723      2. No pure literal causes conflict.
724  **/
725  sat_init_clauses_statistics(m);
726  sat_delete_unmakred_clauses_for_simplification(m);
727  sat_print_clauses_histogram(m);
728  sat_free_ternary(m->ternary);
729
730  mtime = m->elimTime;
731#if 1
732  if (m->status == 2) {
733    if (mtime < 5.0) {
734      m->nIteratePreprocess = 0;
735      sat_build_occurrence_list(m);
736      while (m->satQueue->size > 0) { 
737        if (sat_backward_subsumption_check(m)) {
738          sat_gather_touched_clauses(m);
739          conflicting = sat_implication_on_all_watched_literals(m); 
740          if (conflicting) {
741            m->status = 0;
742            break;
743          } 
744        }
745        else break;
746      }
747
748      if (m->status == 2) {
749        sat_init_clauses_statistics(m);
750        sat_reset_all_watched_lists(m);
751        sat_recover_clauses_DB(m);
752        sat_remove_marked_clauses(m, m->clauses); 
753        sat_remove_marked_clauses(m, m->learned); 
754        sat_assert_pure_literals(m);
755      } 
756    }
757  } 
758#endif
759
760  m->distillTime = ((double)util_cpu_time() - btime) / 1000.0;
761 
762  if ((m->status == 2) && (nIterate > 0)) 
763    goto beginDistill; 
764 
765  sat_report_result_for_distillation(m); 
766}
767
768/**Function********************************************************************
769
770  Synopsis    [ Builds the trie structure of CNF clauses. ]
771
772  Description [ Builds the trie structure of CNF clauses. ]
773
774  SideEffects [ ]
775
776  SeeAlso     [ ]
777
778******************************************************************************/
779void
780sat_build_ternary_tree(satManager_t *m, satArray_t *clauses)
781{
782long range, count;
783long i, j, csize;
784long v, lit;
785satArray_t *clauseArray;
786satTernary_t *root;
787satClause_t *c;
788
789  /** Build a ternary search tree(TST)
790   *  first, which the procedure will
791   *  traverse to generate the trie trees
792   *  for the clause data base.
793   *  ------------------------------------
794   *  REVISION. Trie structure is not
795   *  required any more. Rather, TST will
796   *  be used to represnt all the clauses
797   *  for distillation.
798   *  -----------------------------------
799   **/
800
801  if (m->ternary == 0) {
802    root = (satTernary_t *)malloc(sizeof(satTernary_t));
803    memset(root, 0, sizeof(satTernary_t));
804    m->ternary = root;
805  }
806  else
807    root = m->ternary;
808
809  clauseArray = sat_array_alloc(4);
810 
811  range = clauses->size; 
812  count = 0;
813  /** Build a ternary searching tree(TST)
814   *  by scanning each clause. Since how
815   *  balanced TST is will affect time
816   *  consumption for traversing each node
817   *  in turn, clauses are randomly chosen
818   *  in building TST.
819   **/
820  while (count < range) {
821    i = (long)(sat_drand(m) * range);
822    c = (satClause_t*)clauses->space[i];
823    if (c == 0) continue;
824
825    /** Filter out duplicate clause
826     *  which has been scanned before.
827     *  This can happen, because
828     *  the random function may generate
829     *  the same number several times
830     *  within uniform distribution.
831     **/
832    count++;
833
834    if (SATClauseIrredundant(c))  continue;
835   
836    clauseArray->size = 0;
837    if (!SATClauseVisited(c)) {
838      c->size |= SATCVisited;
839
840      /** Copy the array of literals of the clause
841       *  into the buffer used to do quick-sorting
842       **/
843      csize = SATSizeClause(c);
844      for (j=0; j<csize; j++) {
845        lit = c->lits[j];
846        v = lit>>1;
847        if (m->values[v] == 2) {
848          clauseArray = sat_array_insert(clauseArray, lit);
849        }
850      }
851      if (clauseArray->size == 0)       continue; 
852   
853      clauseArray = sat_array_insert(clauseArray, -(long)c);
854      sat_sort_literal_by_score(clauseArray, m->scores);
855      if (root->id == 0) {
856        root->id = clauseArray->space[0] >> 1;
857      }
858      sat_insert_ternary_tree(root, clauseArray);
859    }
860  }
861
862  /** Second traverse clauses to complete TST
863   *  due to the clauses missed such that the
864   *  indices of clauses are out of range of
865   *  th random numbers generated.
866   **/ 
867   for (i=0; i < range; i++) {
868    c = (satClause_t*)clauses->space[i];
869    clauseArray->size = 0;
870    if (c ==0)  continue;
871
872    if (SATClauseIrredundant(c)) continue;
873 
874    if (SATClauseVisited(c)) {
875      c->size -= SATCVisited;
876    }
877    else {
878      /** Copy the array of literals of the clause
879       *  into the buffer used to do quick-sorting
880       **/
881      csize = SATSizeClause(c);
882      for (j=0; j< csize; j++) {
883        lit = c->lits[j];
884        v = lit>>1;
885        if (m->values[v] == 2) {
886          clauseArray = sat_array_insert(clauseArray, lit);
887        }
888      }
889      if (clauseArray->size == 0)       continue; 
890     
891      clauseArray = sat_array_insert(clauseArray, -((long)c));
892      sat_sort_literal_by_score(clauseArray, m->scores);
893     
894      if (root->id == 0) {
895        root->id = clauseArray->space[0] >> 1;
896      }
897      sat_insert_ternary_tree(root, clauseArray);
898    }
899  }
900
901  m->ternary = root;
902  free(clauseArray);
903 
904  if (m->ternary) { 
905#ifdef DEBUG
906    sat_print_dot_for_ternary_search_tree(m, root, 0);
907#endif
908
909    if (m->verbosity > 2)
910      sat_print_scores(m);
911  }
912}
913
914/**Function********************************************************************
915
916  Synopsis    [ sort literals by the scores ]
917
918  Description [ sort literals by the scores ]
919
920  SideEffects [ ]
921
922  SeeAlso     [ ]
923
924******************************************************************************/
925void 
926sat_sort_literal_by_score(satArray_t *arr, long *scores)
927{
928
929  sat_sort_literal_by_score_aux(&(arr->space[0]), scores, arr->size-1);
930}
931
932void
933sat_sort_literal_by_score_aux(long *lits, long *scores, long size)
934{
935long i, j, tmp, bi;
936long pivot;
937
938  /** TODO : We may need a tiebreaker in a way. **/
939  if(size <=15) {
940    for(i=0; i<size-1; i++) {
941      bi = i;
942      for(j=i+1; j<size; j++) {
943        if(scores[lits[j]] > scores[lits[bi]])
944          bi = j;
945      }
946      tmp = lits[i];
947      lits[i] = lits[bi];
948      lits[bi] = tmp;
949    }
950  }
951  else {
952    pivot = scores[lits[size>>1]];
953    i = -1;
954    j = size;
955
956    while(1) {
957      do i++; while(scores[lits[i]] > pivot);
958      do j--; while(pivot > scores[lits[j]]);
959      if(i>=j)  break;
960      tmp = lits[i];
961      lits[i] = lits[j];
962      lits[j] = tmp;
963    }
964    sat_sort_literal_aux(lits, i);
965    sat_sort_literal_aux(&(lits[i]), size-i);
966  }
967}
968
969/**Function********************************************************************
970
971  Synopsis    [ Insert a literal to ternary tree for Alembic ]
972
973  Description [ Insert a literal to ternary tree for Alembic
974                TST (Ternary Search Tree) ]
975
976  SideEffects [ ]
977
978  SeeAlso     [ ]
979
980******************************************************************************/
981void
982sat_insert_ternary_tree(satTernary_t *root, satArray_t *clause)
983{
984int inverted;
985long v, *plit, lit, i, size;
986satTernary_t *ternary;
987
988  ternary = root;
989  plit = clause->space;
990  size = clause->size;
991 
992  for (i=0; ;) {
993    lit = *plit;
994    v = lit >> 1;
995    inverted = lit&1;
996 
997    if (ternary->id == 0)       return;
998
999    /* Going down to ternary search tree */
1000    if (v < ternary->id) {
1001      if (ternary->lokid == 0) { 
1002        /* Creating a ternary node first */
1003        ternary->lokid = ALLOC(satTernary_t, 1);
1004        memset(ternary->lokid, 0, sizeof(satTernary_t));
1005        ternary = ternary->lokid;
1006        ternary->id = v;
1007      }
1008      else 
1009        ternary = ternary->lokid;
1010    } 
1011    else if (v == ternary->id) {
1012      ++plit; ++i;
1013      if (i >= size - 1) {
1014        /* create a new terminal node */
1015        if (ternary->eqleaf.eqkid[inverted] == 0) {
1016          ternary->eqleaf.eqkid[inverted] = ALLOC(satTernary_t, 1);
1017          memset(ternary->eqleaf.eqkid[inverted], 0, sizeof(satTernary_t));
1018          ternary = ternary->eqleaf.eqkid[inverted];
1019          ternary->id = 0;
1020          ternary->eqleaf.c = (satClause_t*)(-(*plit));
1021         
1022          return;
1023        }
1024        /* cut an existing branch out
1025           with a new terminal node */
1026        ternary = ternary->eqleaf.eqkid[inverted];
1027        if (ternary->id > 0) {
1028          ternary->id = 0; 
1029          sat_free_ternary(ternary->lokid);
1030          ternary->lokid = 0;
1031          sat_free_ternary(ternary->eqleaf.eqkid[0]);
1032          sat_free_ternary(ternary->eqleaf.eqkid[1]);
1033          ternary->eqleaf.eqkid[0] = ternary->eqleaf.eqkid[1] = 0;
1034          ternary->eqleaf.c = (satClause_t*)(-(*plit));
1035          sat_free_ternary(ternary->hikid);
1036          ternary->hikid = 0;
1037          return;
1038        }
1039        /* meet an existing terminsal node,
1040           then forget to insert this clause */
1041        return;
1042      }
1043   
1044      if (ternary->eqleaf.eqkid[inverted]== 0) {
1045        ternary->eqleaf.eqkid[inverted]= ALLOC(satTernary_t, 1);
1046        memset(ternary->eqleaf.eqkid[inverted], 0, sizeof(satTernary_t));
1047        ternary = ternary->eqleaf.eqkid[inverted];
1048        ternary->id = (*plit) >> 1;
1049      }
1050      else
1051        ternary = ternary->eqleaf.eqkid[inverted];
1052    }
1053    else {
1054      if (ternary->hikid == 0) {
1055        /* Creating a ternary node first */
1056        ternary->hikid = ALLOC(satTernary_t, 1);
1057        memset(ternary->hikid, 0, sizeof(satTernary_t));
1058        ternary = ternary->hikid;
1059        ternary->id = v;
1060      }
1061      else
1062        ternary = ternary->hikid;
1063    } 
1064  }
1065}
1066
1067/**Function********************************************************************
1068
1069  Synopsis    [ Apply implication based on ternary tree ]
1070
1071  Description [ Apply implication based on ternary tree
1072               
1073                Special DPLL procedure for distillation performs on the framework
1074                of depth-first-search based on a ternary searching tree.
1075                For each ternary node, lokid, eqkid, and hikid are traversed in order.
1076                For visiting lokid and hikid, nothing but invoking of the function
1077                itself(sat_ternary_tree_ based _ implication()) is conducted. Making
1078                a decision and implication are called, when it stays between them.
1079             ]
1080
1081  SideEffects [  Dependency between sat_ternary_based_back_track() and
1082                   sat_add_learned_clause()
1083
1084                For the case of conflict, the failure driven assertion literal
1085                (FdalLit) is derived by conflict analysis, and it is enqueued
1086                to be asserted by the function sat_enqueue(), which is called
1087                when the computed conflict clause is added, i.e. sat_add_learned_clause().
1088                Enqueuing is performed only if the issued literal is unassigned,
1089                and is skipped  otherwise. Hence, backtracking to undo the current
1090                assignments must come before adding the conflict clause in conflict
1091                analysis.
1092              ]
1093
1094  SeeAlso     []
1095
1096******************************************************************************/
1097void 
1098sat_ternary_tree_based_implication(
1099        satManager_t *m,
1100        satTernary_t *ternary, 
1101        int depth, 
1102        long learned)
1103{
1104long vid;
1105char value;
1106satTernary_t *child;
1107satClause_t *traversed, *conflicting;
1108
1109  if (ternary == 0)     return;
1110 
1111  /** traverse down to the path for lokid
1112      which must be in the same level as
1113      the current node traversing, as if
1114      they are the nodes of trie-trees..
1115   **/
1116  if (m->status == 2 && ternary->lokid)
1117    sat_ternary_tree_based_implication(m, ternary->lokid, depth, learned);
1118
1119DistillANode:
1120  /** perform distillation based implications
1121      for both eqkid0 and eqkid1.
1122    **/
1123
1124  if (m->status != 2) return;
1125  vid = ternary->id;
1126
1127  if (vid > 0) {
1128    value = m->values[vid];
1129    if (value < 2) {
1130      child = ternary->eqleaf.eqkid[!value];   
1131      /* current node is assigned either
1132         0 or 1 already */
1133      if (m->levels[vid] >= 1 && child != 0) {
1134        m->nResolvedInDistill++;
1135        if (child) {
1136          if (child->id == 0) {
1137            /* terminal node which stores a pointer
1138               to a clause currently traversing */
1139            traversed = (satClause_t*)child->eqleaf.c;
1140            traversed->size |= SATCIrredundant; 
1141          }
1142          else
1143            sat_resolvent_analysis(m, ternary, learned); 
1144        }
1145      }
1146      child = ternary->eqleaf.eqkid[(int)value];
1147      if (child && child->id > 0 && m->status == 2)
1148        sat_ternary_tree_based_implication(m, child, depth, learned);
1149     
1150      goto TraverseHikid;
1151    }
1152  }
1153 
1154  /* go for eqkid[0] */
1155  child = ternary->eqleaf.eqkid[0];
1156  if (child && m->status == 2) {
1157    sat_make_decision_based_on_trie(m, ((vid<<1)|1));
1158    conflicting = sat_implication_for_simplification(m);
1159     
1160    if (conflicting) {
1161      sat_conflict_analysis_with_distillation(m, conflicting, learned);
1162      m->nLearnedInDistill++;
1163    }
1164    else if (m->status == 2) {
1165      sat_ternary_tree_based_implication(m, child, depth+1, learned);
1166      sat_ternary_tree_based_undo(m, depth-1);
1167    }
1168  }
1169 
1170  /* go for eqkid[1] */
1171  child = ternary->eqleaf.eqkid[1];
1172  if (child && m->status == 2) {
1173    sat_make_decision_based_on_trie(m, (vid<<1));
1174    conflicting = sat_implication_for_simplification(m); 
1175   
1176    if (conflicting) {
1177      sat_conflict_analysis_with_distillation(m, conflicting, learned);
1178      m->nLearnedInDistill++;
1179    }
1180    else if (m->status == 2)  {
1181      sat_ternary_tree_based_implication(m, child, depth+1, learned);
1182      sat_ternary_tree_based_undo(m, depth-1);
1183    }
1184  }
1185   
1186  /* backtrack to level 0 due to unit conflict */ 
1187  if (m->status == 3 && depth == 1) {
1188    m->status = 2;
1189
1190    conflicting = sat_implication(m); 
1191    if (conflicting) {
1192      m->status = 0;
1193#ifndef STATS
1194      fprintf(stdout, "# Conflict at level 0!\n");             
1195      fprintf(stdout, "Conflict at (");
1196      sat_print_clause_simple(m, conflicting);
1197      fprintf(stdout, ")\n");
1198      sat_print_dot_for_implication_graph(m, conflicting, 0, 1);
1199#endif
1200      return;
1201    } 
1202    /* resume distilling from the root of the
1203       current traversing branch */
1204    goto DistillANode;
1205  }
1206
1207  /** traverse down to the path for hikid
1208      which must be in the same level as
1209      the current node traversing, as if
1210      they are the nodes of trie-trees..
1211   **/
1212TraverseHikid:
1213  if (m->status == 2 && ternary->hikid)
1214    sat_ternary_tree_based_implication(m, ternary->hikid, depth, learned);
1215}
1216
1217
1218/**Function********************************************************************
1219
1220  Synopsis    [ Make decision based on trie in distillation ]
1221
1222  Description [ Make decision based on trie in distillation ]
1223
1224  SideEffects []
1225
1226  SeeAlso     []
1227
1228******************************************************************************/
1229void 
1230sat_make_decision_based_on_trie(satManager_t *m, long lit)
1231{
1232  m->decisionStackSeperator = 
1233      sat_array_insert(m->decisionStackSeperator, m->stackPos);
1234  sat_enqueue(m, lit, 0);
1235}
1236
1237/**Function********************************************************************
1238
1239  Synopsis    [ Undo assignment on the ternary tree ]
1240
1241  Description [ Undo assignment on the ternary tree ]
1242
1243  SideEffects []
1244
1245  SeeAlso     []
1246
1247******************************************************************************/
1248void
1249sat_ternary_tree_based_undo(satManager_t *m, long level)
1250{
1251long i, v;
1252 
1253  if (SATCurLevel(m) > level) {
1254    for (i= m->stackPos-1; i>= m->decisionStackSeperator->space[level]; i--) {
1255      v = m->decisionStack[i] >> 1;
1256      m->values[v] = 2;
1257      m->levels[v] = -1;
1258      m->marks[v] = 0;
1259    } 
1260    m->curPos = m->decisionStackSeperator->space[level];
1261    m->stackPos = m->curPos;
1262    m->decisionStackSeperator->size = level;
1263  }
1264}
1265/**Function********************************************************************
1266
1267  Synopsis    [ Analyzes implication graph to find a good resolvent ]
1268
1269  Description [ Analyzes implication graph to find a good resolvent ]
1270
1271  SideEffects []
1272
1273  SeeAlso     []
1274
1275******************************************************************************/
1276satClause_t* 
1277sat_resolvent_analysis(
1278        satManager_t *m, 
1279        satTernary_t *t,
1280        long learned)
1281{
1282int value, maxI;
1283long i, j;
1284long v, lit, cLit, csize ;
1285satArray_t *clearned, *cclearned, *redundant;
1286satClause_t *c;
1287
1288  v = t->id;
1289
1290  value = m->values[v];
1291 
1292  /** Analyze implication graph to get decisions. **/
1293  clearned = m->clearned;
1294  clearned->size = 0;
1295  cclearned = m->cclearned;
1296  cclearned->size = 0;
1297  redundant = m->redundant;
1298  redundant->size = 0;
1299
1300  lit = (v<<1) | !value;        /* (value==1 ? (v<<1) : (v<<1)|1); */
1301  clearned = sat_array_insert(clearned, lit);
1302
1303  redundant = sat_array_insert(redundant, lit);
1304  while (redundant->size > 0) {
1305    redundant->size--;
1306    c = m->antes[(redundant->space[redundant->size])>>1];
1307    csize = SATSizeClause(c);
1308    for (j = 1; j < csize; j++) {
1309      cLit = c->lits[j];
1310      v = cLit >> 1;
1311      if (!m->marks[v] && m->levels[v] > 0) {
1312        m->marks[v] = 1;
1313        cclearned = sat_array_insert(cclearned, cLit);
1314        if (m->antes[v] != 0) {
1315          redundant = sat_array_insert(redundant, cLit);
1316        }
1317        else {
1318          /* reached a decision */
1319          clearned = sat_array_insert(clearned, cLit); 
1320        }
1321      }
1322    }
1323  }
1324
1325  maxI = 1;
1326  for (i = 2; i < clearned->size; i++) 
1327    if (m->levels[(clearned->space[i])>>1] > m->levels[(clearned->space[maxI])>>1])
1328      maxI = i;
1329
1330  lit = clearned->space[maxI]; 
1331  clearned->space[maxI] = clearned->space[1];
1332  clearned->space[1] = lit;
1333
1334  c = sat_add_distilled_clause(m, clearned, learned);
1335  c->size |= SATCIrredundant;
1336
1337  m->clearned = clearned;
1338  m->cclearned = cclearned;
1339  m->redundant = redundant;
1340  for (i=0; i<cclearned->size; i++) {
1341      lit = cclearned->space[i]; 
1342      m->marks[lit>>1] = 0;
1343  }
1344  return (c);
1345}
1346
1347
1348/**Function********************************************************************
1349
1350  Synopsis    [ Apply implication until the implication queue is empty. ]
1351
1352  Description [ Extension of standard BCP procedure to check subsumption. ]
1353
1354  SideEffects []
1355
1356  SeeAlso     [sat_implication]
1357
1358******************************************************************************/
1359satClause_t *
1360sat_implication_for_simplification(satManager_t *m)
1361{
1362satClause_t *conflicting, *c;
1363satArray_t *wl;
1364satClause_t **i, **j, **end;
1365long lit, iLit, first;
1366long csize, k;
1367long nProps;
1368
1369  nProps = 0;
1370  conflicting = 0;
1371
1372  while(m->curPos < m->stackPos) {
1373    lit = m->decisionStack[m->curPos++];
1374    wl = m->wls[lit];
1375
1376    if(wl == 0) continue;
1377    nProps++;
1378    /** Sort wl by the number of literals of each clause,
1379        to find implicate which is not subsumed by any
1380        other clause.
1381    **/
1382    sat_sort_clause_array_by_length(wl); 
1383
1384    for(i = j = (satClause_t **)&(wl->space[0]), end = i + wl->size; i != end;) {
1385      c = *i++;
1386
1387      iLit = lit ^ 1;
1388      /*if(c == 0 || ((c->lits[0] != iLit) && (c->lits[1] != iLit)))
1389        continue;*/
1390
1391      if(c->lits[0] == iLit)
1392        c->lits[0] = c->lits[1], c->lits[1] = iLit;
1393
1394      first = c->lits[0];
1395      if((m->values[first>>1]^SATSign(first)) == 1) {
1396        *j++ = c;
1397      }
1398      else {
1399        csize = c->size >> SATCsizeShift;
1400        for(k=2; k<csize; k++) {
1401          if((m->values[c->lits[k]>>1] ^ SATSign(c->lits[k])) != 0) {
1402            c->lits[1] = c->lits[k];
1403            c->lits[k] = iLit;
1404            m->wls[(c->lits[1]^1)] = sat_array_alloc_insert(m->wls[(c->lits[1]^1)], (long)c);
1405            /*c->size |= SATCIrredundant; */
1406            goto foundWatch;
1407          }
1408        }
1409
1410        *j++ = c;
1411        if((m->values[first>>1]^SATSign(first)) == 0) {
1412          conflicting = c;
1413          m->curPos = m->stackPos;
1414          while(i<end)  *j++ = *i++;
1415        }
1416        else {
1417         /* if (SATClauseLearned(c) && !learned)
1418            c->size |= SATCIrredundant; */
1419          sat_enqueue(m, first, c);
1420        }
1421      }
1422foundWatch:;
1423    }
1424    wl->size -= i-j;
1425  }
1426  m->nImplicationsInDistill += nProps;
1427  /*m->simpDBProps -= nProps; */
1428  return(conflicting);
1429}
1430
1431/**Function********************************************************************
1432
1433  Synopsis    [ Sort a list of clauses by the number of literals in a clause. ]
1434
1435  Description [ Sort a list of clauses by the number of literals in a clause. ]
1436
1437  SideEffects []
1438
1439  SeeAlso     [ sat_sort_clause_array_by_length_aux ]
1440
1441******************************************************************************/
1442void
1443sat_sort_clause_array_by_length(satArray_t *cl)
1444{
1445  sat_sort_clause_array_by_length_aux(&(cl->space[0]), cl->size);
1446}
1447
1448static void
1449sat_sort_clause_array_by_length_aux(long *carr, long size)
1450{
1451long i, j, tmp, bi;
1452satClause_t *pivot;
1453satClause_t *x, *y;
1454
1455  if(size <=15) {
1456    for(i=0; i<size-1; i++) {
1457      bi = i;
1458      for(j=i+1; j<size; j++) {
1459        x = ((satClause_t *)(carr[j]));
1460        y = ((satClause_t *)(carr[bi]));
1461        if((x->size>>3) < (y->size>>3)) 
1462          bi = j;
1463      }
1464      tmp = carr[i];
1465      carr[i] = carr[bi];
1466      carr[bi] = tmp;
1467    }
1468  }
1469  else {
1470    pivot = (satClause_t *)carr[size>>1];
1471    i = -1;
1472    j = size;
1473
1474    while(1) {
1475      do i++; while( (((satClause_t *)(carr[i]))->size>>3) > 2 && ((pivot->size>>3) <= 2 ||
1476              ((satClause_t *)(carr[i]))->info.activity < pivot->info.activity));
1477      do j--; while( (pivot->size>>3) > 2 && ((((satClause_t *)(carr[j]))->size>>3) <= 2 ||
1478              pivot->info.activity < ((satClause_t *)(carr[j]))->info.activity));
1479      if(i>=j)  break;
1480      tmp = carr[i];
1481      carr[i] = carr[j];
1482      carr[j] = tmp;
1483    }
1484    sat_sort_clause_array_by_length_aux(carr, i);
1485    sat_sort_clause_array_by_length_aux(&(carr[i]), size-i);
1486  }
1487}
1488
1489/**Function********************************************************************
1490
1491  Synopsis    [ Conflict analysis based on ternary tree structure ]
1492
1493  Description [ Conflict analysis based on ternary tree structure ]
1494
1495  SideEffects []
1496
1497  SeeAlso     []
1498
1499******************************************************************************/
1500long
1501sat_conflict_analysis_with_distillation(satManager_t *m, satClause_t *conflicting, long learned)
1502{
1503int isNotDecision;
1504long nMarks, i, j, maxI, limit;
1505long lit, *pLit, cLit;
1506long absLevel, bLevel;
1507long v, csize, tv;
1508satClause_t *c;
1509satArray_t *clearned, *cclearned;
1510
1511int firstIter, subsumptionCheck;
1512int nDecisions;
1513long nAllMarks, nResolventLits;
1514long nDistilled, nLevelZeros, abstract;
1515satClause_t *resolvent, *traversed;
1516
1517#if 0
1518int elimnable, flags;
1519long abstract;
1520#endif
1521
1522  firstIter = 0;
1523  nDistilled = 0;
1524  nAllMarks = 0;
1525  nLevelZeros = 0;
1526  m->resolvents->size = 0;
1527  subsumptionCheck = m->subsumeInConflict;
1528  resolvent = (subsumptionCheck ? conflicting : 0);
1529  traversed = 0;
1530
1531  isNotDecision = 0;
1532  clearned = m->clearned;
1533  clearned->size = 0;
1534  clearned = sat_array_insert(clearned, 0);
1535  i = m->stackPos - 1;
1536  bLevel = lit = 0;
1537  nMarks = 0;
1538  tv = 0;
1539 
1540  do {
1541    nResolventLits = nAllMarks;
1542    nLevelZeros = 0;
1543    nDecisions = 0;
1544
1545    c = conflicting;
1546    csize = SATSizeClause(c);
1547    j = (lit == 0) ? 0 : 1;
1548    pLit = &(c->lits[j]);
1549   
1550    for (; j<csize; j++) {
1551      cLit = *pLit++;
1552      v = cLit >> 1;
1553
1554      if (m->antes[v] <= 0 && m->levels[v] > 0)
1555        nDecisions++;
1556
1557      if (!m->marks[v] && m->levels[v]>0) {
1558        m->marks[v] = 1;
1559
1560        nAllMarks++;
1561        if (m->levels[v] >= SATCurLevel(m))
1562          nMarks++;
1563        else {
1564          clearned = sat_array_insert(clearned, cLit);
1565          if (m->levels[v] > bLevel)
1566            bLevel = m->levels[v];
1567        }
1568      }
1569      else if (m->levels[v] == 0)
1570        nLevelZeros++;
1571    }
1572    if ((traversed == 0) && (nDecisions >= SATCurLevel(m)))
1573      traversed = c; 
1574
1575    /** Subsumption check in conflict analysis **/
1576    if (subsumptionCheck && firstIter > 0) {
1577      if (resolvent > 0 && (nResolventLits == nAllMarks)) {
1578        /* previous resolvent is subsumed by current resolvent */
1579        nDistilled++;
1580     
1581        sat_strengthen_clause_in_conflict_analysis(m, resolvent, 0);
1582        if ((csize - nLevelZeros) > nAllMarks) {
1583          /* delete the antecedent, when antecednet is also subsumed */
1584          m->nEliminatedClsInConflict++;
1585          m->nEliminatedLitsInConflict += csize;
1586          nDistilled++;
1587         
1588          if (SATClauseOriginal(resolvent) || !SATClauseOriginal(c)) {
1589            sat_array_delete_elem(m->wls[(c->lits[1])^1], (long)c);
1590            if (csize > 1)
1591              c->lits[1] = m->nVars << 1;
1592          }
1593          else {
1594            sat_strengthen_clause_in_conflict_analysis(m, c, 0);
1595          }
1596        } 
1597      }
1598      else if ((csize - nLevelZeros) > nAllMarks) {
1599        /* antecedent is subsumed by current resolvent */
1600        nDistilled++;
1601        resolvent = c;
1602        sat_strengthen_clause_in_conflict_analysis(m, resolvent, 0);
1603      }
1604      else 
1605        resolvent = 0;
1606    }
1607
1608    firstIter++;
1609    while (i>=0 && !(m->marks[(m->decisionStack[i--])>>1]));
1610    lit = m->decisionStack[i+1];
1611    tv = lit >> 1; 
1612    conflicting = m->antes[tv];
1613    m->marks[tv] = 0;
1614    nMarks--;
1615    nAllMarks--;
1616  } while (nMarks > 0);
1617  clearned->space[0] = lit^1;
1618
1619  m->nDistillInConflict += nDistilled;
1620
1621#ifdef DEBUG
1622  fprintf(stdout, "learned ");
1623  sat_print_array_as_clause(m, clearned);
1624#endif
1625
1626  m->clearned = clearned;
1627 
1628  if (clearned->size == 0) {
1629    m->status = 0; 
1630    clearned->size = 0;
1631    sat_ternary_tree_based_undo(m, 0);
1632    return 0;
1633  }
1634
1635  if (clearned->size == 1) {
1636    m->status = 3; /* BACKTRACK mode */
1637    m->nLearnedUnitClInDistill++;
1638    /** NOTE : Back tracking must be performed prior to
1639     *  adding a unit conflict clause. Or adding clause
1640     *  function will yield conflict while it asserts
1641     *  the unit clause added.
1642     **/
1643    sat_ternary_tree_based_undo(m, 0);
1644   
1645    if (resolvent > 0) {
1646      resolvent->size |= SATCIrredundant;
1647      sat_enqueue_check(m, resolvent->lits[0], resolvent);
1648      m->nOmittedConflictClauses++;
1649      m->nOmittedConflictLits++;
1650    }
1651    else {
1652      c = sat_add_distilled_clause(m, clearned, 0);
1653      c->size |= SATCIrredundant;
1654    }
1655    /** TODO : not sure for these, but not to change
1656     *  variable and clause decay tends to be more
1657     *  beneficial for industrial benchmarks.
1658     **/
1659    /*sat_update_variable_decay(m);
1660    sat_update_clause_decay(m); */
1661    clearned->size = 0;
1662    return 0;
1663  }
1664  else {
1665    cclearned = m->cclearned;
1666    cclearned->size = 0;
1667    /** minimize conflict learned clause **/
1668    absLevel = 0;
1669    for (i = 1; i < clearned->size; i++) 
1670      absLevel |= sat_abstract_level(m, (clearned->space[i])>>1);
1671    m->cclearned = cclearned = sat_array_copy(clearned, m->cclearned);
1672    isNotDecision = m->antes[(clearned->space[0]>>1)] == 0 ? 0 : 1;
1673    for(i=j=1; i < clearned->size; i++) {
1674       lit = clearned->space[i]; 
1675       v = lit >> 1;
1676       if (m->levels[v] > 0 && (m->antes[v] == 0 || !sat_is_redundant_lit(m, lit, absLevel))) {
1677         clearned->space[j++] = lit;
1678         if (m->antes[v] != 0) 
1679           isNotDecision = 1;
1680       }
1681    }
1682    clearned->size -= (i-j);
1683
1684    maxI = 1;
1685    for (i = 2; i < clearned->size; i++)
1686      if (m->levels[(clearned->space[i])>>1] > m->levels[(clearned->space[maxI])>>1])
1687        maxI = i;
1688    lit = clearned->space[maxI];
1689    clearned->space[maxI] = clearned->space[1];
1690    clearned->space[1] = lit;
1691
1692    /** Subsumption check in conflict analysis **/
1693    if (!isNotDecision && !resolvent)
1694      resolvent = traversed;
1695
1696    if (resolvent > 0) {
1697      resolvent->size |= SATCIrredundant;
1698      if (SATSizeClause(resolvent) > clearned->size) {
1699        sat_delete_watched_literal(m, resolvent);
1700        abstract = 0;
1701        for (i = 0; i < clearned->size; i++) {
1702          lit = clearned->space[i];
1703          resolvent->lits[i] =lit;
1704          abstract |= 1 << (SATVar(lit) & 31);
1705        }
1706        resolvent->size = (clearned->size << SATCsizeShift) | (resolvent->size & SATCMask);
1707        sat_add_watched_literal(m, resolvent);
1708        if (SATClauseVisited(resolvent))
1709          resolvent->info.abstract = abstract;
1710      }
1711      m->nOmittedConflictClauses++;
1712      m->nOmittedConflictLits += m->clearned->size;
1713    }
1714  }
1715  cclearned = m->cclearned;
1716  for (j = 0; j < cclearned->size; j++) 
1717    m->marks[(cclearned->space[j]>>1)] = 0; 
1718
1719  /* check backward subsumption before adding a new clause */
1720
1721  m->clearned = clearned;
1722  m->cclearned = cclearned;
1723 
1724#if 0 
1725  traversed = sat_DFS_to_get_clause_reference(m, t, 1);
1726  traversed->size |= SATCIrredundant;
1727
1728  elimnable = 1;
1729  csize = SATSizeClause(traversed);
1730  if ((csize -1) >= clearned->size) {
1731    for (i = 1; i < csize; i++) {
1732      ante = m->antes[(traversed->lits[i])>>1];
1733      if (ante != 0) {
1734        elimnable = 0;
1735        ante->size |= SATCIrredundant;
1736      }
1737    }
1738  }
1739  else {
1740    elimnable = 0;
1741  }
1742
1743#endif
1744  if (!isNotDecision) {
1745    if (resolvent == 0) {
1746      c = sat_add_distilled_clause(m, clearned, learned);
1747      c->size |= SATCIrredundant;
1748    }
1749
1750#if 0 
1751    sat_delete_watched_literal(m, traversed);
1752    abstract = 0;
1753    for (i = 0; i < clearned->size; i++) {
1754      lit = clearned->space[i];
1755      traversed->lits[i] = lit;
1756      abstract |= 1 << (SATVar(lit) & 31);
1757    }
1758    flags = traversed->size & SATCMask;
1759    traversed->size = (clearned->size << SATCsizeShift) | flags;
1760    traversed->info.abstract = abstract;
1761    sat_add_watched_literal(m, traversed);
1762#endif
1763  }
1764  else { 
1765#if 1
1766    if (!subsumptionCheck || !resolvent) {
1767      limit = m->clauses->size <= 150000 ? (long)(clearned->size * 1.1) : 4 ; 
1768      if (clearned->size <= limit) { 
1769        /** Add the first learned clause
1770         *  which must be set as irredundant.
1771         **/
1772        c = sat_add_distilled_clause(m, clearned, 1);
1773        c->size |= SATCIrredundant; 
1774        m->nLearnedClInDistill++;
1775        m->nLearnedLitInDistill += SATSizeClause(c);
1776      }
1777    }
1778#endif
1779
1780#if 1
1781    for (i = 0; i < clearned->size; i++) {
1782      lit = clearned->space[i];
1783      v = lit >> 1;
1784      if (m->levels[v] < SATCurLevel(m)) 
1785        m->marks[v] = 1;
1786    }
1787    sat_conflict_analysis_on_decisions(m, clearned, traversed, learned);
1788#endif
1789  }
1790  sat_ternary_tree_based_undo(m, SATCurLevel(m)-1);
1791 
1792  return(bLevel);
1793}
1794
1795void
1796sat_conflict_analysis_on_decisions(satManager_t *m, satArray_t *clearned, satClause_t *traversed, long learned) 
1797{
1798int value, maxI1, maxI2, flags;
1799long i, j, k, csize, abstract;
1800long lit, v, tv, tlit;
1801satClause_t *c, *ante;
1802satArray_t *cclearned, *decisions, *redundant;
1803
1804  cclearned = m->cclearned;
1805  cclearned->size = 0;
1806  decisions = m->temp;
1807  decisions->size = 0;
1808  redundant = m->redundant;
1809  redundant->size = 0;
1810
1811  /** traverse implication graph in reverse to replace the literals
1812   *  of the conflict clause with their decisions from which they
1813   *  are implied.
1814   **/
1815#if 0 
1816    fprintf(stdout, "**********************************\n");
1817    fprintf(stdout, "* Conflict analysis on decisions *\n");
1818    fprintf(stdout, "**********************************\n");
1819#endif
1820
1821  m->cclearned = cclearned = sat_array_copy(clearned, m->cclearned); 
1822  for (i=j=0; i < clearned->size; i++) {
1823    lit = clearned->space[i];
1824    v = lit >> 1;
1825    ante = m->antes[v];
1826
1827#if 0 
1828    fprintf(stdout, "Lit %c%ld%c@%d\n", lit&1 ? '-':' ', v, ante == 0 ? '*' : ' ', (int)m->levels[v]);
1829#endif
1830
1831    if (ante != 0) {
1832      /* traverse back upto decisions on which
1833       * the variable is implicated */
1834      redundant = sat_array_insert(redundant, lit);
1835      while (redundant->size > 0) {
1836        redundant->size--;
1837        c = m->antes[(redundant->space[redundant->size])>>1];
1838        csize = SATSizeClause(c);
1839        for (k = 0; k < csize; k++) {
1840          tlit = c->lits[k];
1841          tv = tlit >> 1;
1842          if (!m->marks[tv] && m->levels[tv] > 0) {
1843            m->marks[tv] = 1;
1844            if (m->antes[tv] != 0) {
1845              redundant = sat_array_insert(redundant, tlit); 
1846            }
1847            else {
1848              /* reached a decision */
1849              decisions = sat_array_insert(decisions, tv); 
1850            }
1851            cclearned = sat_array_insert(cclearned, tlit);
1852          }
1853        }
1854      }
1855    }
1856    else {
1857      clearned->space[j++] = lit;
1858    }
1859  } 
1860  clearned->size -= (i-j);
1861
1862  /** add decisions into the conflict clause, then update
1863   *  watched literals
1864   **/
1865#if 1
1866  for (i = 0; i < decisions->size; i++) {
1867    v = decisions->space[i];
1868    value = m->values[v];
1869    clearned = sat_array_insert(clearned, (v<<1)|value);
1870  }
1871
1872  maxI1 = 0;
1873  for (i = 0; i < clearned->size; i++) {
1874    lit = clearned->space[i];
1875    if (m->levels[(lit>>1)] > m->levels[(clearned->space[maxI1]>>1)]) 
1876        maxI1 = i;
1877  }
1878  lit = clearned->space[maxI1];
1879  clearned->space[maxI1] = clearned->space[0];
1880  clearned->space[0] = lit;
1881
1882  maxI2 = 1;
1883  for (i = 2; i < clearned->size; i++) {
1884    lit = clearned->space[i];
1885    if (m->levels[lit>>1] > m->levels[clearned->space[maxI2]>>1]) 
1886        maxI2 = i;
1887  }
1888  lit = clearned->space[maxI2];
1889  clearned->space[maxI2] = clearned->space[1];
1890  clearned->space[1] = lit;
1891
1892  if (traversed == 0) {
1893    c = sat_add_distilled_clause(m, clearned, learned);
1894    c->size |= SATCIrredundant;
1895  }
1896  else {
1897    sat_delete_watched_literal(m, traversed);
1898    abstract = 0;
1899    for (i = 0; i < clearned->size; i++) {
1900      lit = clearned->space[i];
1901      traversed->lits[i] = lit;
1902      abstract |= 1 << (SATVar(lit) & 31);
1903    }
1904    sat_add_watched_literal(m, traversed);
1905    traversed->size |= SATCIrredundant;
1906    flags = traversed->size & SATCMask;
1907    traversed->size = (clearned->size << SATCsizeShift) | flags;
1908    if (learned)
1909      traversed->info.abstract = abstract;
1910  }
1911#endif
1912
1913  for (i = 0; i < cclearned->size; i++) 
1914    m->marks[cclearned->space[i]>>1] = 0;
1915
1916  m->clearned = clearned;
1917  m->cclearned = cclearned;
1918  m->temp = decisions;
1919  m->redundant = redundant;
1920}
1921
1922/*---------------------------------------------------------------------------*/
1923/* Definition of internal functions                                          */
1924/*---------------------------------------------------------------------------*/
1925
1926/**Function********************************************************************
1927
1928  Synopsis    [ Recompute the variables score ]
1929
1930  Description [ Recompute variables score after resetting current scores.
1931                As a default and basic scoring scheme, it counts variables
1932                occurrencies in the CNF clauses. It may be extended with
1933                various scoring schemes. ]
1934
1935  SideEffects [ All clauses found satisfied are eliminated from clause
1936                databased. ]
1937
1938  SeeAlso     [ ]
1939
1940******************************************************************************/
1941int 
1942sat_recompute_var_score(satManager_t *m)
1943{
1944int limit;
1945long i, j, nVars, csize, cflags, lit;
1946long nCl, nLit, nSATCl;
1947char value; 
1948satArray_t *clauses, *arr;
1949satClause_t *c;
1950
1951  arr = sat_array_alloc(16);
1952 
1953  limit = (m->clausesHistogram[m->majorityClauseLength] + m->clausesHistogram[m->majorityClauseLength+1] >= 500000) ? 1 : 0;
1954
1955  /** Reset the current scores of variables **/ 
1956  nVars = m->nVars+1;;
1957  if (m->nDistill > 0) 
1958    memset(m->scores, 0, sizeof(long)*(nVars<<1)); 
1959
1960  nCl = nLit = nSATCl = 0;
1961  /** Counting up the occurrencies of
1962   *  each literal in satisfiable clause.
1963   *  1) For the original clauses
1964   **/
1965  clauses = m->clauses;
1966  for (i=0; i<clauses->size; i++) {
1967    c = (satClause_t *)clauses->space[i];
1968    if (c == 0) continue;
1969 
1970    arr->size = 0;
1971    csize = SATSizeClause(c); 
1972    if (csize > 0) {
1973      if (csize == 1) {
1974        clauses->space[i] = clauses->space[--(clauses->size)];
1975        i--;
1976        continue;
1977      }
1978      else {
1979        if ((limit && csize >= 8) || (limit && csize <= 10 && m->clausesHistogram[csize] > 10000))
1980          c->size |= SATCIrredundant;
1981        else {
1982          for (j=0; j<csize; j++) {
1983            lit = c->lits[j];
1984            if (lit == 0) continue;
1985
1986            value = m->values[lit>>1];
1987            if (value == 2) 
1988              arr = sat_array_insert(arr, lit); 
1989            else if ((value ^ (lit&1)) == 1) { 
1990              /* The clause is satisfied */
1991              clauses->space[i] = clauses->space[--(clauses->size)];
1992              sat_delete_clause(m, c); 
1993              arr->size = 0;
1994              nSATCl++; 
1995              i--;
1996              goto metSATOrgCl;
1997            } 
1998            else {
1999              /* eliminate an false literal */
2000              c->lits[j] = c->lits[--csize]; 
2001              j--;
2002            }
2003          }
2004          /* update the size of clause */
2005          cflags = c->size & SATCMask;
2006          c->size = (csize << SATCsizeShift) | cflags;
2007        }
2008        for (j=0; j<arr->size; j++) {
2009          lit = arr->space[j];
2010          m->scores[lit]++;
2011        }
2012        nCl++; 
2013        nLit += SATSizeClause(c); 
2014      }
2015    } 
2016metSATOrgCl:;
2017  }
2018  if (m->nDistill == 0) {
2019    m->nInClForDistill = nCl;
2020    m->nInLitForDistill = nLit;
2021  }
2022
2023  /**  2) For the learned clauses
2024   **/
2025  nCl = nLit = 0;
2026  clauses = m->learned;
2027  for (i=0; i<clauses->size; i++) {
2028    c = (satClause_t *)clauses->space[i];
2029    if (c == 0) continue;
2030
2031    arr->size = 0;
2032    csize = SATSizeClause(c);
2033    if (csize > 0) {
2034      if (csize == 1) {
2035        clauses->space[i] = clauses->space[--clauses->size];
2036        i--;
2037      }
2038      else {
2039        if ((limit && csize >= 8) || (limit && csize <= 10 && m->clausesHistogram[csize] > 10000)) 
2040          c->size |= SATCIrredundant;
2041        else {
2042          for (j=0; j<csize; j++) {
2043            lit = c->lits[j];
2044            if (lit == 0) continue;
2045
2046            lit = c->lits[j];
2047            value = m->values[lit>>1];
2048            if (value == 2) 
2049              arr = sat_array_insert(arr, lit); 
2050            else if ((value ^ (lit&1)) == 1) { 
2051              /* The clause is satisfied */
2052              clauses->space[i] = clauses->space[--(clauses->size)];
2053              sat_delete_clause(m, c); 
2054              arr->size = 0;
2055              nSATCl++; 
2056              i--;
2057              goto metSATLearnedCl;
2058            }
2059            else {
2060              /* eliminate an false literal */
2061              assert(j > 1);
2062              c->lits[j] = c->lits[--csize]; 
2063              j--;
2064            }
2065          }
2066          /* update the size of clause */
2067          cflags = c->size & SATCMask;
2068          c->size = (csize << SATCsizeShift) | cflags;
2069
2070          for (j=0; j<arr->size; j++) {
2071            lit = arr->space[j];
2072            m->scores[lit]++;
2073          }
2074        }
2075        nCl++; 
2076        nLit += SATSizeClause(c); 
2077      }
2078    }
2079metSATLearnedCl:;
2080  }
2081  if (m->nDistill == 0) {
2082    m->nInLearnedClForDistill = nCl;
2083    m->nInLearnedLitForDistill = nLit;
2084  }
2085  m->nSATCl = nSATCl;
2086
2087  arr->size = 0;
2088  free(arr);
2089
2090  /** All of clauses are satisfied **/
2091  if (m->nInClForDistill==0 && nCl==0) {
2092    fprintf(stdout, "All clauses are satisfied at level zero!\n");
2093    return 0;
2094  }
2095  return 1;
2096}
2097
2098/**Function********************************************************************
2099
2100  Synopsis    [ Print dot file of Ternary Search Tree ]
2101 
2102  Description [ Print dot file of Ternary Search Tree ]
2103 
2104  SideEffects [ ]
2105
2106  SeeAlso     []
2107
2108******************************************************************************/
2109void 
2110sat_print_dot_for_ternary_search_tree(
2111        satManager_t *m, 
2112        satTernary_t *root,
2113        long num)
2114{
2115char name[1024];
2116long nNode;
2117FILE *fp;
2118
2119  if (root == 0) return;
2120 
2121  fprintf(stdout, " >>>> Dot file for Ternary Search Tree is printed! <<<<\n");
2122  sprintf(name, "%s_%s_%d.dot", m->cnfFileName, "ternary", (int)num);
2123  fp = fopen(name, "w");
2124
2125  fprintf(fp, "digraph \"TernaryGraph\" {\n");
2126  fprintf(fp, "  margin=0.5;\n label=\"Trie\";\n");
2127  fprintf(fp, "  page=\"8.5,11\" size=\"7.5,10\";\n ratio=\"auto\" center=\"true\";\n");
2128  //fprintf(fp, "  nNode [shape=box];\n");
2129  nNode = 1;
2130  fprintf(fp, "  %ld.%ld [label=\"%ld\"];\n", root->id, nNode, root->id);
2131  sat_traverse_ternary_tree_to_print_out_dot(m, fp, root, &nNode); 
2132  fprintf(fp, "}\n");
2133  fclose(fp);
2134}
2135
2136/**Function********************************************************************
2137
2138  Synopsis    [ Traverse Ternary Search Tree to print dot file ]
2139
2140  Description [ Traverse Ternary Search Tree to print dot file ]
2141
2142  SideEffects [ order :
2143                        0 - lower kid
2144                        1 - equal kid
2145                        2 - higher kid ]
2146
2147  SeeAlso     []
2148
2149******************************************************************************/
2150void
2151sat_traverse_ternary_tree_to_print_out_dot(
2152        satManager_t *m,
2153        FILE *fp,
2154        satTernary_t *ternary,
2155        long *nNode)
2156{
2157long index;
2158long v, tv;
2159satTernary_t *child;
2160
2161  v = ternary->id;
2162  index = *nNode;
2163 
2164  /** Visit children with printing those nodes out **/
2165  if (ternary->lokid) {
2166    (*nNode)++;
2167    child = ternary->lokid;
2168    tv = child->id;
2169    fprintf(fp, "  %ld.%ld [label=\"%ld\"];\n", tv, *nNode, tv);
2170    fprintf(fp, "  %ld.%ld -> %ld.%ld ", v, index, tv, *nNode); 
2171    fprintf(fp, "  [color=red];\n");
2172    sat_traverse_ternary_tree_to_print_out_dot(m, fp, child, nNode);
2173  }
2174  if (ternary->id > 0) {
2175    if (ternary->eqleaf.eqkid[0]) {
2176      (*nNode)++;
2177      child = ternary->eqleaf.eqkid[0];
2178      tv = child->id;
2179      if (tv == 0) {
2180        fprintf(fp, "  %ld.%ld [shape=box, peripheries=2, label=\"%ld\"];\n", tv, *nNode, (long)((child->eqleaf.c - (satClause_t*)(m->clauses->space[0]))/sizeof(long))+1); 
2181        fprintf(fp, "  %ld.%ld -> %ld.%ld ", v, index, tv, *nNode);
2182        fprintf(fp, "  [style=dotted, label=\"0\"];\n");
2183      }
2184      else {
2185        fprintf(fp, "  %ld.%ld [label=\"%ld\"];\n", tv, *nNode, tv);
2186        fprintf(fp, "  %ld.%ld -> %ld.%ld ", v, index, tv, *nNode);
2187        fprintf(fp, "  [style=dotted, label=\"0\"];\n");
2188        sat_traverse_ternary_tree_to_print_out_dot(m, fp, child, nNode);
2189      }
2190    }
2191    if (ternary->eqleaf.eqkid[1]) {
2192      (*nNode)++;
2193      child = ternary->eqleaf.eqkid[1];
2194      tv = child->id;
2195      if (tv == 0) {
2196        fprintf(fp, "  %ld.%ld [shape=box, peripheries=2, label=\"%ld\"];\n", tv, *nNode, (long)((child->eqleaf.c - (satClause_t*)m->clauses->space[0])/sizeof(long))+1); 
2197        fprintf(fp, "  %ld.%ld -> %ld.%ld ", v, index, tv, *nNode);
2198        fprintf(fp, "  [style=dotted, label=\"1\"];\n");
2199      }
2200      else {
2201        fprintf(fp, "  %ld.%ld [label=\"%ld\"];\n", tv, *nNode, tv);
2202        fprintf(fp, "  %ld.%ld -> %ld.%ld ", v, index, tv, *nNode);
2203        fprintf(fp, "  [style=dotted, label=\"1\"];\n");
2204        sat_traverse_ternary_tree_to_print_out_dot(m, fp, child, nNode);
2205      } 
2206    }
2207  }
2208  if (ternary->hikid) {
2209    (*nNode)++;
2210    child = ternary->hikid;
2211    tv = child->id;
2212    fprintf(fp, "  %ld.%ld [label=\"%ld\"];\n", tv, *nNode, tv);
2213    fprintf(fp, "  %ld.%ld -> %ld.%ld ", v, index, tv, *nNode);
2214    fprintf(fp, "  [color=blue];\n");
2215    sat_traverse_ternary_tree_to_print_out_dot(m, fp, child, nNode);
2216  }
2217}
2218
2219/**Function********************************************************************
2220
2221  Synopsis    [ Print an assignment stack ]
2222
2223  Description [ Print an assignment stack ]
2224
2225  SideEffects [ ]
2226
2227  SeeAlso     [ ]
2228
2229******************************************************************************/
2230void
2231sat_print_scores(satManager_t *m) 
2232{
2233long i, lit;
2234
2235  fprintf(stdout, "------------Print Scores-----------\n");
2236  fprintf(stdout, "%5s : %3s %3s\n", "VAR", "+", "-");
2237  for (i=0; i<=m->nVars; i++) {
2238    lit = i<<1;
2239    fprintf(stdout, "%5d : %3d %3d\n", (int)i, (int)m->scores[lit], (int)m->scores[lit|1]); 
2240  }
2241}
2242
2243/**Function********************************************************************
2244
2245  Synopsis    [ Assert pure literals ]
2246
2247  Description [ Assert pure literals ]
2248
2249  SideEffects [ ]
2250
2251  SeeAlso     [ ]
2252
2253******************************************************************************/
2254void 
2255sat_assert_pure_literals(satManager_t *m)
2256{
2257long i, v;
2258char value;
2259
2260  for (i=0; i<=m->nVars; i++) {
2261    v = i;
2262    value = m->values[v];
2263
2264    if (value != 2) continue;
2265
2266    if(m->pure[i] == 1) 
2267      sat_enqueue_check(m, i<<1, 0);
2268    else if(m->pure[i] == 2) 
2269      sat_enqueue_check(m, (i<<1)+1, 0);
2270  }
2271
2272} 
2273
2274/**Function********************************************************************
2275
2276  Synopsis    [ Add a conflit clause generated during distillation ]
2277
2278  Description [ Add a conflit clause generated during distillation ]
2279
2280  SideEffects [ ]
2281
2282  SeeAlso     [ ]
2283
2284******************************************************************************/
2285satClause_t *
2286sat_add_distilled_clause(satManager_t *m, satArray_t *arr, long learned)
2287{
2288long lit;
2289satClause_t *c;
2290
2291  if(arr->size == 1) {
2292    lit = arr->space[0];
2293    c = sat_new_clause(arr, 0);
2294    if (learned) {
2295      m->learned = sat_array_insert(m->learned, (long)c);
2296      c->size |= SATCLearned; 
2297    }
2298    else 
2299      m->clauses = sat_array_insert(m->clauses, (long)c);
2300    sat_enqueue(m, lit, c);
2301  }
2302  else {
2303    c = sat_new_clause(arr, learned);
2304    if (learned) {
2305      m->learned = sat_array_insert(m->learned, (long)c);
2306    }
2307    else
2308      m->clauses = sat_array_insert(m->clauses, (long)c);
2309    sat_add_watched_literal(m, c);
2310  }
2311
2312  /*if (learned) {
2313    m->nCurLearnedLits += arr->size;
2314    m->nCurLearnedClauses++;
2315    m->nTotalLearnedLits += arr->size;
2316    m->nTotalLearnedClauses++;
2317  }*/
2318  return(c);
2319}
2320
2321/**Function********************************************************************
2322
2323  Synopsis    [ Delete the clauses unmarked in distilling ]
2324
2325  Description [ Delete the clauses unmarked in distilling ]
2326
2327  SideEffects [ Satisfied clauses are also deleted. ]
2328
2329  SeeAlso     [ ]
2330
2331******************************************************************************/
2332void
2333sat_delete_unmakred_clauses_for_simplification(satManager_t *m)
2334{
2335int compactness, callVarelim;
2336long i, j, nLit;
2337long csize, lit;
2338satArray_t *arr;
2339satClause_t *c;
2340
2341  callVarelim = (m->elimTime < 5.0) ? 1 : 0;
2342  /** reset watched literals **/
2343  for (i=1; i<=m->nVars; i++) {
2344    lit = i << 1;
2345    if (m->values[i] <= 2) { 
2346      m->scores[lit] = 0;
2347      m->scores[lit|1] = 0;
2348      if (m->wls[lit|1])  m->wls[lit|1]->size = 0;
2349      if (m->wls[lit])    m->wls[lit]->size = 0;
2350    }
2351  } 
2352
2353  arr = m->clauses;
2354  nLit = 0;
2355  for (i=j=0; i<arr->size; i++) {
2356    c = (satClause_t *)arr->space[i];
2357    csize = SATSizeClause(c); 
2358    if (csize == 1) {
2359      arr->space[j++] = arr->space[i];
2360      sat_update_clauses_statistics(m, c);
2361      continue;
2362    }
2363   
2364    if (!SATClauseIrredundant(c)) {
2365      if(c->dependent)
2366        free(c->dependent);
2367      free(c);
2368    }
2369    else {
2370      c->size -= SATCIrredundant;
2371      compactness = sat_squeeze_clause(m, c); 
2372      sat_update_clauses_statistics(m, c);
2373      if (compactness == 0) {
2374        if (c->dependent)
2375          free(c->dependent);
2376        free(c);
2377      }
2378      else if (compactness == 1) {
2379        if (callVarelim == 1)
2380          sat_sort_clause_literal(c);
2381
2382        sat_add_watched_literal(m, c);
2383        arr->space[j++] = arr->space[i];
2384        nLit += csize; 
2385      }
2386    }
2387  }
2388  arr->size -= (i-j);
2389  m->nOutClForDistill = arr->size;
2390  m->nOutLitForDistill = nLit;
2391
2392  arr = m->learned;
2393  nLit = 0; 
2394  for (i=j=0; i<arr->size; i++) {
2395    c = (satClause_t *)arr->space[i];
2396    csize = SATSizeClause(c);
2397
2398    if (csize == 1) {
2399      arr->space[j++] = arr->space[i];
2400      sat_update_clauses_statistics(m, c);
2401      continue;
2402    }
2403
2404    if (!SATClauseIrredundant(c)) {
2405      if(c->dependent)
2406        free(c->dependent);
2407      free(c);
2408    }
2409    else {
2410      c->size -= SATCIrredundant;
2411      compactness = sat_squeeze_clause(m, c); 
2412      if (compactness == 0) {
2413        if(c->dependent)
2414          free(c->dependent);
2415        free(c);
2416      }
2417      else if (compactness == 1) {
2418        if (callVarelim == 1) 
2419          sat_sort_clause_literal(c);
2420
2421        sat_add_watched_literal(m, c);
2422        arr->space[j++] = arr->space[i];
2423        nLit += csize; 
2424      }
2425    }
2426  }
2427  arr->size -= (i-j);
2428  m->nOutLearnedClForDistill += arr->size;
2429  m->nOutLearnedLitForDistill += nLit;
2430}
2431
2432/******************************************************************************
2433 *
2434 * Utilities
2435 *
2436*******************************************************************************/
2437void 
2438sat_report_result_for_distillation(satManager_t *m) 
2439{
2440  if (m== 0) return;
2441
2442  fprintf(stdout, "===========================[ %s Statistics ]==============================\n",
2443  (m->nDistill == 0) ? "Alembic" : "PAL");
2444
2445  fprintf(stdout, "Distilled origianl clauses    : %ld out of %ld\n", m->nInClForDistill - m->nOutClForDistill, m->nInClForDistill); 
2446  fprintf(stdout, "Distilled origianl literals   : %ld out of %ld\n", m->nInLitForDistill - m->nOutLitForDistill, m->nInLitForDistill); 
2447  fprintf(stdout, "Distilled learned clauses     : %ld out of %ld\n", m->nInLearnedClForDistill - m->nOutLearnedClForDistill, m->nInLearnedClForDistill); 
2448  fprintf(stdout, "Distilled learned literals    : %ld out of %ld\n", m->nInLearnedLitForDistill - m->nOutLearnedLitForDistill, m->nInLearnedLitForDistill); 
2449  fprintf(stdout, "Added clauses in distillation : %ld\n", m->nLearnedClInDistill);
2450  fprintf(stdout, "Added units in distillation   : %ld\n", m->nLearnedUnitClInDistill);
2451  fprintf(stdout, "Added literals in distillation: %ld\n", m->nLearnedLitInDistill);
2452  fprintf(stdout, "Conflicts in distillation     : %ld\n", m->nLearnedInDistill);
2453  fprintf(stdout, "Implied in distillation       : %ld\n", m->nResolvedInDistill);
2454  fprintf(stdout, "Implications in distillation  : %0.f\n", m->nImplicationsInDistill); 
2455 
2456  if (m->subsumeInConflict) { 
2457    fprintf(stdout, "Number of continuous distill in Alembic: %ld\n", m->nDistillInConflict);
2458  }
2459
2460  if (m->nDistill == 0) 
2461    fprintf(stdout, "Distill time : %10g \n", m->distillTime);
2462  fprintf(stdout, "\n");
2463}
2464
2465
2466/**Function********************************************************************
2467
2468  Synopsis    [ Free ternary search tree structure ]
2469
2470  Description [ Free ternary search tree structure ]
2471
2472  SideEffects [ ]
2473
2474  SeeAlso     [ sat_BuildTrieForAlembic ]
2475
2476******************************************************************************/
2477void
2478sat_free_ternary(satTernary_t *ternary)
2479{
2480  if (ternary == 0)     return;
2481
2482  sat_free_ternary(ternary->lokid);
2483 
2484  if (ternary->id > 0) {
2485    sat_free_ternary(ternary->eqleaf.eqkid[0]);
2486    sat_free_ternary(ternary->eqleaf.eqkid[1]);
2487  }
2488  else 
2489    ternary->eqleaf.c = 0;
2490 
2491  sat_free_ternary(ternary->hikid);
2492
2493  free(ternary);
2494}
2495
2496
2497/**Function********************************************************************
2498
2499  Synopsis    [ Print clause array ]
2500
2501  Description [ Print clause array ]
2502
2503  SideEffects [ ]
2504
2505  SeeAlso     [ ]
2506
2507******************************************************************************/
2508void
2509sat_print_array_as_clause(satManager_t *m, satArray_t *arr)
2510{
2511long i, lit, v;
2512
2513  if (arr == 0) return;
2514
2515  fprintf(stdout, "Clause array ( ");
2516  for (i=0; i<arr->size; i++) {
2517    lit = arr->space[i];
2518    v = SATVar(lit);
2519    fprintf(stdout, "%s%ld@%ld%s", lit&1 ? "-":"", v, m->levels[v], 
2520                m->antes[v] != 0? " ":"* ");
2521  }
2522  fprintf(stdout, " )\n");
2523}
2524
Note: See TracBrowser for help on using the repository browser.