/**CFile***********************************************************************

  FileName    [sat_NewDistill.c]

  PackageName [sat]

  Synopsis    [ Routines for Distillation-based preprocessing ]

  Author      [Hyojung Han]

  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado

  All rights reserved.

  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions
  are met:

  Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

  Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

  Neither the name of the University of Colorado nor the names of its
  contributors may be used to endorse or promote products derived from
  this software without specific prior written permission.

  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  POSSIBILITY OF SUCH DAMAGE.]

******************************************************************************/
#include "sat.h"
#include "stdio.h"
#include "malloc.h"
#include "util.h"

/* #define NOBLOCKINGCL */
/* #define DEBUG */
/* #define TEST */

#define STATS
static char rcsid[] UNUSED = "$Id $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/
static void sat_sort_clause_array_by_length_aux(long *carr, long size);
/**AutomaticEnd***************************************************************/
/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [ Initialize options for distillation ] 

  Description [ Initialize options for distillation ]

  SideEffects [ This function allows external application to initialize
                the options of distillation. ]

  SeeAlso     [ sat_init_options_for_varelim, sat_init_options_for_distill]

******************************************************************************/
void
sat_init_options_for_distill(satManager_t *m) 
{

  if (m == 0) 
    fprintf(stderr, "ERROR : SAT manager is not initialized!\n");

  m->distill = 1;
  m->simplify = 1;
  m->nIteratePreprocess = 1; 

  /** set to 1 if periodic distillation
   *  is requested to be enabled.
   */
  m->periodicDistill = 0; 
}

/**Function********************************************************************

  Synopsis    [ Distill all the clauses ] 

  Description [ Distill all the clauses ]

  SideEffects [ ]

  SeeAlso     [ sat_distill_clauses ]

******************************************************************************/
void
sat_distill_clauses_with_preprocessing(satManager_t *m)
{
double btime;
  
  btime = (double)util_cpu_time();
  
  m->nInClForDistill = 0;
  m->nInLitForDistill = 0;
  m->nInLearnedClForDistill = 0; 
  m->nInLearnedLitForDistill = 0; 

  m->nLearnedClInDistill = 0;
  m->nLearnedLitInDistill = 0;
  m->ternary = 0;

  if (m->nCurClauseLits < 500000) {
    m->distillMin = 3; 
    m->distillMax = 15;
  }
  else if (m->nCurClauseLits >= 500000 && m->nCurClauseLits < 1000000){
    m->distillMin = 3;
    m->distillMax = 8;
  }
  else {
    m->distillMin = (m->minorityClauseLength < m->majorityClauseLength ? m->minorityClauseLength : m->majorityClauseLength);
    m->distillMin = (m->distillMin > 4 ? 4 : m->distillMin - 1);
    m->distillMax = (m->distillMin > 8 ? 8 : m->distillMin + 1);
  }
  
  sat_distill_clauses_array(m, m->clauses, 0);
  
  if (m->status == 2)
    sat_reshape_cnf_database_with_distilled_clauses(m, 1);
  else   return ;

  m->distillTime += ((double)util_cpu_time() - btime) / 1000.0;
  
  sat_report_result_for_distillation(m); 

  m->distill++;

  if (m->status != 2) 
    return;
}


/**Function********************************************************************

  Synopsis    [ Distill set of clauses ] 

  Description [ Distill set of clauses ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void 
sat_distill_clauses_array(satManager_t *m, satArray_t* clauses, long learned)
{

  sat_choose_candidates_for_distillation(m, clauses);

  if (m->status != 2)
    return ;

#ifdef STATS
  if (m->nDistill > 0 && learned)
    fprintf(stdout, "| %9s | %7ld %8ld %8ld | %8s %8ld %6.0f | %8s |\n",
          "DISTILL", m->variableHeap->size, 
  	  m->nInClForDistill, m->nInLitForDistill,  
	  "PERIOD", m->nInLearnedClForDistill, 
	  (double)m->nInLearnedLitForDistill/(double)m->nInLearnedClForDistill,
          "REDUCED");   	

#endif

  sat_build_ternary_tree(m, clauses);
  sat_ternary_tree_based_implication(m, m->ternary, 1, learned);
  sat_free_ternary(m->ternary);
  m->ternary = 0;
}

/** Choose candidates for distillation with squeezing set of clauses **/
void 
sat_choose_candidates_for_distillation(satManager_t *m, satArray_t* clauses)
{
long min, max;
long i, j, k, csize;
satClause_t *c;

  min = m->distillMin;
  max = m->distillMax;
  
  if (m->limitDistill && (clauses == m->learned)) {
    for (i = j = 0; i < m->preLearnedPos; i++) {
      c = (satClause_t*)clauses->space[i];

      if (sat_squeeze_clause(m, c)) {
        clauses->space[j++] = (long)c;
	c->size |= SATCIrredundant;
	csize = SATSizeClause(c);
        m->nInLearnedClForDistill++;  
	m->nInLearnedLitForDistill += csize;
      }
      else {
        c->size -= SATCVisited; /* was set by sat_squeeze_clause */  
      }
    } 
  }
  else {
    i = j = 0;
  }

  for ( ; i < clauses->size; i++) {
    c = (satClause_t*)clauses->space[i];

    if (sat_squeeze_clause(m, c)) {
      clauses->space[j++] = (long)c;
      csize = SATSizeClause(c);

      if (SATClauseLearned(c)) {
        m->nInLearnedClForDistill++;  
	m->nInLearnedLitForDistill += csize;
      }
      else {
	m->nInClForDistill++;  
	m->nInLitForDistill += csize;
      }
     
      /** filter clause with bound of size **/
      if ((csize >= min) && (csize <= max))  {
        for (k = 0; k < csize; k++) 
          m->scores[c->lits[k]]++;
      }
      else {
        c->size |= SATCIrredundant;  
      }
    }
    else 
      c->size -= SATCVisited; /* was set by sat_squeeze_clause */  
  }
  clauses->size -= (i-j);
}

void
sat_reshape_cnf_database_with_distilled_clauses(satManager_t *m, int checkSubsumption)
{
satQueue_t *subsumptionQueue;

  subsumptionQueue = m->satQueue;
  
  sat_squeeze_clauses_array(m, checkSubsumption);
  
  if (checkSubsumption) {
    sat_build_occurrence_list(m);
    while (subsumptionQueue->size > 0) {
      if (sat_backward_subsumption_check(m)) {
        sat_gather_touched_clauses(m);
	if (sat_implication_on_all_watched_literals(m)) {
          m->status = 0;
	  break;
	}
      }
      else break;
    }

    if (m->status == 2) {
      /*sat_init_clauses_statistics(m); */
      sat_reset_all_watched_lists(m);
      sat_recover_clauses_DB(m);
      sat_remove_marked_clauses(m, m->clauses); 
      sat_remove_marked_clauses(m, m->learned); 
      sat_assert_pure_literals(m);

      m->nOutClForDistill = m->clauses->size;
      m->nOutLitForDistill = m->nCurClauseLits; 
      m->nOutLearnedClForDistill = m->learned->size;
      m->nOutLearnedLitForDistill = m->nCurLearnedLits;
    }
  }

  sat_heap_remove_var_assigned_level_zero(m, m->variableHeap);
}

void 
sat_squeeze_clauses_array(satManager_t *m, int checkSubsumption)
{
long i, j, csize;
satClause_t *c;
satArray_t *clauses;

  sat_reset_all_watched_lists(m);
  /*sat_init_clauses_statistics(m);*/

  clauses = m->clauses;
  for (i = j = 0; i < clauses->size; i++) {
    c = (satClause_t*)clauses->space[i];
    csize = SATSizeClause(c);

    if (csize == 1) {
      if (SATClauseIrredundant(c))
        c->size -= SATCIrredundant;

      sat_update_clauses_statistics(m, c);
      clauses->space[j++] = (long)c;
      continue;
    }
   
    if (!SATClauseIrredundant(c) || !sat_squeeze_clause(m, c)) {
      sat_free_clause(c);
    }
    else {
      if (checkSubsumption)
        sat_sort_clause_literal(c);
      
      sat_add_watched_literal(m, c);
      sat_update_clauses_statistics(m, c);
      clauses->space[j++] = (long)c;
      c->size -= SATCIrredundant;
    }
  }
  clauses->size -= (i-j);

  clauses = m->learned;
  for (i = j = 0; i < clauses->size; i++) {
    c = (satClause_t*)clauses->space[i];
    csize = SATSizeClause(c);

    if (csize == 1) {
      if (SATClauseIrredundant(c)) 
        c->size -= SATCIrredundant;
  
      sat_update_clauses_statistics(m, c);
      clauses->space[j++] = (long)c;
      m->nCurLearnedLits++;
      continue;
    }
    
    if (!SATClauseIrredundant(c) || !sat_squeeze_clause(m, c)) {
      sat_free_clause(c);
    }
    else {
      /*if (SATClauseVisited(c)) 
	  c->size -= SATCVisited;
      else  { */
      
        if (checkSubsumption) 
          sat_sort_clause_literal(c);
      
        sat_add_watched_literal(m, c);
        /*sat_update_clauses_statistics(m, c);*/
        clauses->space[j++] = (long)c;
        c->size -= SATCIrredundant;
      /*} */
    }
  }
  clauses->size -= (i-j); 
}

void
sat_free_clause(satClause_t *c)
{
  if (c->dependent)
    free(c->dependent);
  free(c);
}


/**Function********************************************************************

  Synopsis    [ Shrink a clause ] 

  Description [ Shrink a clause 
                Only marked literals are removed if marked == 1, and
		only unmarked literals are removed otherwise.
	      ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_strengthen_clause_in_conflict_analysis(satManager_t *m, satClause_t *c, int marked)
{
long i, csize, index, maxI;
long lit, v, flags, abstract;
long pcsize;

  if (c == 0) return;

  index = 0;
  csize = SATSizeClause(c);
  pcsize = csize;

  if (m->marks[SATVar(c->lits[0])] == marked) {
    lit = c->lits[0];
    sat_array_delete_elem(m->wls[lit^1], (long)c);
    c->lits[0] = c->lits[1];
    if ((--csize) > 1) {
      c->lits[1] = c->lits[csize];
      index = 1;
    }
    else {
      lit = c->lits[0];
      sat_array_delete_elem(m->wls[lit^1], (long)c);
    }
  }
  else if (m->marks[SATVar(c->lits[1])] == marked) {
    lit = c->lits[1];
    sat_array_delete_elem(m->wls[lit^1], (long)c);
    c->lits[1] = c->lits[--csize];
    if (csize == 1) {
      lit = c->lits[0];
      sat_array_delete_elem(m->wls[lit^1], (long)c);
    }
    else
      index = 1;
  }
  else {
    for (i = 2; i < csize; i++) {
      lit = c->lits[i];
      v = lit >> 1;
      if (m->marks[v] == marked) {
        c->lits[i] = c->lits[--csize];
	break;
      }
    }
  } 
  
  if (index > 0) {
    maxI = 1;
    for (i = 2; i < csize; i++) {
      lit = c->lits[i];
      v = lit >> 1;
      if (m->levels[v] > m->levels[(c->lits[maxI]>>1)]) 
        maxI = i;
    }
    lit = c->lits[maxI];
    c->lits[maxI] = c->lits[1];
    c->lits[1] = lit;

    index = lit^1;
    m->wls[index] = sat_array_alloc_insert(m->wls[index], (long)c);  
  }

  if (!(SATClauseLearned(c) || SATClauseBlock(c))) {
    abstract = 0;
    for (i = 0; i < csize; i++) 
      abstract |= 1 << (SATVar(c->lits[i]) & 31);
    c->info.abstract = abstract;
  }
  flags = c->size & SATCMask;
  c->size = (csize << SATCsizeShift) | flags;
}


int sat_verify_watched_literal(satManager_t *m, satClause_t *c)
{
int found;
long lit, i;
satClause_t *ct;
satArray_t *wls;

  if (SATSizeClause(c) == 1)  return 0;
  
  found = 0;

  lit= (c->lits[0])^1; 
  wls = m->wls[lit];

  /** Verification of watched literals **/
  for (i = 0; i < wls->size; i++) {
    ct = (satClause_t*)wls->space[i];
    if (ct == c) {
      found = 1;
      break;
    }
  }
  if (found == 0) {
    fprintf(stdout, "ERROR : Missing 1-watched literal in CL(");
    sat_print_clause(m, c);
    fprintf(stdout, "\n");
    return 0;
  }

  if (SATSizeClause(c) > 1) {
    found = 0;
  
    lit= (c->lits[1])^1; 
    wls = m->wls[lit];

    /** Verification of watched literals **/
    for (i = 0; i < wls->size; i++) {
      ct = (satClause_t*)wls->space[i];
      if (ct == c) {
        found = 1;
        break;
      }
    }
    if (found == 0) {
      fprintf(stdout, "ERROR : Missing 2-watched literal!\n");
      return 0;
    }
  }

  return 1;
}

/**Function********************************************************************

  Synopsis    [ Strengthen set of clauses in conflict analysis ] 

  Description [ Strengthen set of clauses in conflict analysis ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_strengthen_set_of_clauses_in_conflict_analysis(satManager_t *m)
{
long i, v, csize;
satClause_t *c;
satArray_t *pivots, *arr;
satQueue_t *clauses_queue;

  pivots = m->resolvents;
  clauses_queue = m->satQueue;  

  i = 0;
  while (clauses_queue->size > 0) {
    c = (satClause_t*)sat_queue_pop(clauses_queue);
    v = pivots->space[i++];
 
    if (v > 0) {
      m->marks[v] = 1;
 
      sat_strengthen_clause_in_conflict_analysis(m, c, 1);
      m->marks[v] = 0;
    }
    else { 
      arr = SATClauseLearned(c) ? m->learned : (c->size & SATCTheory ?
		      m->theory : (SATClauseBlock(c) ? m->blocking :
			      m->clauses)); 
      
      csize = SATSizeClause(c);
      m->nCurClauseLits -= csize;
      m->nTotalClauseLits -= csize;
      
      sat_array_delete_elem(arr, (long)c);
      sat_delete_clause(m, c);
    }
  }
  pivots->size = 0;
}


/**Function********************************************************************

  Synopsis    [ Check if clause cp subsumes clause cq ]  

  Description [ Check if clause cp subsumes clause cq, such that cp and cq are 
                the clauses participating in conflict analysis
		
		Precondition : All literals in cp and cq are assigned.

                Return 1 if cp subsumes cq, 0 otherwise. ] 

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
int
sat_check_subsumption_in_conflict_analysis(satManager_t *m, satClause_t *cp, satClause_t *cq)
{
int subsume;
long i, j, cpsize, cqsize;
long litp, litq;

  cpsize = SATSizeClause(cp);
  cqsize = SATSizeClause(cq);

  subsume = 0;
  for (i = 0; i < cpsize; i++) {
    subsume = 0;
    litp = cp->lits[i];
    if (m->levels[litp>>1] == 0)  continue;

    for (j = 0; j < cqsize; j++) {
      litq = cq->lits[j];
      if (m->levels[litq>>1] == 0)  continue;
      if (litp == litq) {
        subsume = 1;
	break;
      }	
    }
  }  
  
  return (subsume);
}


int 
sat_check_subsumption_resolvent_and_clause(satManager_t *m, satClause_t *c, long nMarks)
{
long i, csize;
long lit;

  csize = SATSizeClause(c);
  for (i = 0; i < csize; i++) {
    lit = c->lits[i];
    if (m->levels[lit>>1] == 0)  continue;
    if (m->marks[lit>>1]) nMarks--;
  }

  if (nMarks > 0) return 0;

  return 1;
}

/**Function********************************************************************

  Synopsis    [ Apply distillation method to simplify clauses ] 

  Description [ Apply distillation method to simplify clauses ]

  SideEffects [ Doing sat_heap_remove_var_assigned_level_zero() 
                after distillation to remove variables assigned
		at level zero ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_distill_clauses(satManager_t *m)
{
int nIterate; 
double btime, mtime;
satClause_t *conflicting;

#if 1
  if ((m->clauses->size > 4000000) || ((m->nCurClauseLits > 10000000))) {
    sat_report_result_for_distillation(m); 
    return;
  }
#endif 

  btime = (double)util_cpu_time();
  
  nIterate = 1; 
  m->nLearnedClInDistill = 0;
  m->nLearnedLitInDistill = 0;

beginDistill: 
  nIterate--; 
  conflicting = sat_implication(m);
  if(conflicting) {
    m->status = 0;
    return;
  }

  /** In recomputing variable scores, 
   *  pure literals generated due to
   *  unit propagations at preprocessing.
   *  If no clause is unsatisfied, 
   *  sat_recompute_var_score returns
   *  FALSE and the solver turns out 
   *  the problem is SATISFIABLE.  
   **/
  if (!sat_recompute_var_score(m)) {
    m->status = 1;	
    memset(m->scores, 0, sizeof(long)*((m->nVars+1)<<1));  
    sat_report_result_for_distillation(m); 
    return;
  }
  sat_build_ternary_tree(m, m->clauses);

  /** Apply distillation procedure on the trie built **/
  sat_ternary_tree_based_implication(m, m->ternary, 1, 0);
  m->nDistill++;
  
  if (m->status != 2) {
    m->distillTime = ((double)util_cpu_time() - btime) / 1000.0;
    sat_report_result_for_distillation(m); 
    return;
  } 
  
  /*sat_assert_pure_literals(m);
  conflicting = sat_implication(m);*/
  /** Assertion :
      1. Current level is zero.
      2. No pure literal causes conflict.
  **/
  sat_init_clauses_statistics(m);
  sat_delete_unmakred_clauses_for_simplification(m);
  sat_print_clauses_histogram(m);
  sat_free_ternary(m->ternary);

  mtime = m->elimTime;
#if 1 
  if (m->status == 2) {
    if (mtime < 5.0) {
      m->nIteratePreprocess = 0;
      sat_build_occurrence_list(m);
      while (m->satQueue->size > 0) { 
        if (sat_backward_subsumption_check(m)) {
          sat_gather_touched_clauses(m);
          conflicting = sat_implication_on_all_watched_literals(m); 
	  if (conflicting) {
	    m->status = 0;
            break;
	  }  
        }
        else break;
      }

      if (m->status == 2) {
        sat_init_clauses_statistics(m);
        sat_reset_all_watched_lists(m);
        sat_recover_clauses_DB(m);
        sat_remove_marked_clauses(m, m->clauses); 
        sat_remove_marked_clauses(m, m->learned); 
        sat_assert_pure_literals(m);
      } 
    }
  } 
#endif 

  m->distillTime = ((double)util_cpu_time() - btime) / 1000.0;
  
  if ((m->status == 2) && (nIterate > 0))  
    goto beginDistill; 
  
  sat_report_result_for_distillation(m); 
}

/**Function********************************************************************

  Synopsis    [ Builds the trie structure of CNF clauses. ]

  Description [ Builds the trie structure of CNF clauses. ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_build_ternary_tree(satManager_t *m, satArray_t *clauses)
{
long range, count;
long i, j, csize;
long v, lit;
satArray_t *clauseArray;
satTernary_t *root;
satClause_t *c;

  /** Build a ternary search tree(TST)
   *  first, which the procedure will 
   *  traverse to generate the trie trees 
   *  for the clause data base.
   *  ------------------------------------
   *  REVISION. Trie structure is not 
   *  required any more. Rather, TST will 
   *  be used to represnt all the clauses 
   *  for distillation.
   *  -----------------------------------
   **/

  if (m->ternary == 0) {
    root = (satTernary_t *)malloc(sizeof(satTernary_t));
    memset(root, 0, sizeof(satTernary_t));
    m->ternary = root;
  }
  else
    root = m->ternary;

  clauseArray = sat_array_alloc(4);
  
  range = clauses->size;  
  count = 0;
  /** Build a ternary searching tree(TST) 
   *  by scanning each clause. Since how 
   *  balanced TST is will affect time 
   *  consumption for traversing each node 
   *  in turn, clauses are randomly chosen
   *  in building TST.
   **/
  while (count < range) {
    i = (long)(sat_drand(m) * range);
    c = (satClause_t*)clauses->space[i];
    if (c == 0)	continue;

    /** Filter out duplicate clause 
     *  which has been scanned before.
     *  This can happen, because
     *  the random function may generate
     *  the same number several times
     *  within uniform distribution. 
     **/
    count++;

    if (SATClauseIrredundant(c))  continue;
    
    clauseArray->size = 0;
    if (!SATClauseVisited(c)) {
      c->size |= SATCVisited;

      /** Copy the array of literals of the clause 
       *  into the buffer used to do quick-sorting 
       **/
      csize = SATSizeClause(c);
      for (j=0; j<csize; j++) {
        lit = c->lits[j];
 	v = lit>>1;
	if (m->values[v] == 2) {
	  clauseArray = sat_array_insert(clauseArray, lit);
	}
      }
      if (clauseArray->size == 0)	continue; 
   
      clauseArray = sat_array_insert(clauseArray, -(long)c);
      sat_sort_literal_by_score(clauseArray, m->scores);
      if (root->id == 0) {
        root->id = clauseArray->space[0] >> 1;
      }
      sat_insert_ternary_tree(root, clauseArray);
    }
  }

  /** Second traverse clauses to complete TST 
   *  due to the clauses missed such that the
   *  indices of clauses are out of range of
   *  th random numbers generated.
   **/ 
   for (i=0; i < range; i++) {
    c = (satClause_t*)clauses->space[i];
    clauseArray->size = 0;
    if (c ==0) 	continue;

    if (SATClauseIrredundant(c)) continue;
 
    if (SATClauseVisited(c)) {
      c->size -= SATCVisited;
    }
    else {
      /** Copy the array of literals of the clause 
       *  into the buffer used to do quick-sorting 
       **/
      csize = SATSizeClause(c);
      for (j=0; j< csize; j++) {
        lit = c->lits[j];
 	v = lit>>1;
	if (m->values[v] == 2) {
	  clauseArray = sat_array_insert(clauseArray, lit);
	}
      }
      if (clauseArray->size == 0)	continue; 
      
      clauseArray = sat_array_insert(clauseArray, -((long)c));
      sat_sort_literal_by_score(clauseArray, m->scores);
      
      if (root->id == 0) {
        root->id = clauseArray->space[0] >> 1;
      }
      sat_insert_ternary_tree(root, clauseArray);
    }
  }

  m->ternary = root;
  free(clauseArray);
  
  if (m->ternary) { 
#ifdef DEBUG
    sat_print_dot_for_ternary_search_tree(m, root, 0);
#endif

    if (m->verbosity > 2)
      sat_print_scores(m);
  }
}

/**Function********************************************************************

  Synopsis    [ sort literals by the scores ]

  Description [ sort literals by the scores ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void 
sat_sort_literal_by_score(satArray_t *arr, long *scores)
{

  sat_sort_literal_by_score_aux(&(arr->space[0]), scores, arr->size-1);
}

void
sat_sort_literal_by_score_aux(long *lits, long *scores, long size)
{
long i, j, tmp, bi;
long pivot;

  /** TODO : We may need a tiebreaker in a way. **/
  if(size <=15) {
    for(i=0; i<size-1; i++) {
      bi = i;
      for(j=i+1; j<size; j++) {
	if(scores[lits[j]] > scores[lits[bi]])
	  bi = j;
      }
      tmp = lits[i];
      lits[i] = lits[bi];
      lits[bi] = tmp;
    }
  }
  else {
    pivot = scores[lits[size>>1]];
    i = -1;
    j = size;

    while(1) {
      do i++; while(scores[lits[i]] > pivot);
      do j--; while(pivot > scores[lits[j]]);
      if(i>=j)	break;
      tmp = lits[i];
      lits[i] = lits[j];
      lits[j] = tmp;
    }
    sat_sort_literal_aux(lits, i);
    sat_sort_literal_aux(&(lits[i]), size-i);
  }
}

/**Function********************************************************************

  Synopsis    [ Insert a literal to ternary tree for Alembic ]

  Description [ Insert a literal to ternary tree for Alembic
  		TST (Ternary Search Tree) ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_insert_ternary_tree(satTernary_t *root, satArray_t *clause)
{
int inverted;
long v, *plit, lit, i, size;
satTernary_t *ternary;

  ternary = root;
  plit = clause->space;
  size = clause->size;
  
  for (i=0; ;) {
    lit = *plit;
    v = lit >> 1;
    inverted = lit&1;
  
    if (ternary->id == 0)	return;

    /* Going down to ternary search tree */
    if (v < ternary->id) {
      if (ternary->lokid == 0) { 
        /* Creating a ternary node first */
        ternary->lokid = ALLOC(satTernary_t, 1);
        memset(ternary->lokid, 0, sizeof(satTernary_t));
        ternary = ternary->lokid;
        ternary->id = v;
      }
      else 
        ternary = ternary->lokid;
    }  
    else if (v == ternary->id) {
      ++plit; ++i;
      if (i >= size - 1) {
        /* create a new terminal node */
        if (ternary->eqleaf.eqkid[inverted] == 0) {
          ternary->eqleaf.eqkid[inverted] = ALLOC(satTernary_t, 1);
	  memset(ternary->eqleaf.eqkid[inverted], 0, sizeof(satTernary_t));
          ternary = ternary->eqleaf.eqkid[inverted];
          ternary->id = 0;
	  ternary->eqleaf.c = (satClause_t*)(-(*plit));
          
	  return;
	}
	/* cut an existing branch out 
	   with a new terminal node */
	ternary = ternary->eqleaf.eqkid[inverted];
	if (ternary->id > 0) {
          ternary->id = 0; 
	  sat_free_ternary(ternary->lokid);
	  ternary->lokid = 0;
          sat_free_ternary(ternary->eqleaf.eqkid[0]);
          sat_free_ternary(ternary->eqleaf.eqkid[1]);
	  ternary->eqleaf.eqkid[0] = ternary->eqleaf.eqkid[1] = 0;
          ternary->eqleaf.c = (satClause_t*)(-(*plit));
	  sat_free_ternary(ternary->hikid);
	  ternary->hikid = 0;
	  return;
	}
        /* meet an existing terminsal node, 
	   then forget to insert this clause */
	return;
      }
    
      if (ternary->eqleaf.eqkid[inverted]== 0) {
        ternary->eqleaf.eqkid[inverted]= ALLOC(satTernary_t, 1);
	memset(ternary->eqleaf.eqkid[inverted], 0, sizeof(satTernary_t));
	ternary = ternary->eqleaf.eqkid[inverted];
	ternary->id = (*plit) >> 1;
      }
      else
        ternary = ternary->eqleaf.eqkid[inverted];
    }
    else {
      if (ternary->hikid == 0) {
        /* Creating a ternary node first */
        ternary->hikid = ALLOC(satTernary_t, 1);
        memset(ternary->hikid, 0, sizeof(satTernary_t));
	ternary = ternary->hikid;
        ternary->id = v;
      }
      else
        ternary = ternary->hikid;
    }  
  }
}

/**Function********************************************************************

  Synopsis    [ Apply implication based on ternary tree ]

  Description [ Apply implication based on ternary tree 
  		
		Special DPLL procedure for distillation performs on the framework 
		of depth-first-search based on a ternary searching tree.
		For each ternary node, lokid, eqkid, and hikid are traversed in order. 
		For visiting lokid and hikid, nothing but invoking of the function 
		itself(sat_ternary_tree_ based _ implication()) is conducted. Making 
		a decision and implication are called, when it stays between them.
	     ]

  SideEffects [  Dependency between sat_ternary_based_back_track() and
                   sat_add_learned_clause()

                For the case of conflict, the failure driven assertion literal
                (FdalLit) is derived by conflict analysis, and it is enqueued
		to be asserted by the function sat_enqueue(), which is called
		when the computed conflict clause is added, i.e. sat_add_learned_clause(). 
		Enqueuing is performed only if the issued literal is unassigned, 
		and is skipped  otherwise. Hence, backtracking to undo the current 
		assignments must come before adding the conflict clause in conflict 
		analysis. 
	      ]

  SeeAlso     []

******************************************************************************/
void 
sat_ternary_tree_based_implication(
	satManager_t *m,
	satTernary_t *ternary, 
	int depth, 
	long learned)
{
long vid;
char value;
satTernary_t *child;
satClause_t *traversed, *conflicting;

  if (ternary == 0) 	return;
 
  /** traverse down to the path for lokid
      which must be in the same level as 
      the current node traversing, as if
      they are the nodes of trie-trees.. 
   **/
  if (m->status == 2 && ternary->lokid)
    sat_ternary_tree_based_implication(m, ternary->lokid, depth, learned);

DistillANode:
  /** perform distillation based implications
      for both eqkid0 and eqkid1.
    **/

  if (m->status != 2) return;
  vid = ternary->id;

  if (vid > 0) {
    value = m->values[vid];
    if (value < 2) {
      child = ternary->eqleaf.eqkid[!value];	
      /* current node is assigned either 
         0 or 1 already */
      if (m->levels[vid] >= 1 && child != 0) {
	m->nResolvedInDistill++;
	if (child) {
	  if (child->id == 0) {
            /* terminal node which stores a pointer 
	       to a clause currently traversing */
            traversed = (satClause_t*)child->eqleaf.c;
            traversed->size |= SATCIrredundant; 
	  }
	  else
	    sat_resolvent_analysis(m, ternary, learned); 
        }
      }
      child = ternary->eqleaf.eqkid[(int)value];
      if (child && child->id > 0 && m->status == 2)
        sat_ternary_tree_based_implication(m, child, depth, learned);
      
      goto TraverseHikid;
    }
  }
  
  /* go for eqkid[0] */
  child = ternary->eqleaf.eqkid[0];
  if (child && m->status == 2) {
    sat_make_decision_based_on_trie(m, ((vid<<1)|1));
    conflicting = sat_implication_for_simplification(m);
     
    if (conflicting) {
      sat_conflict_analysis_with_distillation(m, conflicting, learned);
      m->nLearnedInDistill++;
    }
    else if (m->status == 2) {
      sat_ternary_tree_based_implication(m, child, depth+1, learned);
      sat_ternary_tree_based_undo(m, depth-1);
    }
  }
 
  /* go for eqkid[1] */
  child = ternary->eqleaf.eqkid[1];
  if (child && m->status == 2) {
    sat_make_decision_based_on_trie(m, (vid<<1));
    conflicting = sat_implication_for_simplification(m); 
    
    if (conflicting) {
      sat_conflict_analysis_with_distillation(m, conflicting, learned);
      m->nLearnedInDistill++;
    }
    else if (m->status == 2)  {
      sat_ternary_tree_based_implication(m, child, depth+1, learned);
      sat_ternary_tree_based_undo(m, depth-1);
    }
  }
    
  /* backtrack to level 0 due to unit conflict */  
  if (m->status == 3 && depth == 1) {
    m->status = 2;

    conflicting = sat_implication(m); 
    if (conflicting) {
      m->status = 0;
#ifndef STATS
      fprintf(stdout, "# Conflict at level 0!\n");		
      fprintf(stdout, "Conflict at (");
      sat_print_clause_simple(m, conflicting);
      fprintf(stdout, ")\n");
      sat_print_dot_for_implication_graph(m, conflicting, 0, 1);
#endif
      return;
    } 
    /* resume distilling from the root of the 
       current traversing branch */
    goto DistillANode;
  }

  /** traverse down to the path for hikid
      which must be in the same level as 
      the current node traversing, as if
      they are the nodes of trie-trees.. 
   **/
TraverseHikid:
  if (m->status == 2 && ternary->hikid)
    sat_ternary_tree_based_implication(m, ternary->hikid, depth, learned);
}


/**Function********************************************************************

  Synopsis    [ Make decision based on trie in distillation ] 

  Description [ Make decision based on trie in distillation ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void 
sat_make_decision_based_on_trie(satManager_t *m, long lit)
{
  m->decisionStackSeperator = 
      sat_array_insert(m->decisionStackSeperator, m->stackPos);
  sat_enqueue(m, lit, 0);
}

/**Function********************************************************************

  Synopsis    [ Undo assignment on the ternary tree ] 

  Description [ Undo assignment on the ternary tree ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
sat_ternary_tree_based_undo(satManager_t *m, long level)
{
long i, v;
 
  if (SATCurLevel(m) > level) {
    for (i= m->stackPos-1; i>= m->decisionStackSeperator->space[level]; i--) {
      v = m->decisionStack[i] >> 1;
      m->values[v] = 2;
      m->levels[v] = -1;
      m->marks[v] = 0;
    }  
    m->curPos = m->decisionStackSeperator->space[level];
    m->stackPos = m->curPos;
    m->decisionStackSeperator->size = level;
  }
}
/**Function********************************************************************

  Synopsis    [ Analyzes implication graph to find a good resolvent ] 

  Description [ Analyzes implication graph to find a good resolvent ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
satClause_t* 
sat_resolvent_analysis(
  	satManager_t *m, 
        satTernary_t *t,
	long learned)
{
int value, maxI;
long i, j;
long v, lit, cLit, csize ;
satArray_t *clearned, *cclearned, *redundant;
satClause_t *c;

  v = t->id;

  value = m->values[v];
  
  /** Analyze implication graph to get decisions. **/
  clearned = m->clearned;
  clearned->size = 0;
  cclearned = m->cclearned;
  cclearned->size = 0;
  redundant = m->redundant;
  redundant->size = 0;

  lit = (v<<1) | !value;	/* (value==1 ? (v<<1) : (v<<1)|1); */
  clearned = sat_array_insert(clearned, lit);

  redundant = sat_array_insert(redundant, lit);
  while (redundant->size > 0) {
    redundant->size--;
    c = m->antes[(redundant->space[redundant->size])>>1];
    csize = SATSizeClause(c);
    for (j = 1; j < csize; j++) {
      cLit = c->lits[j];
      v = cLit >> 1;
      if (!m->marks[v] && m->levels[v] > 0) {
        m->marks[v] = 1;
	cclearned = sat_array_insert(cclearned, cLit);
	if (m->antes[v] != 0) {
          redundant = sat_array_insert(redundant, cLit);
	}
	else {
          /* reached a decision */
	  clearned = sat_array_insert(clearned, cLit); 
	}
      }
    }
  }

  maxI = 1;
  for (i = 2; i < clearned->size; i++) 
    if (m->levels[(clearned->space[i])>>1] > m->levels[(clearned->space[maxI])>>1])
      maxI = i;

  lit = clearned->space[maxI]; 
  clearned->space[maxI] = clearned->space[1];
  clearned->space[1] = lit;

  c = sat_add_distilled_clause(m, clearned, learned);
  c->size |= SATCIrredundant;

  m->clearned = clearned;
  m->cclearned = cclearned;
  m->redundant = redundant;
  for (i=0; i<cclearned->size; i++) {
      lit = cclearned->space[i]; 
      m->marks[lit>>1] = 0;
  }
  return (c);
}


/**Function********************************************************************

  Synopsis    [ Apply implication until the implication queue is empty. ]

  Description [ Extension of standard BCP procedure to check subsumption. ] 

  SideEffects []

  SeeAlso     [sat_implication]

******************************************************************************/
satClause_t *
sat_implication_for_simplification(satManager_t *m)
{
satClause_t *conflicting, *c;
satArray_t *wl;
satClause_t **i, **j, **end;
long lit, iLit, first;
long csize, k;
long nProps;

  nProps = 0;
  conflicting = 0;

  while(m->curPos < m->stackPos) {
    lit = m->decisionStack[m->curPos++];
    wl = m->wls[lit];

    if(wl == 0)	continue;
    nProps++;
    /** Sort wl by the number of literals of each clause,
        to find implicate which is not subsumed by any 
	other clause. 
    **/
    sat_sort_clause_array_by_length(wl); 

    for(i = j = (satClause_t **)&(wl->space[0]), end = i + wl->size; i != end;) {
      c = *i++;

      iLit = lit ^ 1;
      /*if(c == 0 || ((c->lits[0] != iLit) && (c->lits[1] != iLit))) 
        continue;*/

      if(c->lits[0] == iLit)
	c->lits[0] = c->lits[1], c->lits[1] = iLit;

      first = c->lits[0];
      if((m->values[first>>1]^SATSign(first)) == 1) {
	*j++ = c;
      }
      else {
	csize = c->size >> SATCsizeShift;
	for(k=2; k<csize; k++) {
	  if((m->values[c->lits[k]>>1] ^ SATSign(c->lits[k])) != 0) {
	    c->lits[1] = c->lits[k];
	    c->lits[k] = iLit;
	    m->wls[(c->lits[1]^1)] = sat_array_alloc_insert(m->wls[(c->lits[1]^1)], (long)c);
	    /*c->size |= SATCIrredundant; */
	    goto foundWatch;
	  }
	}

	*j++ = c;
	if((m->values[first>>1]^SATSign(first)) == 0) {
	  conflicting = c;
	  m->curPos = m->stackPos;
	  while(i<end)	*j++ = *i++;
	}
	else {
	 /* if (SATClauseLearned(c) && !learned)
	    c->size |= SATCIrredundant; */
	  sat_enqueue(m, first, c);
	}
      }
foundWatch:;
    }
    wl->size -= i-j;
  }
  m->nImplicationsInDistill += nProps;
  /*m->simpDBProps -= nProps; */
  return(conflicting);
}

/**Function********************************************************************

  Synopsis    [ Sort a list of clauses by the number of literals in a clause. ]

  Description [ Sort a list of clauses by the number of literals in a clause. ] 

  SideEffects []

  SeeAlso     [ sat_sort_clause_array_by_length_aux ]

******************************************************************************/
void
sat_sort_clause_array_by_length(satArray_t *cl)
{
  sat_sort_clause_array_by_length_aux(&(cl->space[0]), cl->size);
}

static void
sat_sort_clause_array_by_length_aux(long *carr, long size)
{
long i, j, tmp, bi;
satClause_t *pivot;
satClause_t *x, *y;

  if(size <=15) {
    for(i=0; i<size-1; i++) {
      bi = i;
      for(j=i+1; j<size; j++) {
	x = ((satClause_t *)(carr[j]));
	y = ((satClause_t *)(carr[bi]));
	if((x->size>>3) < (y->size>>3)) 
	  bi = j;
      }
      tmp = carr[i];
      carr[i] = carr[bi];
      carr[bi] = tmp;
    }
  }
  else {
    pivot = (satClause_t *)carr[size>>1];
    i = -1;
    j = size;

    while(1) {
      do i++; while( (((satClause_t *)(carr[i]))->size>>3) > 2 && ((pivot->size>>3) <= 2 ||
	      ((satClause_t *)(carr[i]))->info.activity < pivot->info.activity));
      do j--; while( (pivot->size>>3) > 2 && ((((satClause_t *)(carr[j]))->size>>3) <= 2 ||
	      pivot->info.activity < ((satClause_t *)(carr[j]))->info.activity));
      if(i>=j)	break;
      tmp = carr[i];
      carr[i] = carr[j];
      carr[j] = tmp;
    }
    sat_sort_clause_array_by_length_aux(carr, i);
    sat_sort_clause_array_by_length_aux(&(carr[i]), size-i);
  }
}

/**Function********************************************************************

  Synopsis    [ Conflict analysis based on ternary tree structure ]

  Description [ Conflict analysis based on ternary tree structure ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
long
sat_conflict_analysis_with_distillation(satManager_t *m, satClause_t *conflicting, long learned)
{
int isNotDecision;
long nMarks, i, j, maxI, limit;
long lit, *pLit, cLit;
long absLevel, bLevel;
long v, csize, tv;
satClause_t *c;
satArray_t *clearned, *cclearned;

int firstIter, subsumptionCheck;
int nDecisions;
long nAllMarks, nResolventLits;
long nDistilled, nLevelZeros, abstract;
satClause_t *resolvent, *traversed;

#if 0
int elimnable, flags;
long abstract;
#endif

  firstIter = 0;
  nDistilled = 0;
  nAllMarks = 0;
  nLevelZeros = 0;
  m->resolvents->size = 0;
  subsumptionCheck = m->subsumeInConflict;
  resolvent = (subsumptionCheck ? conflicting : 0);
  traversed = 0;

  isNotDecision = 0;
  clearned = m->clearned;
  clearned->size = 0;
  clearned = sat_array_insert(clearned, 0);
  i = m->stackPos - 1;
  bLevel = lit = 0;
  nMarks = 0;
  tv = 0;
  
  do {
    nResolventLits = nAllMarks;
    nLevelZeros = 0;
    nDecisions = 0;

    c = conflicting;
    csize = SATSizeClause(c);
    j = (lit == 0) ? 0 : 1;
    pLit = &(c->lits[j]);
   
    for (; j<csize; j++) {
      cLit = *pLit++;
      v = cLit >> 1;

      if (m->antes[v] <= 0 && m->levels[v] > 0)
        nDecisions++;

      if (!m->marks[v] && m->levels[v]>0) {
	m->marks[v] = 1;

	nAllMarks++;
	if (m->levels[v] >= SATCurLevel(m))
	  nMarks++;
	else {
	  clearned = sat_array_insert(clearned, cLit);
	  if (m->levels[v] > bLevel)
	    bLevel = m->levels[v];
	}
      }
      else if (m->levels[v] == 0)
        nLevelZeros++;
    }
    if ((traversed == 0) && (nDecisions >= SATCurLevel(m)))
      traversed = c; 

    /** Subsumption check in conflict analysis **/
    if (subsumptionCheck && firstIter > 0) {
      if (resolvent > 0 && (nResolventLits == nAllMarks)) {
        /* previous resolvent is subsumed by current resolvent */
        nDistilled++;
      
        sat_strengthen_clause_in_conflict_analysis(m, resolvent, 0);
        if ((csize - nLevelZeros) > nAllMarks) {
          /* delete the antecedent, when antecednet is also subsumed */
	  m->nEliminatedClsInConflict++;
	  m->nEliminatedLitsInConflict += csize;
          nDistilled++;
          
	  if (SATClauseOriginal(resolvent) || !SATClauseOriginal(c)) {
            sat_array_delete_elem(m->wls[(c->lits[1])^1], (long)c);
	    if (csize > 1)
              c->lits[1] = m->nVars << 1;
	  }
	  else {
            sat_strengthen_clause_in_conflict_analysis(m, c, 0);
	  }
	}  
      }
      else if ((csize - nLevelZeros) > nAllMarks) {
        /* antecedent is subsumed by current resolvent */
        nDistilled++;
        resolvent = c;
        sat_strengthen_clause_in_conflict_analysis(m, resolvent, 0);
      }
      else 
        resolvent = 0;
    }

    firstIter++;
    while (i>=0 && !(m->marks[(m->decisionStack[i--])>>1]));
    lit = m->decisionStack[i+1];
    tv = lit >> 1; 
    conflicting = m->antes[tv];
    m->marks[tv] = 0;
    nMarks--;
    nAllMarks--;
  } while (nMarks > 0);
  clearned->space[0] = lit^1;

  m->nDistillInConflict += nDistilled;

#ifdef DEBUG
  fprintf(stdout, "learned ");
  sat_print_array_as_clause(m, clearned);
#endif

  m->clearned = clearned;
  
  if (clearned->size == 0) {
    m->status = 0; 
    clearned->size = 0;
    sat_ternary_tree_based_undo(m, 0);
    return 0;
  }

  if (clearned->size == 1) {
    m->status = 3; /* BACKTRACK mode */
    m->nLearnedUnitClInDistill++;
    /** NOTE : Back tracking must be performed prior to
     *  adding a unit conflict clause. Or adding clause
     *  function will yield conflict while it asserts
     *  the unit clause added.
     **/
    sat_ternary_tree_based_undo(m, 0);
   
    if (resolvent > 0) {
      resolvent->size |= SATCIrredundant;
      sat_enqueue_check(m, resolvent->lits[0], resolvent);
      m->nOmittedConflictClauses++;
      m->nOmittedConflictLits++;
    }
    else {
      c = sat_add_distilled_clause(m, clearned, 0);
      c->size |= SATCIrredundant;
    }
    /** TODO : not sure for these, but not to change
     *  variable and clause decay tends to be more
     *  beneficial for industrial benchmarks.
     **/
    /*sat_update_variable_decay(m);
    sat_update_clause_decay(m); */
    clearned->size = 0;
    return 0;
  }
  else {
    cclearned = m->cclearned;
    cclearned->size = 0;
    /** minimize conflict learned clause **/
    absLevel = 0;
    for (i = 1; i < clearned->size; i++) 
      absLevel |= sat_abstract_level(m, (clearned->space[i])>>1);
    m->cclearned = cclearned = sat_array_copy(clearned, m->cclearned);
    isNotDecision = m->antes[(clearned->space[0]>>1)] == 0 ? 0 : 1;
    for(i=j=1; i < clearned->size; i++) {
       lit = clearned->space[i]; 
       v = lit >> 1;
       if (m->levels[v] > 0 && (m->antes[v] == 0 || !sat_is_redundant_lit(m, lit, absLevel))) {
         clearned->space[j++] = lit;
	 if (m->antes[v] != 0) 
	   isNotDecision = 1;
       }
    }
    clearned->size -= (i-j);

    maxI = 1;
    for (i = 2; i < clearned->size; i++)
      if (m->levels[(clearned->space[i])>>1] > m->levels[(clearned->space[maxI])>>1])
        maxI = i;
    lit = clearned->space[maxI];
    clearned->space[maxI] = clearned->space[1];
    clearned->space[1] = lit;

    /** Subsumption check in conflict analysis **/
    if (!isNotDecision && !resolvent)
      resolvent = traversed;

    if (resolvent > 0) {
      resolvent->size |= SATCIrredundant;
      if (SATSizeClause(resolvent) > clearned->size) {
        sat_delete_watched_literal(m, resolvent);
        abstract = 0;
	for (i = 0; i < clearned->size; i++) {
          lit = clearned->space[i];
	  resolvent->lits[i] =lit;
	  abstract |= 1 << (SATVar(lit) & 31);
	}
	resolvent->size = (clearned->size << SATCsizeShift) | (resolvent->size & SATCMask);
	sat_add_watched_literal(m, resolvent);
	if (SATClauseVisited(resolvent))
	  resolvent->info.abstract = abstract;
      }
      m->nOmittedConflictClauses++;
      m->nOmittedConflictLits += m->clearned->size;
    }
  }
  cclearned = m->cclearned;
  for (j = 0; j < cclearned->size; j++) 
    m->marks[(cclearned->space[j]>>1)] = 0; 

  /* check backward subsumption before adding a new clause */

  m->clearned = clearned;
  m->cclearned = cclearned;
  
#if 0 
  traversed = sat_DFS_to_get_clause_reference(m, t, 1); 
  traversed->size |= SATCIrredundant;

  elimnable = 1;
  csize = SATSizeClause(traversed);
  if ((csize -1) >= clearned->size) {
    for (i = 1; i < csize; i++) {
      ante = m->antes[(traversed->lits[i])>>1];
      if (ante != 0) {
        elimnable = 0;
	ante->size |= SATCIrredundant;
      }
    }
  }
  else {
    elimnable = 0;
  }

#endif
  if (!isNotDecision) {
    if (resolvent == 0) {
      c = sat_add_distilled_clause(m, clearned, learned);
      c->size |= SATCIrredundant;
    }

#if 0 
    sat_delete_watched_literal(m, traversed); 
    abstract = 0;
    for (i = 0; i < clearned->size; i++) {
      lit = clearned->space[i];
      traversed->lits[i] = lit;
      abstract |= 1 << (SATVar(lit) & 31);
    }
    flags = traversed->size & SATCMask; 
    traversed->size = (clearned->size << SATCsizeShift) | flags;
    traversed->info.abstract = abstract;
    sat_add_watched_literal(m, traversed);
#endif
  }
  else { 
#if 1 
    if (!subsumptionCheck || !resolvent) {
      limit = m->clauses->size <= 150000 ? (long)(clearned->size * 1.1) : 4 ; 
      if (clearned->size <= limit) { 
	/** Add the first learned clause 
         *  which must be set as irredundant.
         **/
        c = sat_add_distilled_clause(m, clearned, 1);
        c->size |= SATCIrredundant; 
        m->nLearnedClInDistill++;
        m->nLearnedLitInDistill += SATSizeClause(c);
      }
    }
#endif

#if 1 
    for (i = 0; i < clearned->size; i++) {
      lit = clearned->space[i];
      v = lit >> 1;
      if (m->levels[v] < SATCurLevel(m)) 
        m->marks[v] = 1;
    }
    sat_conflict_analysis_on_decisions(m, clearned, traversed, learned);
#endif
  }
  sat_ternary_tree_based_undo(m, SATCurLevel(m)-1);
 
  return(bLevel);
}

void
sat_conflict_analysis_on_decisions(satManager_t *m, satArray_t *clearned, satClause_t *traversed, long learned) 
{
int value, maxI1, maxI2, flags;
long i, j, k, csize, abstract;
long lit, v, tv, tlit;
satClause_t *c, *ante;
satArray_t *cclearned, *decisions, *redundant;

  cclearned = m->cclearned;
  cclearned->size = 0;
  decisions = m->temp;
  decisions->size = 0;
  redundant = m->redundant;
  redundant->size = 0;

  /** traverse implication graph in reverse to replace the literals 
   *  of the conflict clause with their decisions from which they
   *  are implied.
   **/
#if 0 
    fprintf(stdout, "**********************************\n");
    fprintf(stdout, "* Conflict analysis on decisions *\n");
    fprintf(stdout, "**********************************\n");
#endif

  m->cclearned = cclearned = sat_array_copy(clearned, m->cclearned); 
  for (i=j=0; i < clearned->size; i++) {
    lit = clearned->space[i];
    v = lit >> 1;
    ante = m->antes[v];

#if 0 
    fprintf(stdout, "Lit %c%ld%c@%d\n", lit&1 ? '-':' ', v, ante == 0 ? '*' : ' ', (int)m->levels[v]);
#endif

    if (ante != 0) {
      /* traverse back upto decisions on which 
       * the variable is implicated */
      redundant = sat_array_insert(redundant, lit);
      while (redundant->size > 0) {
        redundant->size--;
        c = m->antes[(redundant->space[redundant->size])>>1];
	csize = SATSizeClause(c);
	for (k = 0; k < csize; k++) {
	  tlit = c->lits[k];
	  tv = tlit >> 1;
          if (!m->marks[tv] && m->levels[tv] > 0) {
	    m->marks[tv] = 1;
            if (m->antes[tv] != 0) {
	      redundant = sat_array_insert(redundant, tlit); 
	    }
	    else {
	      /* reached a decision */
              decisions = sat_array_insert(decisions, tv); 
	    }
	    cclearned = sat_array_insert(cclearned, tlit);
	  }
	}
      }
    }
    else {
      clearned->space[j++] = lit;
    }
  } 
  clearned->size -= (i-j);

  /** add decisions into the conflict clause, then update
   *  watched literals 
   **/
#if 1 
  for (i = 0; i < decisions->size; i++) {
    v = decisions->space[i];
    value = m->values[v];
    clearned = sat_array_insert(clearned, (v<<1)|value);
  }

  maxI1 = 0;
  for (i = 0; i < clearned->size; i++) {
    lit = clearned->space[i];
    if (m->levels[(lit>>1)] > m->levels[(clearned->space[maxI1]>>1)]) 
        maxI1 = i;
  }
  lit = clearned->space[maxI1];
  clearned->space[maxI1] = clearned->space[0];
  clearned->space[0] = lit;

  maxI2 = 1;
  for (i = 2; i < clearned->size; i++) {
    lit = clearned->space[i];
    if (m->levels[lit>>1] > m->levels[clearned->space[maxI2]>>1]) 
        maxI2 = i;
  }
  lit = clearned->space[maxI2];
  clearned->space[maxI2] = clearned->space[1];
  clearned->space[1] = lit;

  if (traversed == 0) {
    c = sat_add_distilled_clause(m, clearned, learned);
    c->size |= SATCIrredundant;
  }
  else {
    sat_delete_watched_literal(m, traversed);
    abstract = 0;
    for (i = 0; i < clearned->size; i++) {
      lit = clearned->space[i];
      traversed->lits[i] = lit;
      abstract |= 1 << (SATVar(lit) & 31);
    }
    sat_add_watched_literal(m, traversed);
    traversed->size |= SATCIrredundant;
    flags = traversed->size & SATCMask;
    traversed->size = (clearned->size << SATCsizeShift) | flags;
    if (learned)
      traversed->info.abstract = abstract;
  }
#endif

  for (i = 0; i < cclearned->size; i++) 
    m->marks[cclearned->space[i]>>1] = 0;

  m->clearned = clearned;
  m->cclearned = cclearned;
  m->temp = decisions;
  m->redundant = redundant;
}

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [ Recompute the variables score ]

  Description [ Recompute variables score after resetting current scores.
                As a default and basic scoring scheme, it counts variables
	        occurrencies in the CNF clauses. It may be extended with
		various scoring schemes. ]

  SideEffects [ All clauses found satisfied are eliminated from clause 
                databased. ]

  SeeAlso     [ ]

******************************************************************************/
int  
sat_recompute_var_score(satManager_t *m)
{
int limit;
long i, j, nVars, csize, cflags, lit;
long nCl, nLit, nSATCl;
char value; 
satArray_t *clauses, *arr;
satClause_t *c;

  arr = sat_array_alloc(16);
  
  limit = (m->clausesHistogram[m->majorityClauseLength] + m->clausesHistogram[m->majorityClauseLength+1] >= 500000) ? 1 : 0;

  /** Reset the current scores of variables **/ 
  nVars = m->nVars+1;;
  if (m->nDistill > 0)  
    memset(m->scores, 0, sizeof(long)*(nVars<<1));  

  nCl = nLit = nSATCl = 0;
  /** Counting up the occurrencies of 
   *  each literal in satisfiable clause.
   *  1) For the original clauses 
   **/
  clauses = m->clauses;
  for (i=0; i<clauses->size; i++) {
    c = (satClause_t *)clauses->space[i];
    if (c == 0)	continue;
  
    arr->size = 0;
    csize = SATSizeClause(c); 
    if (csize > 0) {
      if (csize == 1) {
        clauses->space[i] = clauses->space[--(clauses->size)];
	i--;
	continue;
      }
      else {
        if ((limit && csize >= 8) || (limit && csize <= 10 && m->clausesHistogram[csize] > 10000))
          c->size |= SATCIrredundant;
        else {
          for (j=0; j<csize; j++) {
            lit = c->lits[j];
	    if (lit == 0) continue;

	    value = m->values[lit>>1];
	    if (value == 2) 
	      arr = sat_array_insert(arr, lit); 
	    else if ((value ^ (lit&1)) == 1) { 
              /* The clause is satisfied */
	      clauses->space[i] = clauses->space[--(clauses->size)];
	      sat_delete_clause(m, c); 
	      arr->size = 0;
	      nSATCl++;  
	      i--;
	      goto metSATOrgCl;
	    }  
	    else {
	      /* eliminate an false literal */
              c->lits[j] = c->lits[--csize]; 
	      j--;
	    }
          }
	  /* update the size of clause */
          cflags = c->size & SATCMask;
          c->size = (csize << SATCsizeShift) | cflags;
        }
        for (j=0; j<arr->size; j++) {
          lit = arr->space[j];
          m->scores[lit]++;
        }
        nCl++; 
        nLit += SATSizeClause(c); 
      }
    }  
metSATOrgCl:;
  }
  if (m->nDistill == 0) {
    m->nInClForDistill = nCl;
    m->nInLitForDistill = nLit;
  }

  /**  2) For the learned clauses 
   **/
  nCl = nLit = 0;
  clauses = m->learned;
  for (i=0; i<clauses->size; i++) {
    c = (satClause_t *)clauses->space[i];
    if (c == 0)	continue;

    arr->size = 0;
    csize = SATSizeClause(c);
    if (csize > 0) {
      if (csize == 1) {
        clauses->space[i] = clauses->space[--clauses->size];
        i--;
      }
      else {
        if ((limit && csize >= 8) || (limit && csize <= 10 && m->clausesHistogram[csize] > 10000)) 
          c->size |= SATCIrredundant;
	else {
          for (j=0; j<csize; j++) {
            lit = c->lits[j];
	    if (lit == 0) continue;

            lit = c->lits[j];
	    value = m->values[lit>>1];
	    if (value == 2) 
	      arr = sat_array_insert(arr, lit); 
	    else if ((value ^ (lit&1)) == 1) { 
              /* The clause is satisfied */
	      clauses->space[i] = clauses->space[--(clauses->size)];
	      sat_delete_clause(m, c); 
	      arr->size = 0;
	      nSATCl++;  
	      i--;
	      goto metSATLearnedCl;
	    }
	    else {
	      /* eliminate an false literal */
	      assert(j > 1);
              c->lits[j] = c->lits[--csize]; 
	      j--;
	    }
          }
	  /* update the size of clause */
          cflags = c->size & SATCMask;
          c->size = (csize << SATCsizeShift) | cflags;

          for (j=0; j<arr->size; j++) {
            lit = arr->space[j];
            m->scores[lit]++;
          }
	}
        nCl++; 
        nLit += SATSizeClause(c); 
      }
    }
metSATLearnedCl:;
  }
  if (m->nDistill == 0) {
    m->nInLearnedClForDistill = nCl;
    m->nInLearnedLitForDistill = nLit;
  }
  m->nSATCl = nSATCl;

  arr->size = 0;
  free(arr);

  /** All of clauses are satisfied **/
  if (m->nInClForDistill==0 && nCl==0) {
    fprintf(stdout, "All clauses are satisfied at level zero!\n");
    return 0;
  }
  return 1;
}

/**Function********************************************************************

  Synopsis    [ Print dot file of Ternary Search Tree ]
  
  Description [ Print dot file of Ternary Search Tree ]
  
  SideEffects [ ]

  SeeAlso     []

******************************************************************************/
void 
sat_print_dot_for_ternary_search_tree(
	satManager_t *m, 
	satTernary_t *root,
	long num)
{
char name[1024];
long nNode;
FILE *fp;

  if (root == 0) return;
  
  fprintf(stdout, " >>>> Dot file for Ternary Search Tree is printed! <<<<\n");
  sprintf(name, "%s_%s_%d.dot", m->cnfFileName, "ternary", (int)num);
  fp = fopen(name, "w");

  fprintf(fp, "digraph \"TernaryGraph\" {\n");
  fprintf(fp, "  margin=0.5;\n label=\"Trie\";\n");
  fprintf(fp, "  page=\"8.5,11\" size=\"7.5,10\";\n ratio=\"auto\" center=\"true\";\n");
  //fprintf(fp, "  nNode [shape=box];\n");
  nNode = 1;
  fprintf(fp, "  %ld.%ld [label=\"%ld\"];\n", root->id, nNode, root->id);
  sat_traverse_ternary_tree_to_print_out_dot(m, fp, root, &nNode); 
  fprintf(fp, "}\n");
  fclose(fp);
}

/**Function********************************************************************

  Synopsis    [ Traverse Ternary Search Tree to print dot file ]

  Description [ Traverse Ternary Search Tree to print dot file ]

  SideEffects [ order :
  			0 - lower kid
			1 - equal kid
			2 - higher kid ]

  SeeAlso     []

******************************************************************************/
void
sat_traverse_ternary_tree_to_print_out_dot(
	satManager_t *m,
	FILE *fp,
	satTernary_t *ternary,
	long *nNode)
{
long index;
long v, tv;
satTernary_t *child;

  v = ternary->id;
  index = *nNode;
  
  /** Visit children with printing those nodes out **/
  if (ternary->lokid) {
    (*nNode)++;
    child = ternary->lokid;
    tv = child->id;
    fprintf(fp, "  %ld.%ld [label=\"%ld\"];\n", tv, *nNode, tv);
    fprintf(fp, "  %ld.%ld -> %ld.%ld ", v, index, tv, *nNode); 
    fprintf(fp, "  [color=red];\n");
    sat_traverse_ternary_tree_to_print_out_dot(m, fp, child, nNode);
  }
  if (ternary->id > 0) {
    if (ternary->eqleaf.eqkid[0]) {
      (*nNode)++;
      child = ternary->eqleaf.eqkid[0];
      tv = child->id;
      if (tv == 0) {
        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); 
        fprintf(fp, "  %ld.%ld -> %ld.%ld ", v, index, tv, *nNode);
        fprintf(fp, "  [style=dotted, label=\"0\"];\n");
      }
      else {
        fprintf(fp, "  %ld.%ld [label=\"%ld\"];\n", tv, *nNode, tv);
        fprintf(fp, "  %ld.%ld -> %ld.%ld ", v, index, tv, *nNode);
        fprintf(fp, "  [style=dotted, label=\"0\"];\n");
        sat_traverse_ternary_tree_to_print_out_dot(m, fp, child, nNode);
      }
    }
    if (ternary->eqleaf.eqkid[1]) {
      (*nNode)++;
      child = ternary->eqleaf.eqkid[1];
      tv = child->id;
      if (tv == 0) {
        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); 
        fprintf(fp, "  %ld.%ld -> %ld.%ld ", v, index, tv, *nNode);
        fprintf(fp, "  [style=dotted, label=\"1\"];\n");
      }
      else {
        fprintf(fp, "  %ld.%ld [label=\"%ld\"];\n", tv, *nNode, tv);
        fprintf(fp, "  %ld.%ld -> %ld.%ld ", v, index, tv, *nNode);
        fprintf(fp, "  [style=dotted, label=\"1\"];\n");
        sat_traverse_ternary_tree_to_print_out_dot(m, fp, child, nNode);
      }  
    }
  }
  if (ternary->hikid) {
    (*nNode)++;
    child = ternary->hikid;
    tv = child->id;
    fprintf(fp, "  %ld.%ld [label=\"%ld\"];\n", tv, *nNode, tv);
    fprintf(fp, "  %ld.%ld -> %ld.%ld ", v, index, tv, *nNode);
    fprintf(fp, "  [color=blue];\n");
    sat_traverse_ternary_tree_to_print_out_dot(m, fp, child, nNode);
  }
}

/**Function********************************************************************

  Synopsis    [ Print an assignment stack ]

  Description [ Print an assignment stack ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_print_scores(satManager_t *m) 
{
long i, lit;

  fprintf(stdout, "------------Print Scores-----------\n");
  fprintf(stdout, "%5s : %3s %3s\n", "VAR", "+", "-");
  for (i=0; i<=m->nVars; i++) {
    lit = i<<1;
    fprintf(stdout, "%5d : %3d %3d\n", (int)i, (int)m->scores[lit], (int)m->scores[lit|1]);  
  }
}

/**Function********************************************************************

  Synopsis    [ Assert pure literals ]

  Description [ Assert pure literals ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void 
sat_assert_pure_literals(satManager_t *m)
{
long i, v;
char value;

  for (i=0; i<=m->nVars; i++) {
    v = i;
    value = m->values[v];

    if (value != 2) continue;

    if(m->pure[i] == 1) 
      sat_enqueue_check(m, i<<1, 0);
    else if(m->pure[i] == 2) 
      sat_enqueue_check(m, (i<<1)+1, 0);
  }

} 

/**Function********************************************************************

  Synopsis    [ Add a conflit clause generated during distillation ]

  Description [ Add a conflit clause generated during distillation ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
satClause_t *
sat_add_distilled_clause(satManager_t *m, satArray_t *arr, long learned)
{
long lit;
satClause_t *c;

  if(arr->size == 1) {
    lit = arr->space[0];
    c = sat_new_clause(arr, 0);
    if (learned) {
      m->learned = sat_array_insert(m->learned, (long)c);
      c->size |= SATCLearned; 
    }
    else 
      m->clauses = sat_array_insert(m->clauses, (long)c);
    sat_enqueue(m, lit, c);
  }
  else {
    c = sat_new_clause(arr, learned);
    if (learned) {
      m->learned = sat_array_insert(m->learned, (long)c);
    }
    else
      m->clauses = sat_array_insert(m->clauses, (long)c);
    sat_add_watched_literal(m, c);
  }

  /*if (learned) {
    m->nCurLearnedLits += arr->size;
    m->nCurLearnedClauses++;
    m->nTotalLearnedLits += arr->size;
    m->nTotalLearnedClauses++;
  }*/
  return(c);
}

/**Function********************************************************************

  Synopsis    [ Delete the clauses unmarked in distilling ]

  Description [ Delete the clauses unmarked in distilling ]

  SideEffects [ Satisfied clauses are also deleted. ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_delete_unmakred_clauses_for_simplification(satManager_t *m)
{
int compactness, callVarelim;
long i, j, nLit;
long csize, lit;
satArray_t *arr;
satClause_t *c;

  callVarelim = (m->elimTime < 5.0) ? 1 : 0;
  /** reset watched literals **/
  for (i=1; i<=m->nVars; i++) {
    lit = i << 1;
    if (m->values[i] <= 2) { 
      m->scores[lit] = 0;
      m->scores[lit|1] = 0;
      if (m->wls[lit|1])  m->wls[lit|1]->size = 0;
      if (m->wls[lit])    m->wls[lit]->size = 0;
    }
  } 

  arr = m->clauses;
  nLit = 0;
  for (i=j=0; i<arr->size; i++) {
    c = (satClause_t *)arr->space[i];
    csize = SATSizeClause(c); 
    if (csize == 1) {
      arr->space[j++] = arr->space[i];
      sat_update_clauses_statistics(m, c);
      continue;
    }
    
    if (!SATClauseIrredundant(c)) {
      if(c->dependent)
        free(c->dependent);
      free(c);
    }
    else {
      c->size -= SATCIrredundant;
      compactness = sat_squeeze_clause(m, c); 
      sat_update_clauses_statistics(m, c);
      if (compactness == 0) {
        if (c->dependent)
          free(c->dependent);
        free(c);
      }
      else if (compactness == 1) {
        if (callVarelim == 1)
	  sat_sort_clause_literal(c);

        sat_add_watched_literal(m, c);
        arr->space[j++] = arr->space[i];
        nLit += csize; 
      }
    }
  }
  arr->size -= (i-j);
  m->nOutClForDistill = arr->size;
  m->nOutLitForDistill = nLit;

  arr = m->learned;
  nLit = 0; 
  for (i=j=0; i<arr->size; i++) {
    c = (satClause_t *)arr->space[i];
    csize = SATSizeClause(c);

    if (csize == 1) {
      arr->space[j++] = arr->space[i];
      sat_update_clauses_statistics(m, c);
      continue;
    }

    if (!SATClauseIrredundant(c)) {
      if(c->dependent)
        free(c->dependent);
      free(c);
    }
    else {
      c->size -= SATCIrredundant;
      compactness = sat_squeeze_clause(m, c); 
      if (compactness == 0) {
        if(c->dependent)
          free(c->dependent);
        free(c);
      }
      else if (compactness == 1) {
        if (callVarelim == 1) 
          sat_sort_clause_literal(c);

        sat_add_watched_literal(m, c);
        arr->space[j++] = arr->space[i];
        nLit += csize; 
      }
    }
  }
  arr->size -= (i-j);
  m->nOutLearnedClForDistill += arr->size;
  m->nOutLearnedLitForDistill += nLit;
}

/******************************************************************************
 * 
 * Utilities
 *
*******************************************************************************/
void 
sat_report_result_for_distillation(satManager_t *m) 
{
  if (m== 0) return;

  fprintf(stdout, "===========================[ %s Statistics ]==============================\n",
  (m->nDistill == 0) ? "Alembic" : "PAL");

  fprintf(stdout, "Distilled origianl clauses    : %ld out of %ld\n", m->nInClForDistill - m->nOutClForDistill, m->nInClForDistill); 
  fprintf(stdout, "Distilled origianl literals   : %ld out of %ld\n", m->nInLitForDistill - m->nOutLitForDistill, m->nInLitForDistill); 
  fprintf(stdout, "Distilled learned clauses     : %ld out of %ld\n", m->nInLearnedClForDistill - m->nOutLearnedClForDistill, m->nInLearnedClForDistill); 
  fprintf(stdout, "Distilled learned literals    : %ld out of %ld\n", m->nInLearnedLitForDistill - m->nOutLearnedLitForDistill, m->nInLearnedLitForDistill); 
  fprintf(stdout, "Added clauses in distillation : %ld\n", m->nLearnedClInDistill);
  fprintf(stdout, "Added units in distillation   : %ld\n", m->nLearnedUnitClInDistill);
  fprintf(stdout, "Added literals in distillation: %ld\n", m->nLearnedLitInDistill);
  fprintf(stdout, "Conflicts in distillation     : %ld\n", m->nLearnedInDistill);
  fprintf(stdout, "Implied in distillation       : %ld\n", m->nResolvedInDistill);
  fprintf(stdout, "Implications in distillation  : %0.f\n", m->nImplicationsInDistill); 
 
  if (m->subsumeInConflict) { 
    fprintf(stdout, "Number of continuous distill in Alembic: %ld\n", m->nDistillInConflict);
  }

  if (m->nDistill == 0) 
    fprintf(stdout, "Distill time : %10g \n", m->distillTime);
  fprintf(stdout, "\n");
}


/**Function********************************************************************

  Synopsis    [ Free ternary search tree structure ]

  Description [ Free ternary search tree structure ]

  SideEffects [ ]

  SeeAlso     [ sat_BuildTrieForAlembic ]

******************************************************************************/
void
sat_free_ternary(satTernary_t *ternary)
{
  if (ternary == 0)	return;

  sat_free_ternary(ternary->lokid);
  
  if (ternary->id > 0) {
    sat_free_ternary(ternary->eqleaf.eqkid[0]);
    sat_free_ternary(ternary->eqleaf.eqkid[1]);
  }
  else  
    ternary->eqleaf.c = 0;
  
  sat_free_ternary(ternary->hikid);

  free(ternary);
}


/**Function********************************************************************

  Synopsis    [ Print clause array ]

  Description [ Print clause array ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
void
sat_print_array_as_clause(satManager_t *m, satArray_t *arr)
{
long i, lit, v;

  if (arr == 0) return;

  fprintf(stdout, "Clause array ( ");
  for (i=0; i<arr->size; i++) {
    lit = arr->space[i];
    v = SATVar(lit);
    fprintf(stdout, "%s%ld@%ld%s", lit&1 ? "-":"", v, m->levels[v], 
    		m->antes[v] != 0? " ":"* ");
  }
  fprintf(stdout, " )\n");
}