source: vis_dev/cusp-1.1/src/sat/sat.c

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

  FileName    [sat.c]

  PackageName [sat]

  Synopsis    [Routines for sat function.]

  Author      [Hoonsang Jin, 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 <setjmp.h>
#include <signal.h>
#include <string.h>
#include <stdlib.h>
#include <zlib.h>
#include "sat.h"
#include "util.h"

#define STATS
#define HS_INDEX 6
#define LINEBUFSIZE 327680  

static char rcsid[] UNUSED = "$Id $";
static jmp_buf timeOutEnv;
static int CirCUsTimeOut;       
static long alarmLapTime;

#ifndef HAVE_LIBGMP

int
main(int argc, char ** argv)
{
char * filename = 0;
int timeout = -1;
int i;
satArray_t *sat_options;

  sat_options = sat_array_alloc(3);
  for (i = 0; i < 3; i++)  
    sat_array_insert(sat_options, 0);

  fprintf(stdout, "c %s (compiled %s)\n", 
          CUR_VER,  DateReadFromDateString(CUR_DATE));

  if (argc <= 2) { 
    if (argc < 2 || !strcmp (argv[1], "-h")) {
      goto usage;
    } 
    filename = strdup(argv[1]);
    sat_main(filename, timeout, sat_options);
    return 0;    
  }
 
  for (i = 1; i < argc; i++) {
    if (!strcmp (argv[i], "-cnf")) {
      
      filename = strdup(argv[i+1]);
      
    } else if (!strcmp (argv[i], "-t")) {
      
      timeout = atoi(argv[i+1]);      
      
    } else if (!strcmp (argv[i], "-quiet")) {

      sat_options->space[0] = 1;
      
    } else if (!strcmp (argv[i], "-velim")) {

      sat_options->space[1] = 1;
      
    } else if (!strcmp (argv[i], "-distill")) {

      sat_options->space[2] = 1;
      
    } else if (i == 1) {

      filename = strdup(argv[i]);
      
    }
  }

  if (!filename)   goto usage;

  /* e.g. cusp -cnf file */
  sat_main(filename, timeout, sat_options);
  
  return 0;

usage:
  (void) fprintf(stderr, "USAGE: cusp [-h] [problem] <input-file> [problem-options] [-t <seconds>]\n\n");
  (void) fprintf(stderr, "-h            print the command usage\n\n");
  (void) fprintf(stderr, "PROBLEM:\n\n");
  (void) fprintf(stderr, "  -cnf        Propositional Satisfiability (default)\n\n");
  (void) fprintf(stderr, "CNF-OPTIONS:\n\n");
  (void) fprintf(stderr, "  -quiet      suppress printing solution (default 0)\n");
  (void) fprintf(stderr, "  -velim      preprocessing: variable elimination (default 0)\n");
  (void) fprintf(stderr, "  -distill    preprocessing: clause distillation (default 0)\n");
  (void) fprintf(stderr, "\n");

  return 1;
}
#endif

int
sat_main(char * filename, int timeout, satArray_t* options)
{
satManager_t *m;
long btime, etime;

  btime = util_cpu_time();
  m = sat_init_manager();
  m->allSat = 0;
  if (timeout > 0) {
    CirCUsTimeOut = timeout;
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(CirCUsTimeOut);
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(stdout,
                "c CirCUs : timeout occurred after %d seconds.\n", CirCUsTimeOut);
      alarm(0);
      etime = util_cpu_time();
      m->solveTime = (double)(etime - btime) / 1000.0;
      sat_report_result(m);
      free(filename);
      return 1;
    }
  }

    
  if (options->space[0]) {      /* supress printing solution */
    m->printModel = 0;  
  }
  else {
    m->printModel = 1;  
  }
  if (options->space[1]) {      /* preprocess variable elimination */
    m->simplify = 1;
    m->grow = 0;
    m->nIteratePreprocess = 3;
  }
  if (options->space[2]) {      /* preprocess clause distillation */
    m->distill = 1; 
  }
  
  if(sat_read_cnf(m, filename) == 0) 
    goto gotoEnd;

  if(m->status == 0) {
    sat_report_result(m);
    goto gotoEnd;
  }

  etime = util_cpu_time();
  m->readTime = (double)(etime - btime) / 1000.0;

  if (m->simplify)
    sat_eliminate_var_main(m);

  if(m->status == 2) {
    sat_circus_solve(m);
    if(m->status == 1) {
      if (m->simplify)
        sat_extend_model(m);
      sat_verify(m);
    }
  }

  etime = util_cpu_time();
  m->solveTime = (double)(etime - btime) / 1000.0;

  sat_report_result(m);

  if(m->coreGeneration && m->status == 0) {
    sat_generate_unsat_core_main(m);
    sat_print_unsat_core(m, filename);
  }

gotoEnd:;
   
  free(filename);
  sat_free_manager(m);
  return 0;
} 

void
TimeOutHandle(void)
{
  int seconds = (int) ((util_cpu_ctime() - alarmLapTime) / 1000);

  if (seconds < CirCUsTimeOut) {
    unsigned slack = (unsigned) (CirCUsTimeOut - seconds);
    (void) signal(SIGALRM, (void(*)(int)) TimeOutHandle);
    (void) alarm(slack);
  } else {
    longjmp(timeOutEnv, 1);
  }
} 

void 
sat_circus_solve(satManager_t *m)
{
double nConflicts;
long iter, i;

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

  if (m->simplify == 0)
    sat_simplify(m);

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

  if(m->allSat == 0) {
    for(i=1; i<=m->nVars; i++) {
      if(m->values[i] == 2)
        sat_heap_insert(m, m->variableHeap, i);
    }
  }

  if (m->distill)
    sat_distill_clauses_with_preprocessing(m);

  sat_print_cnf(m, 0);
  
  nConflicts = m->restartFirst;
  m->reduceClausesThresh = (m->clauses->size + m->learned->size) * m->learnedSizeFactor;
  if(m->reduceClausesThresh < 2000)     m->reduceClausesThresh = 2000;
  m->reduceClausesThresh = (m->reduceClausesThresh + m->learned->size) > 5000 ? 5000 : m->reduceClausesThresh;

#ifdef STATS
  fprintf(stdout, "============================[ Search Statistics ]==============================\n");
  fprintf(stdout, "| Conflicts |          ORIGINAL         |          LEARNT          | Progress |\n");
  fprintf(stdout, "|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |\n");
  fprintf(stdout, "===============================================================================\n");
#endif
  
  iter = 0;
  m->preTotalLearnedCl = m->nTotalLearnedClauses;
  m->preTotalLearnedLit = m->nTotalLearnedLits;
  m->preJumpCl = m->nTotalLearnedClauses;

  while(m->status == 2) {

#ifdef STATS
    fprintf(stdout, "| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", 
            (int)m->nTotalLearnedClauses, (int)m->variableHeap->size, 
            (int)m->clauses->size, (int)m->nCurClauseLits, 
            (int)m->reduceClausesThresh, (int)m->learned->size, 
            (double)m->nCurLearnedLits/m->learned->size, 
            m->progress*100); 
    fflush(stdout);
#endif
    sat_dpll(m, (long)nConflicts);
    
#ifdef LUBY_RESTART
    sat_generate_next_restart_bound(m);
    nConflicts = m->restartFirst * m->restartInc;
    m->preLearnedPos = m->learned->size;
#else
    nConflicts *= m->restartInc;
    m->reduceClausesThresh *= m->learnedSizeInc;
#endif

    iter++;
  }

#ifdef STATS
  fprintf(stdout, "| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", 
            (int)m->nTotalLearnedClauses, (int)m->variableHeap->size, 
            (int)m->clauses->size, (int)m->nCurClauseLits, 
            (int)m->reduceClausesThresh, (int)m->learned->size, 
            (double)m->nCurLearnedLits/m->learned->size, 
            m->progress*100); 
    fflush(stdout);
    fprintf(stdout, "===============================================================================\n"); 
#endif

}

void
sat_generate_next_restart_bound(satManager_t *m)
{
int pvalue;

#ifdef LUBY_RESTART
  pvalue = 1;
  pvalue = (pvalue << m->restartIndex);
  if(m->restartInc == pvalue) {
    m->restartIndex++;
    m->restartInc = 1;
  }
  else {
    m->restartInc = (m->restartInc << 1);
  }

#endif
  return;
}

void
sat_estimate_progress(satManager_t *m)
{
double progress;
double f;
long i, level;
long beg, end;

  progress = 0;
  f = 1.0/m->nVars;
  level = m->decisionStackSeperator->size;
  level = level>10?10:level;
  for(i=0; i<level; i++) {
    beg = i==0 ? 0 : m->decisionStackSeperator->space[i-1];
    end = i==level ? m->stackPos : m->decisionStackSeperator->space[i];
    progress += pow(f, (double)i) * (end-beg);
  }

  progress = progress/m->nVars;
  if(m->progress < progress)    m->progress = progress;
  return;
}


satClause_t *
sat_add_theory_conflict_clause(satManager_t *m, satArray_t *learned)
{
satClause_t *c;

  if(learned->size == 1) {
    c = sat_new_clause(learned, 1);
    m->learned = sat_array_insert(m->learned, (long)c);
    sat_enqueue_check(m, learned->space[0], c);
    m->nCurLearnedLits ++; m->nCurLearnedClauses++;
    m->nTotalLearnedLits ++; m->nTotalLearnedClauses++;
  }
  else {
    c = sat_new_clause(learned, 1);
    m->learned = sat_array_insert(m->learned, (long)c);
    sat_add_watched_literal(m, c);
    sat_update_clause_activity(m, c);
    sat_enqueue_check(m, learned->space[0], c);
/**
    sat_print_clause_simple(m, c);
    fprintf(stdout, "\n");
    fprintf(stdout, " size of learned %d ", m->nCurLearnedLits);
    fprintf(stdout, " %d ", (int)m->stackPos);
    fprintf(stdout, " %10g\n", m->varInc);
    sat_print_clauses(m, m->learned);
**/
  }

#if 0
  sat_print_clause(m, c);
  fprintf(stdout, "\n");
  fflush(stdout);
#endif
  return(c);
}

satClause_t *
sat_add_blocking_clause(satManager_t *m, satArray_t *learned)
{
satClause_t *c;
long level, tmp, i, j, lit, v, levelLitIndex;

  level = SATCurLevel(m);
  levelLitIndex = 0;
  for(i=j=0; i<learned->size; i++) {
    lit = learned->space[i];
    v = lit >> 1;
    if(m->levels[v] != 0) {
      if(m->levels[v] == level) 
        levelLitIndex = j;
      learned->space[j++] = lit;
    }
  }
  learned->size -= (i-j);
  tmp = learned->space[0];
  learned->space[0] = learned->space[levelLitIndex];
  learned->space[levelLitIndex] = tmp;

  if(learned->size == 1) {
    c = sat_new_clause(learned, 2);
    m->blocking = sat_array_insert(m->blocking, (long)c);
    m->nCurLearnedLits ++; m->nCurLearnedClauses++;
    m->nTotalLearnedLits ++; m->nTotalLearnedClauses++;
  }
  else {
    c = sat_new_clause(learned, 2);
    m->blocking = sat_array_insert(m->blocking, (long)c);
    /*    sat_update_clause_activity(m, c); */
    sat_add_watched_literal(m, c);
/**
    sat_print_clause_simple(m, c);
    fprintf(stdout, "\n");
    fprintf(stdout, " size of learned %d ", m->nCurLearnedLits);
    fprintf(stdout, " %d ", (int)m->stackPos);
    fprintf(stdout, " %10g\n", m->varInc);
    sat_print_clauses(m, m->learned);
**/
  }
  m->nCurBlockingLits += learned->size;
  m->nCurBlockingClauses++;
  m->nTotalBlockingLits += learned->size;
  m->nTotalBlockingClauses++;
  return(c);
}

void
sat_add_blocking_clause_for_theorem_prover(satManager_t *m, satArray_t *arr)
{
satClause_t *c;
long level, tmp, i, j, lit, v, levelLitIndex;
long bLevel, nMarks, iLit;

  level = SATCurLevel(m);
  levelLitIndex = 0;
  nMarks = 0;
  bLevel = 0;
  for(i=j=0; i<arr->size; i++) {
    lit = arr->space[i];
    v = lit >> 1;
    if(m->levels[v] == 0)
      continue;
    if(m->levels[v] == level) {
      levelLitIndex = j;
      nMarks++;
    }
    else if(m->levels[v] > bLevel) {
      bLevel = m->levels[v];
    }
    arr->space[j++] = lit;
  }
  arr->size -= (i-j);
  tmp = arr->space[0];
  arr->space[0] = arr->space[levelLitIndex];
  arr->space[levelLitIndex] = tmp;
  
#if 0
  fprintf(stdout, "Blocking clause generated nMarks %ld bLevel %ld\n", nMarks, bLevel);
  sat_print_clause_array(m, arr);
  fprintf(stdout, "\n");
#endif
  c = sat_new_clause(arr, 2);
  if(nMarks > 1) {
    bLevel = sat_conflict_analysis(m, c);
    /** add a conflict clause if on-the-fly subsumption  
     *  replaced a clause with the newly found conflict clause.
     **/
    if (m->clearned->size > 0) {
      if(c->dependent)
        free(c->dependent);
      free(c);
      sat_undo(m, bLevel);
      c = sat_add_learned_clause(m, m->clearned);
    }
#if 0
    fprintf(stdout, "Result of conflict analysis bLevel %ld\n", bLevel);
    sat_print_clause(m, c);
    fprintf(stdout, "\n");
#endif
  }
  else {
    sat_undo(m, bLevel);

    m->blocking = sat_array_insert(m->blocking, (long)c);
    iLit = (c->lits[0]);
    if(arr->size == 1) {
      sat_enqueue_check(m, iLit, 0);
    }
    else {
      sat_add_watched_literal(m, c);
      sat_enqueue_check(m, iLit, c);
    }
    m->nCurBlockingLits += arr->size;
    m->nCurBlockingClauses++;
    m->nTotalBlockingLits += arr->size;
    m->nTotalBlockingClauses++;
  }
}

satClause_t *
sat_add_theory_clause(satManager_t *m, satArray_t *learned)
{
satClause_t *c;
/* long level, tmp, i, lit, v; */

/**
  if(learned->size == 1) {
    c = sat_new_clause(learned, 1);
  }
  else {
    level = SATCurLevel(m);
    for(i=0; i<learned->size; i++) {
      lit = learned->space[i];
      v = lit>>1;
      if(m->levels[v] == level) {
        tmp = learned->space[0];
        learned->space[0] = learned->space[i];
        learned->space[i] = tmp;
        break;
      }
    }
**/
/**
  if(learned->size == 2) {
    c = sat_add_clause(m, learned, 4);
  }
  else {
  **/

    c = sat_new_clause(learned, 4);
#ifdef SMT_ADD_THEORY
    if (m->enableAddTheoryClause) {
      m->theory = sat_array_insert(m->theory, (long)c);
      sat_add_watched_literal(m, c);
      sat_update_clause_activity(m, c);
    }
#endif
 /* } */

  return(c);
}

#if 1
void
sat_dpll(satManager_t *m, long nConflicts)
{
long bLevel, lit;
long previousStackPointer;
long nLearnedClauses;
satClause_t *conflicting, *c;

  m->nRestarts++;
  m->nCurConflicts = 0;
  previousStackPointer = 0; 

  while(1) {
    conflicting = sat_implication(m);
    if(conflicting) {
      m->nConflicts++; m->nCurConflicts++;
      if(SATCurLevel(m) == 0) {
        if(m->coreGeneration) {
          m->nullClause = conflicting;
        }
        m->status = 0;
        return;
      }

      nLearnedClauses = m->learned->size;
      bLevel = sat_conflict_analysis(m, conflicting);

      /** add a conflict clause if on-the-fly subsumption  
       *  replaced a clause with the newly found conflict clause.
       **/
      if (m->clearned->size > 0) {
        sat_undo(m, bLevel);

        previousStackPointer = m->stackPos;

        c = sat_add_learned_clause(m, m->clearned);
        if(m->coreGeneration)
          sat_make_dependent_graph(m, c);
      }
      else {
        if (m->learned->size > nLearnedClauses) {
          sat_undo(m, bLevel);
          previousStackPointer = m->stackPos;
        }
        else {
          /* stackPos was increased at the conflict analysis */
          previousStackPointer = m->stackPos - 1;       
        }
      }
      sat_update_variable_decay(m);
      sat_update_clause_decay(m);
      
      if(m->maxContiguousLevel > m->maxContiguousLimit) {
        nConflicts = m->nCurConflicts;
        m->mcla[m->maxContiguousLevel]++;
        if(m->maxContiguousLevel >= HS_INDEX)
          m->mclaTotal++;
        m->maxContiguousLevel = 0;
      }
      sat_calculate_restart_bound_new(m);

    }
    else {
      if(nConflicts >= 0 && m->nCurConflicts >= nConflicts) {
        sat_estimate_progress(m);
        sat_undo(m, 0);
        return;
      }
      if(SATCurLevel(m) == 0 && m->enableSimplify) {
        previousStackPointer = 0;
        sat_simplify(m);
        if(m->status != 2)      return;
      }
      if(m->reduceClausesThresh >= 0 && 
        m->learned->size-m->stackPos-m->n2LitClauses>= m->reduceClausesThresh) {
        sat_reduce_learned_clauses(m);
      }
#ifdef HAVE_LIBGMP
      if(m->allSat) {
        if(smt_get_size_of_atomic_variable(m)<<2 < m->theory->size) {
          sat_reduce_theory_clauses(m);
        }

        if((m->reduceClausesThresh>>4) < m->blocking->size) {
          sat_reduce_blocking_clauses(m);
        }
        /** 
         * 1. send information of implied variables to theory solver
         * 2. call thoery solver with partial assignment
         *    then check feasibility of theory
         *    if conflict happens then find explanation
         *    otherwise do theory propagation.
         * 3. If conflict occurs put explanation into CNF database
         **/
        int flag;
        
        flag = smt_call_theory_solver(m, previousStackPointer);
        if(flag == 2 && m->status == 0) {
          /** UNSATISFIABLE **/
          return;
        } else if(flag == 3) {
          /** bound computed in level 0 **/
          m->status = 3;
          return;
        } else if(flag == 4) {
          /** bound computed in level 0 and theory prop **/
          previousStackPointer = m->stackPos;
          return;
        }
        if(flag == 1) {
          previousStackPointer = m->stackPos;
          continue;
        }
        else if(flag == 2) {
          /** -1 is required because there is implied literal **/
          previousStackPointer = m->stackPos-1;
          continue;
        }
      }
#else
      if (previousStackPointer) previousStackPointer = 0; /* HK : dummy assignment */
#endif
      sat_decide_polarity_new(m);
      /* nLearned = m->learned->size*4;
      sat_decide_restart(m, (long)nLearned);
      */
      m->nDecisions++;
      lit = sat_make_decision(m);
      
      if(lit == 0){
#ifdef HAVE_LIBGMP
        int flag;
        if(m->allSat) {
          flag = smt_call_theory_solver(m, previousStackPointer);
          if(flag >= 2 && m->status == 0) {
            /** UNSATISFIABLE **/
            return;
          }
          if(flag == 1) {
           previousStackPointer = m->stackPos;
            continue;
          }
          else if(flag >= 2) {
            previousStackPointer = m->stackPos-1;
            continue;
          }
        }
#endif
        m->status = 1;
        return;
      }

      m->decisionStackSeperator = 
          sat_array_insert(m->decisionStackSeperator, m->stackPos);
      previousStackPointer = m->stackPos;
      sat_enqueue(m, lit, 0);
    }
  }
}
#endif

void
sat_calculate_restart_bound_new(satManager_t *m)
{
  double ht_divide_ratio;
  int hs_index;
  int he_index;
  int te_index;
  int i;
  double slope;
  double n=0, yaxis=0, sumx=0, sumx2=0, sumxy=0, sumy=0, sumy2=0;
  double xaxis;
  int ttotal;

  if(m->enableFrequentRestart == 0) {
    m->maxContiguousLimit = 256;
    return;
  }
  if(m->mclaTotal < 128)        return;
  ht_divide_ratio = 0.90;
  hs_index = HS_INDEX;
  he_index = m->maxContiguousLimit+1;
  if(m->mcla[he_index] > 5) {
    ttotal = m->mcla[he_index]; 
    while(ttotal>1) {
      m->mcla[he_index] = ttotal/2;
      ttotal = ttotal - ttotal/2;
      he_index++;
    }
    m->mcla[he_index] = ttotal;
  }

  while(1) {
    if(m->mcla[he_index] > 0)   break;
    he_index--; 
  }
  n = 0;
  for(i=hs_index; i<=he_index; i++) {
    if(m->mcla[i] == 0) continue;
    yaxis = log(m->mcla[i]);
/**
    if(m->mcla[i] == 0) yaxis = 0;
    else yaxis = log(m->mcla[i]);
**/
    sumx += i;
    sumx2 += i*i;
    sumxy += i*yaxis;
    sumy += yaxis;
    sumy2 += yaxis*yaxis;
    n = n+1;
  }
/**
**/
  xaxis = (n*sumx2 - sqrt(sumx));
/**
  fprintf(stdout, "xaxis %f\n", xaxis);
  fprintf(stdout, "slope %f\n", n*sumxy - sumx*sumy);
  fprintf(stdout, "yaxis %f\n", sumy*sumx2 - sumx*sumxy);
**/
  slope = (n*sumxy - sumx*sumy)/xaxis;
  yaxis = (sumy*sumx2 - sumx*sumxy)/xaxis;
  xaxis = (-yaxis)/slope;

/**
  fprintf(stdout, "n %f sumxy %f sumx %f sumy %f sqrt(sumx) %f\n", n, sumxy, sumx, sumy, sqrt(sumx));
  for(i=hs_index; i<=he_index; i++) {
    fprintf(stdout, "%4d ", m->mcla[i]);
  }
  fprintf(stdout, "\n");
  for(i=hs_index; i<=he_index; i++) {
    fprintf(stdout, "%.2f ", log(m->mcla[i]));
  }
  fprintf(stdout, "\n");
  fprintf(stdout, "slope %f y %f x %f\n", slope, yaxis, (double)xaxis);
**/
#if 1
  if(m->maxContiguousLimit/2 < xaxis)
    te_index = xaxis;
  else 
    te_index = m->maxContiguousLimit;
#endif
  if(xaxis < 0) {
    te_index = m->maxContiguousLimit * 1.2;
  }
  if(te_index < 10)
    m->maxContiguousLimit = 10;
    else if(te_index < 256) { // 50 at 07.20
    m->maxContiguousLimit = (double)(te_index-hs_index)*ht_divide_ratio + hs_index;
  }
  /*fprintf(stdout, "Bound == %d (%d %d) %f\n", m->maxContiguousLimit,
   * hs_index, te_index, xaxis); */
  fflush(stdout);
  
  memset(m->mcla, 0, sizeof(int)*m->mclaSize);
  m->mclaTotal = 0;
  m->maxContiguousData[0] = 0;
  m->maxContiguousData[1] = 0;
  m->maxContiguousData[2] = 0;
  m->maxContiguousData[3] = 0;
  m->maxContiguousData[4] = 0;
  m->maxContiguousData[5] = 0;
}





void
sat_decide_polarity(satManager_t *m) 
{
double avgLit;
long nLearnedClauses;
long nLearnedLits;
long limit;

  limit = (m->reduceClausesThresh>>6);
  limit = limit>256 ? 256 : limit;
  limit = limit<64 ? 64 : limit;
  nLearnedClauses = m->nTotalLearnedClauses-m->preTotalLearnedCl;
  if(nLearnedClauses > limit) {
/**
    if(m->polarityMode == 2)    
      m->polarityMode = 0;
**/
    nLearnedLits = m->nTotalLearnedLits-m->preTotalLearnedLit;
    avgLit = (double)nLearnedLits/(double)nLearnedClauses;
    /**
    if(preAvgLit < avgLit) {
      m->defaultSign = m->defaultSign ^ 1;
      m->polarityMode++;
      m->polarityMode = m->polarityMode%3;
    }
    **/
    if(m->preLit+2 < avgLit) {
      m->defaultSign = m->defaultSign ^ 1;
      m->nPolarityChange++;
    }
    /**
    fprintf(stdout, "average jump %10.1f average level %10.1f DEFAULT %d\n",
            avgJump, avgLevel, m->defaultSign);
    fflush(stdout);
    **/

    /**
    if(avgJump < 2)
      sat_change_search_direction(m);
    **/

    m->preLit = avgLit;
    m->preTotalLearnedCl = m->nTotalLearnedClauses;
    m->preTotalLearnedLit = m->nTotalLearnedLits;
  }
}

void
sat_decide_polarity_new(satManager_t *m) 
{
double avgLit;
long nLearnedClauses;
long nLearnedLits;

  nLearnedClauses = m->nTotalLearnedClauses-m->preTotalLearnedCl;
  if(nLearnedClauses > m->polarityChangeLimit) {
    nLearnedLits = m->nTotalLearnedLits-m->preTotalLearnedLit;
    avgLit = (double)nLearnedLits/(double)nLearnedClauses;

    if((m->preLit+2.0000000001) < avgLit) {
      m->defaultSign = m->defaultSign ^ 1;
      m->nPolarityChange++;
    }
    m->preLit = avgLit;
    m->preTotalLearnedCl = m->nTotalLearnedClauses;
    m->preTotalLearnedLit = m->nTotalLearnedLits;
    m->polarityChangeLimit = (double)m->polarityChangeLimit * 1.6;
    if(m->polarityChangeLimit > 256)
      m->polarityChangeLimit = 64;
  }
}

void
sat_decide_restart(satManager_t *m, long nLearned) 
{
double avgJump, avgLevel;
long nLearnedClauses;
long limit, levelLimit;
long implePerDecision;
long maxLevel;

  limit = nLearned>>6;
  limit = limit<64 ? 64 : limit;

  nLearnedClauses = m->nTotalLearnedClauses-m->preJumpCl;
/**
  if(nLearnedClauses > limit && m->decisionStackSeperator->size > 8) {
**/
  if(nLearnedClauses > limit) {
    if(m->decisionStackSeperator->size < 2) {
      m->preJumpCl = m->nTotalLearnedClauses;
      m->nJump = 0;
      m->nLevel = 0;
      return;
    }
    implePerDecision = m->stackPos-m->decisionStackSeperator->space[0];
    implePerDecision = implePerDecision/(m->decisionStackSeperator->size+1);
    implePerDecision = implePerDecision == 0 ? 1 : implePerDecision;
    maxLevel = m->variableHeap->size/implePerDecision;
    levelLimit = maxLevel>>3;

    avgJump = (double)m->nJump/(double)nLearnedClauses;
    avgLevel = (double)m->nLevel/(double)nLearnedClauses;

/**
    fprintf(stdout, "%d %d %d %10g %10g\n", 
            (int)implePerDecision, (int)maxLevel, (int)levelLimit, 
            avgJump, avgLevel);
**/

    levelLimit = levelLimit<4 ? 4 : levelLimit;

    if(avgJump<2 && avgLevel>(levelLimit)) {
      sat_estimate_progress(m);
      sat_undo(m, 0);
      m->nForceRestart++;
    }
    else if(avgJump<1.5) {
      sat_estimate_progress(m);
      sat_undo(m, 0);
      m->nForceRestart++;
    }
#if 0
    if(avgJump<2.5 && avgLevel>(levelLimit)) {
      sat_estimate_progress(m);
      sat_undo(m, 0);
      m->nForceRestart++;
    }
    else if(avgJump<2.0 && avgLevel>(levelLimit<<1)) {
      sat_estimate_progress(m);
      sat_undo(m, 0);
      m->nForceRestart++;
    }
    else if(avgJump<1.5 && avgLevel>(levelLimit<<2)) {
      sat_estimate_progress(m);
      sat_undo(m, 0);
      m->nForceRestart++;
    }
#endif
    m->preJumpCl = m->nTotalLearnedClauses;
    m->nJump = 0;
    m->nLevel = 0;
  }
  return;
}

long 
sat_make_decision(satManager_t *m)
{
long next, lit, v;
long index;


  next = 0;
  if(m->useRandom && 
     sat_drand(m) < m->randomFrequency && 
     m->variableHeap->size != 0) {
    index = (long)(sat_drand(m) * m->variableHeap->size);
    next = m->variableHeap->heap[index];
    if(next > 0 && m->values[next] == 2)        m->nRandomDecisions++;
  }

  if(m->usePreviousDecisionHistory) {
    while(m->previousDecisionHistory->size) {
      m->nTHistoryDecisions++;
      lit = m->previousDecisionHistory->space[m->previousDecisionHistory->size-1];
      v = lit>>1;
      if(m->values[v] == 2) {
        m->previousDecisionHistory->size--;
        m->nHistoryDecisions++;
        return(lit^1);
      }
      m->previousDecisionHistory->size--;
    }
  }

  while(next==0 || m->values[next] != 2) {
    if(m->variableHeap->size == 0) {
      next = 0;
      break;
    }
    else 
      next = sat_heap_remove_min(m, m->variableHeap);
  }
  /**
  if(m->polarityMode == 2) {
    m->defaultSign = m->defaultSign ^ 1;
  }
  **/
  lit = next == 0 ? 0 : ((next<<1) + m->defaultSign);

  return(lit);
}

double
sat_drand(satManager_t *m)
{
long q;

  m->randomSeed *= 1389796;
  q = (long)(m->randomSeed/ 2147483647);
  m->randomSeed -= (double)q * 2147483647;
  return(m->randomSeed/2147483647);
}

void
sat_change_search_direction(satManager_t *m)
{
long i, csize, lit, v, size;
satArray_t *learned;
satClause_t *c;

  sat_sort_clause_array(m->learned, compare_sort_learned);
  learned = m->learned;
  size = learned->size/2;
  for(i=0; i<size; i++) {
    c = (satClause_t *)learned->space[i];
    csize = SATSizeClause(c);
    lit = c->lits[0];
    v = lit>>1;
    if(csize > 2 && 
       !((m->values[v]^SATSign(lit)) == 1)) {
      sat_update_variable_activity(m, v);
    }
  }
}

void
sat_reduce_learned_clauses(satManager_t *m)
{
long i, j, k;
double limit;
long v, size, csize;
satClause_t *c;
satArray_t *learned;

  m->nReduceClauses++;
  limit = m->clauseInc / (double)m->learned->size;

  learned = m->learned;

  sat_sort_clause_array(m->learned, compare_sort_learned);

  for(k=learned->size-1; k>=0; k--) {
    c = (satClause_t *)learned->space[k];
    csize = SATSizeClause(c);
    if(csize > 2)
      break;
  }
  m->n2LitClauses = learned->size - k;

  size = k>>1;
  for(i=j=0; i<size; i++) {
    c = (satClause_t *)learned->space[i];
    csize = SATSizeClause(c);
    v = (c->lits[0]>>1);
    if(csize > 2 && 
       !(m->antes[v] == c && (m->values[v]^SATSign(c->lits[0])) == 1)) {
      if(m->coreGeneration) {
        m->deleted = sat_array_insert(m->deleted, (long)c);
        sat_delete_watched_literal(m, c);
      }
      else 
        sat_delete_clause(m, c);
    }
    else
      learned->space[j++] = learned->space[i];
  }

  size = k;
  for(; i<size; i++) {
    c = (satClause_t *)learned->space[i];
    csize = SATSizeClause(c);
    v = (c->lits[0]>>1);
    if(csize > 2 && 
       !(m->antes[v] == c && (m->values[v]^SATSign(c->lits[0])) == 1) &&
       c->info.activity < limit)       
      if(m->coreGeneration) {
        m->deleted = sat_array_insert(m->deleted, (long)c);
        sat_delete_watched_literal(m, c);
      }
      else 
        sat_delete_clause(m, c);
    else
      learned->space[j++] = learned->space[i];
  }

  size = learned->size;
  for(; i<size; i++) {
    learned->space[j++] = learned->space[i];
  }

  learned->size -= (i-j);
  m->reduceClausesThresh = (double)m->reduceClausesThresh * m->learnedSizeInc;

}

void
sat_reduce_blocking_clauses(satManager_t *m)
{
long i, j, k;
double limit;
long v, size, csize;
satClause_t *c;
satArray_t *learned;

  limit = m->clauseInc / (double)m->blocking->size;
  learned = m->blocking;

#if 0
  k = learned->size;
  size = k;
  for(i=j=0; i<size; i++) {
    c = (satClause_t *)learned->space[i];
    csize = SATSizeClause(c);
    v = (c->lits[0]>>1);
    if(csize > 2 && 
       !(m->antes[v] == c && (m->values[v]^SATSign(c->lits[0])) == 1) &&
       c->info.activity < limit) {     
      if(m->coreGeneration) {
        m->deleted = sat_array_insert(m->deleted, (long)c);
        sat_delete_watched_literal(m, c);
      }
      else 
        sat_delete_clause(m, c);
    }
    else
      learned->space[j++] = learned->space[i];
  }
#endif

#if 1
  k = learned->size;
  size = (k>>1);
  for(i=j=0; i<size; i++) {
    c = (satClause_t *)learned->space[i];
    csize = SATSizeClause(c);
    v = (c->lits[0]>>1);
    if(csize > 2 && 
       !(m->antes[v] == c && (m->values[v]^SATSign(c->lits[0])) == 1)) {
      if(m->coreGeneration) {
        m->deleted = sat_array_insert(m->deleted, (long)c);
        sat_delete_watched_literal(m, c);
      }
      else 
        sat_delete_clause(m, c);
    }
    else
      learned->space[j++] = learned->space[i];
  }

  size = k;
  for(; i<size; i++) {
    c = (satClause_t *)learned->space[i];
    csize = SATSizeClause(c);
    v = (c->lits[0]>>1);
    if(csize > 2 && 
       !(m->antes[v] == c && (m->values[v]^SATSign(c->lits[0])) == 1) &&
       c->info.activity < limit)       
      if(m->coreGeneration) {
        m->deleted = sat_array_insert(m->deleted, (long)c);
        sat_delete_watched_literal(m, c);
      }
      else 
        sat_delete_clause(m, c);
    else
      learned->space[j++] = learned->space[i];
  }
#endif

  size = learned->size;
  for(; i<size; i++) {
    learned->space[j++] = learned->space[i];
  }

  learned->size -= (i-j);
  /**
  fprintf(stdout, "reduced clause %d out of %d\n", i-j, k);
  fprintf(stdout, "current learned lit %d ", m->nCurLearnedLits);
  fprintf(stdout, "%10g\n",  m->clauseInc);
  **/
}

int 
compare_sort_variable_id(const void *x1, const void *y1)
{
long x, y;
  x = (long)x1; x = x>>1;
  y = (long)y1; y = y>>1;
  return(x < y);
}

int 
compare_sort_learned(const void *x1, const void *y1)
{
satClause_t *x, *y;
  x = (satClause_t *)x1;
  y = (satClause_t *)y1;
  return(SATSizeClause((x)) > 2 && 
        ( SATSizeClause((y)) <= 2 || (x)->info.activity < (y)->info.activity));
}

int 
compare_sort_theory(const void *x1, const void *y1)
{
satClause_t *x, *y;
  x = (satClause_t *)x1;
  y = (satClause_t *)y1;
  return((x)->info.activity < (y)->info.activity);
}

int 
compare_sort_block(const void *x1, const void *y1)
{
satClause_t *x, *y;
  x = (satClause_t *)x1;
  y = (satClause_t *)y1;
  return((x)->info.activity > (y)->info.activity);
}

void
sat_reduce_theory_clauses(satManager_t *m)
{
long i, j;
double limit;
long v, size;
/** long csize; **/
satClause_t *c;
satArray_t *theory;


  sat_sort_clause_array(m->theory, compare_sort_theory);

  theory = m->theory;

  limit = 0;
  limit = m->clauseInc / (double)m->theory->size;
  limit = 1;
  size = (theory->size>>1);

  for(i=j=0; i<size; i++) {
    c = (satClause_t *)theory->space[i];
    /**csize = SATSizeClause(c);**/
    v = (c->lits[0]>>1);
    /**
    if(csize > 2 && 
       !(m->antes[v] == c && (m->values[v]^SATSign(c->lits[0])) == 1))
       **/
    if(!(m->antes[v] == c && (m->values[v]^SATSign(c->lits[0])) == 1))
      sat_delete_clause(m, c);
    else
      theory->space[j++] = theory->space[i];
  }

  size = theory->size;
  for(; i<size; i++) {
    c = (satClause_t *)theory->space[i];
    /**csize = SATSizeClause(c);**/
    v = (c->lits[0]>>1);
    /**
    if(csize > 2 && 
       !(m->antes[v] == c && (m->values[v]^SATSign(c->lits[0])) == 1) &&
       c->info.activity < limit)       
       **/
    if(!(m->antes[v] == c && (m->values[v]^SATSign(c->lits[0])) == 1) &&
       c->info.activity < limit)       
      sat_delete_clause(m, c);
    else
      theory->space[j++] = theory->space[i];
  }

  theory->size -= (i-j);
  /**
  fprintf(stdout, "reduced theory clauses %d\n", i-j);
  fprintf(stdout, "current learned lit %d ", m->nCurLearnedLits);
  fprintf(stdout, "%10g\n",  m->clauseInc);
  **/
}



int
sat_is_redundant_lit(satManager_t *m, long oLit, long absLevel)
{
satArray_t *cclearned, *redundant;
satClause_t *c;
int top, i, j;
long v, csize, lit;

  if(m->coreGeneration) return(0);

  c = 0;
  redundant = m->redundant;
  redundant->size = 0;
  m->temp->size = 0;
  redundant = sat_array_insert(redundant, oLit);
  cclearned = m->cclearned;
  top = cclearned->size;

  if(m->coreGeneration) 
    m->temp = sat_array_insert(m->temp, (long)m->antes[oLit>>1]);
  while(redundant->size > 0) {
    redundant->size--;
    c = m->antes[(redundant->space[redundant->size])>>1];
    csize = SATSizeClause(c);
    for(i=0; i<csize; i++) {
      lit = c->lits[i];
      v = lit>>1;
      if(!m->marks[v] && m->levels[v] > 0) {
        if(m->antes[v] != 0 && (sat_abstract_level(m, v) & absLevel)) {
          m->marks[v] = 1;
          redundant = sat_array_insert(redundant, lit);
          cclearned = sat_array_insert(cclearned, lit);
          if(m->coreGeneration) 
            m->temp = sat_array_insert(m->temp, (long)m->antes[lit>>1]);
        }
        else {
          for(j=top; j<cclearned->size; j++) 
            m->marks[(cclearned->space[j]>>1)] = 0;
          cclearned->size = top;
          m->cclearned = cclearned;
          m->redundant = redundant;
          m->temp->size = 0;
          return(0);
        }
      }
    }
  }
  m->cclearned = cclearned;
  if(m->coreGeneration) {
    for(j=0; j<m->temp->size; j++) 
      c = (satClause_t *)m->temp->space[j];
      m->dependent = sat_array_insert(m->dependent, (long)c);
  }
  m->redundant = redundant;
  m->temp->size = 0;
  return(1);
}

int
sat_minimize_conflict(satManager_t *m, long v, int depth)
{
int level, res;
  if(!m->minimizeConflict) return(0);

  if(m->removable[v])   return 1;
  if(m->unremovable[v]) return 0;
  if(depth && m->marks[v])      return 1;
  if(m->antes[v] == 0)  return 0;

  level = m->levels[v];
  if(level == 0 && !m->includeLevelZero)        return 0;
  if(depth++ > m->minimizeConflictLimit)        return 0;

  res = 0;
  long lit = (m->values[v] == 0) ? (v<<1)+1 : (v<<1);
  {
    satClause_t *c = m->antes[v];
    int csize = SATSizeClause(c);
    int i;
    for(i=0; i<csize; i++) { 
      long other = c->lits[i];
      if(lit == other)  continue;
      long u = other>>1; 
      if(m->marks[u])   continue;
      if(m->removable[u])       continue;
      if(m->unremovable[u])return 0;
      if(m->levels[u] == 0 && !m->includeLevelZero)     continue;
    }
    for(i=0; i<csize; i++) { 
      long other = c->lits[i];
      if(lit == other)  continue;
      long u = other>>1; 
      if(m->marks[u])   continue;
      if(m->removable[u])       continue;
      if(m->unremovable[u])return 0;
      if(m->levels[u] == 0 && !m->includeLevelZero)     continue;
      if(!sat_minimize_conflict(m, u, depth))   return 0;
    }
    res = 1;
  }
  m->removable[v] = res;
  m->unremovable[v] = res^1;
  /** add variable to stack for cleaning up **/
  m->seen = sat_array_insert(m->seen, v);
  return res;
}

void
sat_cleanup_for_minimize_conflict(satManager_t *m, satArray_t *arr)
{
  int i;
  for(i=0; i<arr->size; i++) {
    long v = arr->space[i];
    m->marks[v] = 0;
    m->removable[v] = 0;
    m->unremovable[v] = 0;
  }
  arr->size = 0;
}


long
sat_conflict_analysis(satManager_t *m, satClause_t *conflicting)
{
long nMarks, i, j, maxI;
long tWidth, mMarks;
long width, depth;
long nEdges, nVertex;
long lit, cLit, bLevel, tLit;
long *pLit;
long v, csize, preV, tv;
long level, nReduction;
long mInc, mIncRef, mIncV, mEdges;
long firstIter;
long pre_size;
long fromBeginning;
long nAllMarks, nResolventLits;
long nDistilled, nLevelZeros, abstract;
int subsumptionCheck, mSelectNextIncV;
int binary;
satClause_t *c;
satClause_t *oc;
satArray_t *clearned, *cclearned;
satClause_t *resolvent;
#ifdef OLD_OCI
satArray_t *arr;
#endif

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

  clearned = m->clearned;
  clearned->size = 0;
  clearned = sat_array_insert(clearned, 0);
  m->dependent->size = 0;
  i = m->stackPos - 1;
  bLevel = lit = 0;
  nMarks = mMarks = 0;
  nEdges = nVertex = 0;
  tWidth = 0;
  mInc = 0;
  mIncV = 0;
  mIncRef = 0;
  mEdges = 0;
  preV = tv = 0;
  oc = conflicting;
  m->previousDecisionHistory->size = 0;
  firstIter = 0;
  pre_size = 0;
  fromBeginning = 0;
  binary = 0;

  do {
    nResolventLits = nAllMarks;
    nLevelZeros = 0;

    c = conflicting;
    
    if(m->coreGeneration)
      m->dependent = sat_array_insert(m->dependent, (long)c);

    if(SATClauseLearned(c) || SATClauseBlock(c))
      sat_update_clause_activity(m, c);

    mIncRef = clearned->size;

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

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

          m->marks[v] = 1;
           
          nAllMarks++;
          sat_update_variable_activity(m, v);
          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->includeLevelZero==0 && m->levels[v]==0) 
          nLevelZeros++;
      }

    }
 
    /** Subsumption check in conflict analysis **/
    if (subsumptionCheck && firstIter > 0) {
      if (resolvent > 0 && (nResolventLits == nAllMarks)) {
        /* previous resolvent is subsumed by current resolvent */

      #ifdef OLD_OCI
        sat_strengthen_clause_in_conflict_analysis(m, resolvent, 0);
        if (nMarks > 1) {
          oc = resolvent;
          nEdges = nVertex = tWidth = 0;
        }
      #else
        sat_queue_insert(m->satQueue, (long)resolvent);
        m->resolvents = sat_array_insert(m->resolvents, tv);
      #endif
  
        if ((csize - nLevelZeros) > nAllMarks) {
          /* delete the antecedent, when antecednet is also subsumed */
          m->nEliminatedClsInConflict++;
          m->nEliminatedLitsInConflict += csize;
        
        #ifdef OLD_OCI
          arr = SATClauseLearned(c) ? m->learned : m->clauses;
          sat_array_delete_elem(arr, (long)c);
          sat_delete_clause(m, c);
        #else
          if (SATClauseOriginal(resolvent) || !SATClauseOriginal(c)) {
            sat_queue_insert(m->satQueue, (long)c);
            m->resolvents = sat_array_insert(m->resolvents, 0);
          }
          else {
            sat_queue_insert(m->satQueue, (long)c);
            m->resolvents = sat_array_insert(m->resolvents, tv);
          } 
        #endif
        }
        m->depthOfOTS += nVertex; 
        nDistilled++;
      }
      else if ((csize - nLevelZeros) > nAllMarks) {
        /* antecedent is subsumed by current resolvent */
        nDistilled++;
        m->depthOfOTS += nVertex; 
        resolvent = c;
         
    #ifdef OLD_OCI
        sat_strengthen_clause_in_conflict_analysis(m, resolvent, 0);
        if (nMarks > 1) {
          oc = resolvent;
          nEdges = nVertex = tWidth = 0;
        }
    #else
        sat_queue_insert(m->satQueue, (long)resolvent);
        m->resolvents = sat_array_insert(m->resolvents, tv);
    #endif
      }
      else 
        resolvent = 0;
    }

    firstIter++;
    tWidth += nMarks;
    nVertex++;
    mMarks = (nMarks > mMarks) ? nMarks : mMarks;

    preV = tv;
    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--;
 
    if(clearned->size-mIncRef >= mInc) { 
      mInc = clearned->size-mIncRef;
      mIncV = preV;
      mEdges = nEdges;
    }
    
  } while(nMarks > 0);

  m->depthOfConflict += nVertex;
  m->nDistillInConflict += nDistilled;
 
  clearned->space[0] = lit^1;
  tLit = lit;
  
  cclearned = m->cclearned;
  cclearned->size = 0;

  nReduction = 0;
  if(clearned->size == 1) 
    bLevel = 0;
  else {
    /** minimize conflict learned clause **/
    m->cclearned = cclearned = sat_array_copy(clearned, m->cclearned);
    for(i=j=1; i<clearned->size; i++) {
      lit = clearned->space[i];
      v = lit >> 1;
      if(m->antes[v] == 0 || !sat_minimize_conflict(m, v, 0)) 
        clearned->space[j++] = lit;
    }
    clearned->size -= (i-j);
    nReduction = (i-j);
    sat_cleanup_for_minimize_conflict(m, m->seen);

    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;
    bLevel = m->levels[lit>>1];

    #ifdef OLD_OCI 
    if (resolvent > 0) {
      lit = clearned->space[1];
      if (resolvent->lits[1] != lit) { 
        sat_array_delete_elem(m->wls[((resolvent->lits[1])^1)], (long)resolvent);
        m->wls[(lit^1)] = sat_array_alloc_insert(m->wls[(lit^1)], (long)resolvent); 
      }
      for (i=1; i<clearned->size; i++) {
        lit = clearned->space[i];
        resolvent->lits[i] = lit;       
      }
      resolvent->size = (clearned->size << SATCsizeShift) | (resolvent->size & SATCMask); 
    }
    #endif
  }

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

/**
  for(j=1; j<clearned->size; j++)
    if(m->levels[(clearned->space[j]>>1)] > 0)
      sat_update_variable_activity(m, (clearned->space[j]>>1));
**/


  m->clearned = clearned;
  m->cclearned = cclearned;

  m->nJump += m->decisionStackSeperator->size - bLevel;
  m->nLevel += m->decisionStackSeperator->size;

  width = (long)((double)tWidth/(double)nVertex+0.5)+1;
  depth = (long)((double)nEdges/(double)width+ 0.5);
  level = m->decisionStackSeperator->size;

  v = clearned->space[0]>>1;
  if(m->antes[v] != 0)  m->nFirstUip++;

  if(m->coreGeneration == 0) {
  
#if 0 
  if(depth > 20 && width < 4 ) {
    if (resolvent == 0 || nReduction > 0)
      m->tlearned = sat_array_copy(m->clearned, m->tlearned);
    sat_conflict_analysis_strong(m, oc, m->clearned->size*3/2, nVertex>>1);
    m->nAuxConflictAnalysis++;
    if (resolvent == 0 || nReduction > 0)
      m->clearned = sat_array_copy(m->tlearned, m->clearned);
  }
#endif

#if 0 
  if(depth > 5 && mIncV && mInc>5 && mInc > clearned->size/3 && mEdges > nEdges/2) {
    if (resolvent == 0 || nReduction > 0)
      m->tlearned = sat_array_copy(m->clearned, m->tlearned);
    sat_conflict_analysis_supplemental(m, oc, mIncV, clearned->size*2/3);
    m->nAuxConflictAnalysis++;
    if (resolvent == 0 || nReduction > 0)
      m->clearned = sat_array_copy(m->tlearned, m->clearned);
  }
#endif
  }

  if(SATClauseBlock(oc))
    oc->info.activity = 0;

  /** Subsumption check in conflict analysis **/
  if (subsumptionCheck) {
    sat_strengthen_set_of_clauses_in_conflict_analysis(m);
 
    if (resolvent > 0) {
      if (nReduction > 0) {
        abstract = 0;
        lit = clearned->space[1];
        if (resolvent->lits[1] != lit) { 
          sat_array_delete_elem(m->wls[((resolvent->lits[1])^1)], (long)resolvent);
          m->wls[(lit^1)] = sat_array_alloc_insert(m->wls[(lit^1)], (long)resolvent); 
        }
        resolvent->size = (clearned->size << SATCsizeShift) | (resolvent->size & SATCMask); 
        
        abstract |= 1 << (SATVar(resolvent->lits[0]) & 31);
        for (i=1; i<clearned->size; i++) {
          lit = clearned->space[i];
          resolvent->lits[i] = lit;     
          abstract |= 1 << (SATVar(lit) & 31);
        }
        if (!SATClauseLearned(resolvent)) 
          resolvent->info.abstract = abstract;
      } 
      m->nOmittedConflictClauses++;
      m->nOmittedConflictLits += m->clearned->size;

      /** For unit conflict clause, we may need to move the clause
       *  strengthened to unit literal into the array of original
       *  clauses if the clause is a learned clause.
       **/
      m->clearned->size = 0;
      sat_undo(m, bLevel);
      sat_enqueue_check(m, resolvent->lits[0], resolvent);
    } 
  }  

  m->conflictLevels[(int)m->nConflicts%5] = m->decisionStackSeperator->size;
  double alevel = ( (double)(m->conflictLevels[0]+m->conflictLevels[1]+m->conflictLevels[2]+m->conflictLevels[3]+m->conflictLevels[4]-m->decisionStackSeperator->size) / 4.0);
  double glevel = alevel - m->decisionStackSeperator->size;
  if(-3.0<glevel && glevel<3.0 && m->decisionStackSeperator->size-bLevel < 9 ) {
    m->maxContiguousLevel++;
  }
  else {
    if(m->maxContiguousDataCollect) {
      if(m->mclaSize <= m->maxContiguousLevel) {
        m->mcla = (int *)realloc((int *)m->mcla, sizeof(int)*(m->mclaSize<<1));
        memset(&m->mcla[m->mclaSize], 0, sizeof(int)*m->mclaSize);
        m->mclaSize = (m->mclaSize<<1);
      }
      m->mcla[m->maxContiguousLevel]++;
      m->maxContiguousLevelTotal += m->maxContiguousLevel;
      m->maxContiguousLevelCount ++;
      if(m->maxContiguousLevel >= HS_INDEX)
        m->mclaTotal++;
    }
    m->maxContiguousLevel = 0;
  }

/**  if(m->tempUnitClauses->size > 0) {
    bLevel = 0;
    sat_undo(m, bLevel);
    for(i=0; i<m->tempUnitClauses->size; i++) {
      c = (satClause_t *)m->tempUnitClauses->space[i];
      sat_enqueue_check(m, c->lits[0], c);
    }
    m->tempUnitClauses->size = 0;
  }
**/
  return(bLevel);
}


void
sat_conflict_analysis_strong(satManager_t *m, satClause_t *conflicting, long sLimit, long implLimit)
{
long nMarks, i, j;
long tWidth, mMarks;
long nEdges, nVertex;

long lit, cLit;
long absLevel, v, csize;
long implL, implR;
satClause_t *c;
satArray_t *clearned, *cclearned;

  clearned = m->clearned;
  clearned->size = 0;
  clearned = sat_array_insert(clearned, 0);
  clearned = sat_array_insert(clearned, 0);
  m->dependent->size = 0;
  i = m->stackPos - 1;
  lit = 0;
  nMarks = mMarks = 0;
  nEdges = nVertex = 0;
  tWidth = 0;
  implL = implLimit*5/10;
  implR = implLimit*15/10;
  

  do {
    c = conflicting;

    if(m->coreGeneration)
      m->dependent = sat_array_insert(m->dependent, (long)c);

    csize = SATSizeClause(c);
    for(j=(lit == 0)?0:1; j<csize; j++) {
      cLit = c->lits[j];
      v = cLit >> 1;
      if(m->levels[v] == SATCurLevel(m))
        nEdges++;
      /**
      if(!m->marks[v] && m->levels[v]>0) {
        m->marks[v] = 1;
        if(m->levels[v] >= SATCurLevel(m))
          nMarks++;
        else {
          clearned = sat_array_insert(clearned, cLit);
        }
      }
      **/

      if(!m->marks[v]) {
        if((m->includeLevelZero==0 && m->levels[v]>0) || m->includeLevelZero==1) {
          m->marks[v] = 1;
          if(m->levels[v] >= SATCurLevel(m))
            nMarks++;
          else {
            clearned = sat_array_insert(clearned, cLit);
          }
        }
      }
    }
    tWidth += nMarks;
    nVertex++;
    mMarks = (nMarks > mMarks) ? nMarks : mMarks;

    while(!(m->marks[(m->decisionStack[i--])>>1]));
    lit = m->decisionStack[i+1];
    v = lit>>1; 
    conflicting = m->antes[v];
    m->marks[v] = 0;
    nMarks--;

   
    if(implL < nVertex && nVertex < implR && clearned->size < sLimit && nMarks == 1) {
      if(m->coreGeneration) 
        m->dependent = sat_array_insert(m->dependent, (long)conflicting);

      clearned->space[1] = lit^1;
      while(!(m->marks[(m->decisionStack[i--])>>1]));
      lit = m->decisionStack[i+1];
      v = lit>>1; 
      m->marks[v] = 0;
      nMarks--;
      clearned->space[0] = lit^1;
      m->depthOfStrong += nVertex;
    }
    else if(clearned->size >= sLimit) {
      do{
        while(!(m->marks[(m->decisionStack[i--])>>1]));
        lit = m->decisionStack[i+1];
        v = lit>>1; 
        m->marks[v] = 0;
        nMarks--;
      }while(nMarks>0);
    }
  } while(nMarks > 0);

  if(clearned->size >= sLimit || clearned->space[0] == 0) {
    m->clearned = clearned;
    for(j=0; j<clearned->size; j++)
      m->marks[(clearned->space[j]>>1)] = 0;
    return;
  }

  cclearned = m->cclearned;
  cclearned->size = 0;

  if(clearned->size == 1);
  else {
    /** 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);
    for(i=j=1; i<clearned->size; i++) {
      lit = clearned->space[i];
      v = lit >> 1;
      if(m->includeLevelZero && m->levels[v] == 0)
        clearned->space[j++] = lit;
      else if(m->antes[v] == 0 || !sat_is_redundant_lit(m, lit, absLevel))
        clearned->space[j++] = lit;
    }
    clearned->size -= (i-j);
  }

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


  m->clearned = clearned;
  m->cclearned = cclearned;

  if(sLimit > clearned->size) {
    c = sat_new_clause(m->clearned, 1);
    m->learned = sat_array_insert(m->learned, (long)c);
    sat_add_watched_literal(m, c);
    
    m->nAuxLearnedClauses++;
    m->nAuxLearnedLits += SATSizeClause(c);

    if(m->coreGeneration)
      sat_make_dependent_graph(m, c);

/**
    if(m->preJump <3)
    sat_update_clause_activity(m, c);
**/
  }

  return;
}

void
sat_conflict_analysis_supplemental(satManager_t *m, satClause_t *conflicting, long refV, long sLimit)
{
long nMarks, i, j;
long tWidth, mMarks;
long nEdges, nVertex;
long lit, cLit;
long absLevel, v, csize;
satClause_t *c;
satArray_t *clearned, *cclearned;

  clearned = m->clearned;
  clearned->size = 0;
  clearned = sat_array_insert(clearned, 0);
  clearned = sat_array_insert(clearned, 0); 
  m->dependent->size = 0;
  i = m->stackPos - 1;
  lit = 0;
  nMarks = mMarks = 0;
  nEdges = nVertex = 0;
  tWidth = 0;

  
  do {
    c = conflicting;
    if(m->coreGeneration)
      m->dependent = sat_array_insert(m->dependent, (long)c);

    csize = SATSizeClause(c);
    for(j=(lit == 0)?0:1; j<csize; j++) {
      cLit = c->lits[j];
      v = cLit >> 1;
      if(m->levels[v] == SATCurLevel(m))
        nEdges++;
      /**
      if(!m->marks[v] && m->levels[v]>0) {
        m->marks[v] = 1;
        if(m->levels[v] >= SATCurLevel(m))
          nMarks++;
        else {
          clearned = sat_array_insert(clearned, cLit);
        }
      }
      **/
      if(!m->marks[v]) {
        if((m->includeLevelZero==0 && m->levels[v]>0) || m->includeLevelZero==1) {
          m->marks[v] = 1;
          if(m->levels[v] >= SATCurLevel(m))
            nMarks++;
          else {
            clearned = sat_array_insert(clearned, cLit);
          }
        }
      }
    }
    tWidth += nMarks;
    nVertex++;
    mMarks = (nMarks > mMarks) ? nMarks : mMarks;

    while(!(m->marks[(m->decisionStack[i--])>>1]));
    lit = m->decisionStack[i+1];
    v = lit>>1; 
    conflicting = m->antes[v];
    m->marks[v] = 0;
    nMarks--;


    if(refV == v) {
      clearned->space[0] = lit^1;
      do{
        if(m->coreGeneration) 
          m->dependent = sat_array_insert(m->dependent, (long)conflicting);
        while(!(m->marks[(m->decisionStack[i--])>>1]));
        lit = m->decisionStack[i+1];
        v = lit>>1; 
        m->marks[v] = 0;
        nMarks--;
        conflicting = m->antes[v];
        if (nMarks > 0) 
          clearned = sat_array_insert(clearned, lit^1);
        else
          clearned->space[1] = lit^1;

      }while(nMarks>0);
      m->depthOfStrong += nVertex; 
    }
  } while(nMarks > 0);

  /**
  if(clearned->size >= sLimit) {
    m->clearned = clearned;
    for(j=0; j<clearned->size; j++)
      m->marks[(clearned->space[j]>>1)] = 0;
    return;
  }
  **/


  cclearned = m->cclearned;
  cclearned->size = 0;

  if(clearned->size == 1); 
  else {
    /** 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);
    for(i=j=1; i<clearned->size; i++) {
      lit = clearned->space[i];
      v = lit >> 1;
      if(m->includeLevelZero && m->levels[v] == 0)
        clearned->space[j++] = lit;
      else if(m->antes[v] == 0 || !sat_is_redundant_lit(m, lit, absLevel))
        clearned->space[j++] = lit;
    }
    clearned->size -= (i-j);
  }

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


  m->clearned = clearned;
  m->cclearned = cclearned;

  if(sLimit > clearned->size) {
    c = sat_new_clause(m->clearned, 1);
    m->learned = sat_array_insert(m->learned, (long)c);
    sat_add_watched_literal(m, c);

    m->nAuxLearnedClauses++;
    m->nAuxLearnedLits += SATSizeClause(c);

    if(m->coreGeneration)
      sat_make_dependent_graph(m, c);

/**
    if(m->preJump <3)
      sat_update_clause_activity(m, c);
**/
  }

  return;
}

void
sat_check_marks(satManager_t *m)
{
long i;

  for(i=0; i<=m->nVars; i++) {
    if(m->marks[i] != 0) {
      fprintf(stdout, "Variable %d@%d is marked\n", (int)i, (int)m->levels[i]);
    }
  }
  fflush(stdout);

}

void
sat_conflict_analysis_for_literal(satManager_t *m, long target)
{
long nMarks, i, j, ti;
long tWidth, mMarks;
long width, depth;
long nEdges, nVertex;
long lit, cLit, bLevel, tLit;
long absLevel, v, csize;
long level;
satClause_t *c;
/** satClause_t *oc; **/
satClause_t *conflicting;
satArray_t *clearned, *cclearned;

  clearned = m->clearned;
  clearned->size = 0;
  clearned = sat_array_insert(clearned, 0);
  i = m->stackPos - 1;
  bLevel = lit = 0;
  nMarks = 0;
  tWidth = 0;
  mMarks = 0;
  nEdges = 0;
  nVertex = 0;

  clearned = sat_array_insert(clearned, target);
  conflicting = m->antes[target>>1];
  /**oc = conflicting; **/
  
  do {
    c = conflicting;

    csize = SATSizeClause(c);
    for(j=(lit == 0)?0:1; j<csize; j++) {
      cLit = c->lits[j];
      v = cLit >> 1;
      if(m->levels[v] == SATCurLevel(m))
        nEdges++;
      if(!m->marks[v] && m->levels[v]>0) {
        m->marks[v] = 1;
        if(m->levels[v] >= SATCurLevel(m))
          nMarks++;
        else {
          clearned = sat_array_insert(clearned, cLit);
          if(m->levels[v] > bLevel)
            bLevel = m->levels[v];
        }
      }
    }
    tWidth += nMarks;
    nVertex++;
    mMarks = (nMarks > mMarks) ? nMarks : mMarks;

    while(!(m->marks[(m->decisionStack[i--])>>1]));
    lit = m->decisionStack[i+1];
    v = lit>>1; 
    conflicting = m->antes[v];
    m->marks[v] = 0;
    nMarks--;
  } while(nMarks > 0);
  clearned->space[0] = lit^1;
  tLit = lit;
  ti = i;

  
  cclearned = m->cclearned;
  cclearned->size = 0;

  if(clearned->size == 1) 
    bLevel = 0;
  else {
    /** 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);
    for(i=j=1; i<clearned->size; i++) {
      lit = clearned->space[i];
      v = lit >> 1;
      if(m->antes[v] == 0 || !sat_is_redundant_lit(m, lit, absLevel))
        clearned->space[j++] = lit;
    }
    clearned->size -= (i-j);
  }

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

  m->clearned = clearned;
  m->cclearned = cclearned;

  width = (long)((double)tWidth/(double)nVertex+0.5)+1;
  depth = (long)((double)nEdges/(double)width+ 0.5);

  if(depth>10 && width > 7 &&
     m->clearned->size<(long)((double)m->nCurLearnedLits/m->learned->size)) {
/**
  if(sat_check_complementary(depth, m->clearned->size, (double)m->nCurLearnedLits/m->learned->size)) {
**/
    c = sat_new_clause(m->clearned, 1);
    m->learned = sat_array_insert(m->learned, (long)c);
    sat_add_watched_literal(m, c);
/**
    sat_update_clause_activity(m, c);
**/
  }

  level = m->decisionStackSeperator->size;
  if(m->antes[tLit>>1] != 0) {
    if(ti-m->decisionStackSeperator->space[level-1] > nVertex<<1) {
      /**
      fprintf(stdout, "mmarks %d, twidth %d, nEdges %d\n", mMarks, tWidth, nEdges);
      fprintf(stdout, "width %d, depth %d\n", width, depth);
      sat_print_dot_for_implication_graph(m, oc, m->decisionStackSeperator->size, 0);
      **/
      sat_conflict_analysis_for_literal(m, tLit);
    }
  }

  return;
}

int
sat_check_complementary(int depth, int nLits, double avg)
{
double diff;
double refDepth;
/*double y; HK*/


  if(depth < 5) return(0);
  diff = (double)nLits - avg;

  if(diff > avg)        return(0);

  refDepth = 10;

  if(diff>0) {
    if(depth < refDepth)        return(0);
    if(nLits < avg*1.5) return(1);
    else                return(0);
    /*y = refDepth*8/avg * diff - refDepth; HK */
  }
  else {
    if(depth > refDepth)        return(1);
    if(nLits < 4)       return(1);
    else                return(0);
  }
  /*if(depth > y)       return(1);
  else          return(0); HK */
}

long
sat_abstract_level(satManager_t *m, long v)
{
  return( 1<<((m->levels[v]) & 31));
}

satClause_t *
sat_implication(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++;

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

      /** It can be implemented using conditional assignment **/
      iLit = lit ^ 1;

      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 = SATSizeClause(c);
        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);
            sat_verify_watched_literal(m, c);
            goto foundWatch;
          }
        }

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


void
sat_undo(satManager_t *m, long level)
{
long i, v;
satHeap_t *h;

  if(SATCurLevel(m) > level) {
    if(m->usePreviousDecisionHistory && level != 0 && SATCurLevel(m)-level < 5) {
      for(i=SATCurLevel(m); i>level; i--) {
        v = m->decisionStack[m->decisionStackSeperator->space[i-1]];
        m->previousDecisionHistory = sat_array_insert(m->previousDecisionHistory, v); 
      }
    }
    h = m->variableHeap;
    for(i=m->stackPos-1; i>=m->decisionStackSeperator->space[level]; i--) {
      v = m->decisionStack[i] >> 1;
      m->values[v] = 2;
      m->levels[v] = -1; /* redundant undo **/

      if(h->indices[v] < 0) /* a variable is not in heap **/
        sat_heap_insert(m, m->variableHeap, v);
    }
    m->curPos = m->decisionStackSeperator->space[level];
    m->stackPos = m->curPos;
    m->decisionStackSeperator->size = level; 
  }
  if(level == -1) {
    m->decisionStackSeperator->size = 0; 
    m->stackPos = 0;
  }
#ifdef HAVE_LIBGMP
  if(m->allSat)
    smt_theory_undo(m);
#endif
}

void
sat_simplify(satManager_t *m)
{
satClause_t *c;
/*int limitVars;*/
long limitVars;

  assert(SATCurLevel(m) == 0);

  if(m->coreGeneration == 1 || m->enableSimplify == 0) 
    return;

  c = sat_implication(m);
  if(c) {
    m->status = 0;
    return;
  }

/**
  fprintf(stdout, "%d %d\n", m->simpDBAssigns, m->simpDBProps);
  if(m->stackPos == m->simpDBAssigns || m->simpDBProps > 0)
    return;
**/
/**
 **/
  limitVars = m->nVars / 100;
  if(limitVars == 0) limitVars = 1;
  if(m->stackPos - m->preLevelZeroStackPos < limitVars || m->simpDBProps > 0) 
    return;
  
  m->nSimplify++;
  sat_remove_satisfied_clauses(m, m->learned);
  sat_remove_satisfied_clauses(m, m->clauses);
  sat_remove_satisfied_clauses(m, m->blocking);
  
  sat_heap_remove_var_assigned_level_zero(m, m->variableHeap);

  m->preLevelZeroStackPos = m->stackPos;

  m->simpDBAssigns = m->stackPos;
  m->simpDBProps = m->nCurClauseLits + m->nCurLearnedLits;

  m->preJumpCl = m->nTotalLearnedClauses;
  m->nJump = 0;
  m->nLevel = 0;
}

void
sat_remove_satisfied_clauses(satManager_t *m, satArray_t *arr)
{
long i, j, k, satisfied;
long csize, lit, v;
satClause_t *c;

  for(i=j=0; i<arr->size; i++) {
    c = (satClause_t *)arr->space[i];
    satisfied = 0;
    csize = SATSizeClause(c);
    if(csize == 1)      {
      arr->space[j++] = arr->space[i];
      continue;
    }
    for(k=0; k<csize; k++) {
      lit = c->lits[k];
      v = lit>>1;
      if((m->values[v] ^ (lit&1)) == 1) {
        satisfied = 1;
        break;
      }
    }

    if(satisfied) sat_delete_clause(m, c);
    else          arr->space[j++] = arr->space[i];
  }
  arr->size -= (i-j);
/**
  fprintf(stdout, "%d simplified\n", i-j);
**/
}

satManager_t *
sat_init_manager()
{
satManager_t *m;

   m = (satManager_t *)malloc(sizeof(satManager_t));
   memset(m, 0, sizeof(satManager_t));

   m->status = 2;
   m->nRestarts = 0;
   m->nFirstUip = 0;;

   m->varDecay = 1.0/0.95;
   m->clauseDecay = 1.0/0.999;
   m->varInc = 1.0;
   m->clauseInc = 1.0;

   m->randomSeed = 91648253;
   m->randomFrequency = 0.02;

#ifdef LUBY_RESTART
   m->restartFirst = 256;
   m->restartInc = 1;
#endif
#ifndef LUBY_RESTART
   m->restartFirst = 100;
   m->restartInc = 1.5;
#endif
   m->learnedSizeFactor = (double)1/(double)3;
   m->learnedSizeInc = 1.1;
   m->polarityChangeLimit = 64;

   m->simpDBAssigns = -1;
   m->simpDBProps = 0;

   m->buildBridge = 1;
   m->useRandom = 1;
   m->defaultSign = 1;
   m->polarityMode = 1;
   m->preJump = 3;
   m->coreGeneration = 0;
   m->includeLevelZero = 0;
   m->enableSimplify = 1;

   m->usePreviousDecisionHistory = 0;
   
   m->enableAddTheoryClause = 1;
   m->enableOptimizeClause = 0;
   
   if(m->coreGeneration) {
     m->includeLevelZero = 1;
     m->enableSimplify = 0;
   }

#ifdef CirCUsCNF
   m->allSat = 0;
#endif
#ifdef CirCUsALLSAT
   m->allSat = 1;
#endif
   m->checkSubsumption = 0;
   if (!m->allSat)
     m->subsumeInConflict = 1;  
   return(m);
}


void
sat_create_database(satManager_t *m)
{
long nVars;
long i;

    m->curPos = 0;
    m->stackPos = 0;
    m->clauses = sat_array_alloc(1024);
    m->learned = sat_array_alloc(1024);
    m->blocking = sat_array_alloc(1024);
    m->theory = sat_array_alloc(1024);
    m->deleted = sat_array_alloc(1024);
    m->shortClauses = sat_array_alloc(1024);
    m->previousDecisionHistory = sat_array_alloc(1024);
    m->seen = sat_array_alloc(16);
    m->tempUnitClauses = sat_array_alloc(16);

    nVars = m->nVars+1;

    m->activity = (double *)malloc(sizeof(double)*nVars);
    m->values = (char *)malloc(sizeof(char)*nVars);
    m->marks = (char *)malloc(sizeof(char)*nVars);
    m->visits = (char *)malloc(sizeof(char)*nVars);
    m->pure = (char *)malloc(sizeof(char)*nVars);
#ifdef CHECK_EQUIVALENCE_RELATION
    m->dummy = (char *)malloc(sizeof(char)*nVars);
    m->equi = (char *)malloc(sizeof(char)*nVars);
    m->maps = (long *)malloc(sizeof(long)*nVars);
#endif

    m->levels = (long *)malloc(sizeof(long)*nVars);
    m->decisionStack = (long *)malloc(sizeof(long)*nVars);
    m->antes = (satClause_t **)malloc(sizeof(satClause_t *)*(nVars));
     
    m->mclaSize = 1024;
    m->mcla = (int *)malloc(sizeof(int)*(m->mclaSize));
    memset(m->mcla, 0, sizeof(int)*m->mclaSize);


    for(i=0; i<nVars; i++) {
      m->activity[i] = 0;
      m->marks[i] = 0;
      m->visits[i] = 0;
      m->pure[i] = 0;
      m->decisionStack[i] = 0;
      m->antes[i] = 0;
      m->levels[i] = -1;
      m->values[i] = 2; 

#ifdef CHECK_EQUIVALENCE_RELATION
      m->dummy[i] = 0;
      m->equi[i] = 0;
      m->maps[i] = 0;
#endif
    }

    m->wls = (satArray_t **)malloc(sizeof(satArray_t *)*(nVars<<1));
    for(i=0; i<(nVars<<1); i++) m->wls[i] = 0;

    m->decisionStackSeperator = sat_array_alloc(1024);
    m->clearned = sat_array_alloc(16);
    m->tlearned = sat_array_alloc(16);
    m->cclearned = sat_array_alloc(16);
    m->redundant = sat_array_alloc(16);
    m->dependent = sat_array_alloc(16);
    m->temp = sat_array_alloc(16);

    m->variableHeap = sat_heap_init(m, sat_compare_activity);

#ifdef SATELITE
    if(m->checkSubsumption) {
      m->subsumptionQueue = sat_queue_alloc(m->nClauses);
      m->elimOrderArray = (long *)malloc(sizeof(long)*nVars);
      memset(m->elimOrderArray, 0, sizeof(long)*nVars);
      m->elimClauses = (satArray_t **)malloc(sizeof(satArray_t*)*nVars);
      memset(m->elimClauses, 0, sizeof(satArray_t *)*nVars);
      m->occurrence = (satArray_t **)malloc(sizeof(satArray_t*)*(nVars));
      memset(m->occurrence, 0, sizeof(satArray_t *)*nVars);
    }
#endif

    m->resolvents = sat_array_alloc(16);
    m->satQueue = sat_queue_init(m->nClauses << 2); 
    if(m->simplify || m->distill || m->subsumeInConflict) {
      
      m->clausesHistogram = (long *)malloc(sizeof(long)*13);
      for (i = 0; i < 13; i++) m->clausesHistogram[i] = 0;

      m->elimtable = sat_array_alloc(4);
      m->candidates = sat_array_alloc(16);
     
      m->litMarks = (char *)malloc(sizeof(char)*(nVars<<1));
      m->scores = (long *)malloc(sizeof(long)*(nVars<<1));
      for(i=0; i<(nVars<<1); i++) {
        m->litMarks[i] = 0;
        m->scores[i] = 0;
      }

      m->equi = (char *)malloc(sizeof(char)*nVars);
      m->maps = (long *)malloc(sizeof(long)*nVars);
      m->bvars = (char *)malloc(sizeof(char)*nVars);
      for(i=0; i<nVars; i++) {
        m->equi[i] = 0;
        m->maps[i] = 0;
        m->bvars[i] = 0;
      }
      vel_heap_init(m, nVars);
    }
}

void
sat_resize_database(satManager_t *m, int numVariables)
{
long nVars, prenVars;
long i;

    if(m->nVars > numVariables)  return;

    prenVars = m->nVars;
    m->nVars = numVariables;
    nVars = m->nVars+1;

    m->activity = (double *)realloc((double *)m->activity, sizeof(double)*nVars);
    m->values = (char *)realloc((char *)m->values, sizeof(char)*nVars);
    m->marks = (char *)realloc((char *)m->marks, sizeof(char)*nVars);
    m->visits = (char *)realloc((char *)m->visits, sizeof(char)*nVars);
    m->pure = (char *)realloc((char *)m->pure, sizeof(char)*nVars);
#ifdef CHECK_EQUIVALENCE_RELATION
    m->dummy = (char *)realloc((char *)m->dummy, sizeof(char)*nVars);
    m->equi = (char *)realloc((char *)m->equi, sizeof(char)*nVars);
    m->maps = (long *)realloc((long *)m->maps, sizeof(long)*nVars);
#endif

    m->levels = (long *)realloc((long *)m->levels, sizeof(long)*nVars);
    m->decisionStack = (long *)realloc((long *)m->decisionStack, sizeof(long)*nVars);
    m->antes = (satClause_t **)realloc((satClause_t **)m->antes, sizeof(satClause_t *)*(nVars));

    for(i=prenVars+1; i<nVars; i++) {
      m->activity[i] = 0;
      m->marks[i] = 0;
      m->visits[i] = 0;
      m->pure[i] = 0;
      m->decisionStack[i] = 0;
      m->antes[i] = 0;
      m->levels[i] = -1;
      m->values[i] = 2; 
#ifdef CHECK_EQUIVALENCE_RELATION
      m->dummy[i] = 0;
      m->equi[i] = 0;
      m->maps[i] = 0;
#endif
    }

    m->wls = (satArray_t **)realloc((satArray_t **)m->wls, sizeof(satArray_t *)*(nVars<<1));
    for(i=((prenVars+1)<<1); i<(nVars<<1); i++) m->wls[i] = 0;

    sat_heap_resize(m, m->variableHeap, prenVars);
}


void
sat_free_manager(satManager_t *m)
{
long size, i;
satArray_t *arr;

  sat_free_clause_array(m->learned);
  if(m->learned) free(m->learned);
  sat_free_clause_array(m->clauses);
  if(m->clauses) free(m->clauses);
  sat_free_clause_array(m->blocking);
  if(m->blocking) free(m->blocking);
  sat_free_clause_array(m->theory);
  if(m->theory) free(m->theory);
  sat_free_clause_array(m->deleted);
  if(m->deleted) free(m->deleted);
  if(m->shortClauses) free(m->shortClauses);


  sat_heap_free(m->variableHeap);
  m->variableHeap = 0;
  
  if(m->activity)       free(m->activity);
  if(m->values)         free(m->values);
  if(m->marks)          free(m->marks);
  if(m->visits)         free(m->visits);
  if(m->dummy)          free(m->dummy);
  if(m->equi)           free(m->equi);
  if(m->maps)           free(m->maps);
  if(m->levels)         free(m->levels);
  if(m->decisionStack)  free(m->decisionStack);
  if(m->seen)           free(m->seen);

  if(m->wls) {
    size = m->nVars+1;
    size = size<<1;
    for(i=0; i<size; i++) {
      arr = m->wls[i];
      if(arr)   free(arr);
    }
    free(m->wls);
  }

  if(m->antes)  free(m->antes);

  if(m->decisionStackSeperator) free(m->decisionStackSeperator);
  if(m->clearned)       free(m->clearned);
  if(m->tlearned)       free(m->tlearned);
  if(m->cclearned)      free(m->cclearned);
  if(m->redundant)      free(m->redundant);
  if(m->dependent)      free(m->dependent);
  if(m->pure)           free(m->pure);
  if(m->temp)           free(m->temp);
  if(m->explanation)    free(m->explanation);
  if(m->previousDecisionHistory) free(m->previousDecisionHistory);

  if(m->clausesHistogram)       free(m->clausesHistogram); 
  vel_heap_free(m);
  if(m->satQueue)       sat_queue_free(m->satQueue);
  if(m->scores)         free(m->scores);
  if(m->candidates)     free(m->candidates);
  if(m->resolvents)     free(m->resolvents);
  if(m->litMarks)       free(m->litMarks);
  if(m->elimtable)      free(m->elimtable);
  if(m->bvars)          free(m->bvars);  
  free(m);
}

void
sat_free_clause_array(satArray_t *arr)
{
long i;
satClause_t *c;

  if(arr) {
    for(i=0; i<arr->size; i++) {
      c = (satClause_t *)arr->space[i];
      if(c->dependent) free(c->dependent);
      free(c);
    }
  }
}

int
sat_read_cnf(satManager_t *m, char *filename)
{
FILE *fin;        
char *gzcmd;

char line[LINEBUFSIZE], word[1024], *lp;
int nArg, begin, flength;
long id, sign, nCl;
long i;
int nPure;
satArray_t *clauseArray;
satClause_t *c;

  flength = strlen(filename);
  if (strcmp(filename+flength-3, ".gz") == 0) {
    fprintf(stdout, "Reading compressed CNF file %s ...\n", filename);

    gzcmd = (char *)malloc(sizeof(char)*(flength + 6));
    strcpy(gzcmd, "zcat ");
    strcat(gzcmd, filename);
    if(!(fin = popen(gzcmd, "r"))) {
      fprintf(stderr, "ERROR : Can't open CNF file %s\n", 
            filename);
      free(gzcmd);
      return(0);
    }
    free(gzcmd);
  }
  else if(!(fin = fopen(filename, "r"))) {
    fprintf(stderr, "ERROR : Can't open CNF file %s\n", 
            filename);
    return(0);
  } 
  
  begin = nCl = 0;
  clauseArray = sat_array_alloc(1024);
  
  while(fgets(line, sizeof line, fin)) {
    lp = sat_remove_space(line);
    if(lp[0] == '\n')   continue;
    if(lp[0] == '#')    continue;
    if(lp[0] == 'c')    continue;
    if(lp[0] == 'p') {
      nArg = sscanf(line, "p cnf %ld %ld", &(m->nVars), &(m->nClauses));
      if(nArg < 2) {
        fprintf(stderr, "ERROR : Unable to read the number of variables and clauses from CNF file %s\n", filename);
        pclose(fin);
        free(clauseArray);
        return(0);
      }
      begin = 1;

      sat_create_database(m);
      continue;
    }
    else if(begin == 0) continue;

    clauseArray->size = 0;
    while(1) {
      lp = sat_remove_space(lp);
      lp = sat_copy_word(lp, word);

      if(strlen(word)) {
        id = atoi(word);
        sign = 1;

        if(id != 0) {
          sign = (id<0) ? 1 : 0;
          id = (id<0) ? -id : id;
          if(id>m->nVars) {
            fprintf(stdout, "ERROR : variable index %d exceed max variable index\n", (int)id);
            pclose(fin);
            free(clauseArray);
            return(0);
          }
          clauseArray = sat_array_insert(clauseArray, ((id<<1) + sign));
        }
        else {
          c = sat_add_clause(m, clauseArray, 0);
          if (m->clauses->size > nCl) {
            sat_init_variable_activity(m, c);
            nCl++;
          }
          clauseArray->size = 0;
        }
      }
      else if(fgets(line, LINEBUFSIZE, fin)){
        lp = &line[0];
        if(lp[0] == '\n')       break;
        if(lp[0] == '#')        break;
        if(lp[0] == 'c')        break;
      }
      else {
        break;
      }
    } 
  }
  
  if(begin == 0) {
    fprintf(stderr, "c ERROR : Can't read CNF file %s\n", filename);
    free(clauseArray);
    return(0);
  }

  if(m->nClauses != nCl) {
    fprintf(stdout, "WARNING : wrong number of clauses %d(%d)\n", (int)m->nClauses, (int)nCl);
  }
  
  nPure = 0;
  if(!m->allSat) {
    for(i=1; i<=m->nVars; i++) {
      if(m->pure[i] == 1) {
        sat_enqueue_check(m, i<<1, 0);
        nPure++;
      }
      else if(m->pure[i] == 2) {
        sat_enqueue_check(m, (i<<1)+1, 0);
        nPure++;
      }
    }
  }


  pclose(fin);
  free(clauseArray);

  return(1);
}

void
sat_init_variable_activity(satManager_t *m, satClause_t *c)
{
long csize, i, lit;

  if(c == 0)    return;
  csize = SATSizeClause(c);
  for(i=0; i<csize; i++) {
    lit = c->lits[i];
    m->activity[lit>>1] += 1.0/(double)csize;
  }
}
satClause_t *
sat_add_learned_clause(satManager_t *m, satArray_t *learned)
{
satClause_t *c;

  if(learned->size == 1) {
/**
    c = sat_new_clause(learned, 1);
    m->learned = sat_array_insert(m->learned, (long)c);
    sat_enqueue_check(m, learned->space[0], c);
    m->nCurLearnedLits ++; m->nCurLearnedClauses++;
    m->nTotalLearnedLits ++; m->nTotalLearnedClauses++;
**/
    c = sat_add_clause(m, learned, 0);
  }
  else {
    c = sat_new_clause(learned, 1);
    m->learned = sat_array_insert(m->learned, (long)c);
    sat_add_watched_literal(m, c);
    sat_update_clause_activity(m, c);
    sat_enqueue_check(m, learned->space[0], c);
  }
  return(c);
}

satClause_t *
sat_add_clause(satManager_t *m, satArray_t *arr, long learned)
{
long lit, v; 
int csize, i;
satClause_t *c;

  if(arr->size == 1) {
    lit = arr->space[0];
    if(learned == 1) {
      m->nCurLearnedLits ++; m->nCurLearnedClauses++;
      m->nTotalLearnedLits ++; m->nTotalLearnedClauses++;
      learned = 0;
    }
    else if(learned == 0) {
      m->nCurClauseLits ++;
      m->nTotalClauseLits ++; 
    }
 
    c = sat_new_clause(arr, learned); /* original clause */
    sat_mark_for_pure_lits(m, c);
    if(learned) 
      m->learned = sat_array_insert(m->learned, (long)c);
    else 
      m->clauses = sat_array_insert(m->clauses, (long)c);
    sat_enqueue_check(m, lit, c);
  }
  else {
    c = sat_new_clause(arr, learned); /* original clause */
    sat_sort_clause_literal(c); 
    if (sat_compress_clause(m, c)) {
      free(c);
      return 0;
    } 
    sat_mark_for_pure_lits(m, c);
    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);
  }

#ifdef SATELITE
  if(m->checkSubsumption && learned == 0) {
    sat_queue_insert(m->subsumptionQueue, (long)c);
    csize = SATSizeClause(c);
    for(i=0; i<csize; i++) {
      lit = c->lits[i];
      v = lit>>1;
      m->occurrence[v] = sat_array_insert(m->occurrence[v], (long)c);
      m->nOccurrence[lit]++;
      m->visits[v] = 1;

      /** What is this for ? HOONSANG **/
      if(m->eliminateHeap->indices[v] > 0)
        sat_heap_up(m, m->eliminateHeap, m->eliminateHeap->indices[v]);
    }
  }
#endif

  if (m->simplify && learned == 0) {
    sat_queue_insert(m->satQueue, (long)c);
    sat_add_all_watched_literal(m, c);
    sat_update_clauses_statistics(m, c);
    csize = SATSizeClause(c);
    m->nLits += SATSizeClause(c);
    for(i=0; i<csize; i++) {
      lit = c->lits[i];
      v = lit >> 1;

      /** restricted to boolean variables 
       ** given by Sateen 
       */
      if (m->allSat == 1 && m->bvars[v] == 0) 
        continue;

      if(m->varElimHeap->indices[v] >= 0)
        vel_heap_down(m, m->varElimHeap->indices[v]);
      else  
        vel_heap_insert(m, v);
    }
  }

  if(arr->size > 1)
    return(c);
  else
    return(0);
}

/**
 *  if value of pure is 0 then no occurence of variable
 *     value of pureis 1 then it is positive pure literal
 *     value of pureis 2 then it is negative pure literal
 *     value of pureis 3 then it is not pure literal
 **/
void
sat_mark_for_pure_lits(satManager_t *m, satClause_t *c)
{
long csize, i;
long lit, sign, v, value;

  csize = SATSizeClause(c);
  for(i=0; i<csize; i++) {
    lit = c->lits[i];
    sign = lit&1;
    v = lit>>1;
    value = (sign == 0) ? 1 : 2;
    m->pure[v] |= value;
  }
}


satClause_t *
sat_add_clause_only(satManager_t *m, satArray_t *arr, long learned)
{
long lit, iLit, pLit;
long i, j;
satClause_t *c;

  sat_literal_array_sort(arr);
  pLit = 0;
  for(i=j=0; i<arr->size; i++) {
    lit = arr->space[i];
    iLit = (pLit ^ 1);
    if(lit == iLit) /* trivially satisfied */
      return(0);
    else if(((m->values[lit>>1]) ^ (SATSign(lit))) != 0 && lit != pLit) {
      pLit = lit;
      arr->space[j++] = pLit;
    }
  }
  arr->size -= (i-j);

  if(arr->size == 1) {
    lit = arr->space[0];
    sat_enqueue(m, lit, 0);
    return(0);
  }
  else {
    c = sat_new_clause(arr, learned); /* original clause */
    sat_add_watched_literal(m, c);
    return(c);
  }
}

void
sat_print_variables(satManager_t *m)
{
long i;

  for(i=0; i<=m->nVars; i++) {
    fprintf(stdout, "%d(%d)(%10g)\n", (int)i, (int)m->values[i], m->activity[i]);
  }
}

void
sat_print_clauses(satManager_t *m, satArray_t *learned)
{
satClause_t *c;
int i;

  for(i=0; i<learned->size; i++) {
    c = (satClause_t *)learned->space[i];
    fprintf(stdout, "%f ", c->info.activity);
    sat_print_clause_simple(m, c);
    fprintf(stdout, "\n");
  }
}

void
sat_delete_clause(satManager_t *m, satClause_t *c)
{
  /**
  fprintf(stdout, "%f ", c->info.activity);
  sat_print_clause_simple(m, c);
  fprintf(stdout, "\n");
  **/

  sat_delete_watched_literal(m, c);
  if(c->dependent)
    free(c->dependent);
  free(c);
}

void
sat_delete_watched_literal(satManager_t *m, satClause_t *c)
{
long index, learned, size;

  index = (c->lits[0])^1;
  if (m->wls[index] && m->wls[index]->size)
    sat_array_delete_elem(m->wls[index], (long)c);

  index = (c->lits[1])^1;
  if (m->wls[index] && m->wls[index]->size)
    sat_array_delete_elem(m->wls[index], (long)c);

  learned = c->size & 1;
  size = SATSizeClause(c);
  if(learned)   {
    m->nCurLearnedLits -= size;
    m->nCurLearnedClauses--;
  }
  else          m->nCurClauseLits -= size;
}

void
sat_add_watched_literal(satManager_t *m, satClause_t *c)
{
long index, learned, size;
satArray_t *arr;

  index = (c->lits[0])^1;
  arr = m->wls[index];
  m->wls[index] = sat_array_alloc_insert(arr, (long)c);

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

  learned = c->size & 1;
  size = SATSizeClause(c);

  if(learned)   {
    m->nCurLearnedLits += size;
    m->nCurLearnedClauses++;
    m->nTotalLearnedLits += size;
    m->nTotalLearnedClauses++;
  }
  else {
    m->nCurClauseLits += size;
    m->nTotalClauseLits += size;
  }
}

satClause_t *
sat_new_clause(satArray_t *arr, long learned)
{
satClause_t *c;
int i;
long abstract;

  c = (satClause_t *)malloc(sizeof(satClause_t) + sizeof(long)*arr->size);
  c->size = (arr->size << SATCsizeShift) | learned;
  for(i=0; i<arr->size; i++)    {
    assert(arr->space[i] != 0);
    c->lits[i] = arr->space[i];
  }
  c->info.activity = 0;
  if(learned == 0) {
    abstract = 0;
    for(i=0; i<arr->size; i++)
      abstract |= 1 << (SATVar(arr->space[i]) & 31);
    c->info.abstract = abstract;
  }
  c->dependent = 0;
  return(c);
}

/** Seperate sat_enqueue and sat_enqueue_check **/
void
sat_enqueue(satManager_t *m, long lit, satClause_t *ante)
{ 
long var;
  
  assert(lit>1);
  var = SATVar(lit);
  m->values[var] = (char)(!SATSign(lit));
  m->levels[var] = SATCurLevel(m);
  m->antes[var] = ante;
  m->decisionStack[m->stackPos++] = lit;
}

void
sat_enqueue_check(satManager_t *m, long lit, satClause_t *ante)
{ 
long var;
  
  assert(lit>1);
  var = SATVar(lit);
  if(m->values[var] == 2)       {
    m->values[var] = (char)(!SATSign(lit));
    m->levels[var] = SATCurLevel(m);
    m->antes[var] = ante;
    m->decisionStack[m->stackPos++] = lit;
  }
  else {
    if(m->values[var] != (char)(!SATSign(lit))) {
      m->status = 0;
    }
  }
}

char *
sat_copy_word(char *lp, char *word)
{
char *wp;

  for(wp = word; ; lp++, wp++) {
    if((*lp == ' ') || (*lp == '\t') || (*lp == '\n'))  break;
    *wp = *lp;
  }
  *wp = '\0';
  return(lp);
}

char *
sat_remove_space(char *line)
{
int i;

  for(i=0; ; i++) {
    if(line[i] == ' ')          continue;
    else if(line[i] == '\t')    continue;
    return(&(line[i]));
  }
}

void
sat_update_variable_activity(satManager_t *m, long v)
{
long  i;

  if((m->activity[v] += m->varInc) > 1e100) {
    for(i=0; i<=m->nVars; i++)
      m->activity[i] *= 1e-100;
    m->varInc *= 1e-100;
  }

  if(m->variableHeap->indices[v] > 0)
    sat_heap_up(m, m->variableHeap, m->variableHeap->indices[v]);
}

void
sat_update_clause_activity(satManager_t *m, satClause_t *c)
{
long  i;
satArray_t *learned;

  learned = 0;
  if((c->info.activity += m->clauseInc) > 1e20) {
    if(c->size&SATCLearned)     learned = m->learned;
    else if(c->size&SATCBlocking)learned = m->blocking;
    else if(c->size&SATCTheory) learned = m->theory;
    for(i=0; i<learned->size; i++) {
      c = (satClause_t *)learned->space[i];
      c->info.activity *= 1e-20;
    }
    m->clauseInc *= 1e-20;
  }
}
void
sat_update_variable_decay(satManager_t *m)
{
  m->varInc *= m->varDecay;
}

void
sat_update_clause_decay(satManager_t *m)
{
  m->clauseInc *= m->clauseDecay;
}

char *
DateReadFromDateString(
  char * datestr)
{
  static char result[25];
  char        day[10];
  char        month[10];
  char        zone[10];
  char       *at;
  int         date;
  int         hour;
  int         minute;
  int         second;
  int         year;

  if (sscanf(datestr, "%s %s %2d %2d:%2d:%2d %s %4d",
             day, month, &date, &hour, &minute, &second, zone, &year) == 8) {
    if (hour >= 12) {
      if (hour >= 13) hour -= 12;
      at = "PM";
    }
    else {
      if (hour == 0) hour = 12;
      at = "AM";
    }
    (void) sprintf(result, "%d-%3s-%02d at %d:%02d %s", 
                   date, month, year % 100, hour, minute, at);
    return result;
  }
  else {
    return datestr;
  }
}

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

  Synopsis    [ Reports memory usage ] 

  Description [ Reports memory usage ]

  SideEffects [ ]

  SeeAlso     [ ]

******************************************************************************/
long
sat_mem_used(int field)
{
char name[256];
FILE *in;
pid_t pid;
long value;

  pid = getpid();
  sprintf(name, "/proc/%d/statm", pid);
  in = fopen(name, "rb");
  if (in == 0)  return 0;

  for ( ; field >= 0; field--)
    if (fscanf(in, "%ld", &value) != 1) {
      fprintf(stderr, "Can't get MEM usage!\n");
      return 0;
    }  
  fclose(in);

  value *= getpagesize();
  return value;
}


void
sat_verify(satManager_t *m)
{
long i, j, csize, lit;
satArray_t *clauses;
satClause_t *c;
int satisfied;

  clauses = m->clauses;
  for(i=0; i<clauses->size; i++) {
    c = (satClause_t *)clauses->space[i];
    csize = SATSizeClause(c);
    satisfied = 0;
    for(j=0; j<csize; j++) {
      lit = c->lits[j];
      if((m->values[lit>>1] ^ (lit&1)) == 1) {
        satisfied = 1;
        break;
      }
    }
    if(satisfied == 0) {
      fprintf(stdout, "ERROR : unsatisfied claues\n");
      sat_print_clause(m, c);
      fprintf(stdout, "\n");
    }
  }

  clauses = m->deleted;
  for(i=0; i<clauses->size; i++) {
    c = (satClause_t *)clauses->space[i];
    csize = SATSizeClause(c);
    satisfied = 0;
    for(j=0; j<csize; j++) {
      lit = c->lits[j];
      if((m->values[lit>>1] ^ (lit&1)) == 1) {
        satisfied = 1;
        break;
      }
    }
    if(satisfied == 0) {
      fprintf(stdout, "ERROR : unsatisfied claues\n");
      sat_print_clause(m, c);
      fprintf(stdout, "\n");
    }
  } 
}

void
sat_print_database(satManager_t *m)
{
long i;
satClause_t *c;
satArray_t *arr;

  fprintf(stdout, "==========================\n");
  fprintf(stdout, " Current CNF Clauses\n");
  fprintf(stdout, "==========================\n");

  arr = m->clauses;
  for(i=0; i<arr->size; i++) {
    c = (satClause_t *)arr->space[i];
    sat_print_clause(m, c);
    fprintf(stdout, "\n");
  }

  arr = m->learned;
  for(i=0; i<arr->size; i++) {
    c = (satClause_t *)arr->space[i];
    sat_print_clause(m, c);
    fprintf(stdout, "\n");
  }

  fprintf(stdout, "\n");
}

void
sat_print_clause(satManager_t *m, satClause_t *c)
{
long i, csize, lit;
  
  csize = SATSizeClause(c);
  fprintf(stdout, "%d %f (", (int) c->size&SATCTypeMask, c->info.activity);
  for(i=0; i<csize; i++) {
    lit = c->lits[i];
    sat_print_literal(m, lit, 0);
    fprintf(stdout, " ");
    if(i!=0 && (i%10)==0)
      fprintf(stdout, "\n");
  }
  fprintf(stdout, ")");
  fflush(stdout);
}

void
sat_print_clause_array(satManager_t *m, satArray_t *learned)
{
long i, lit;
  
  for(i=0; i<learned->size; i++) {
    lit = learned->space[i];
    sat_print_literal(m, lit, 0);
    fprintf(stdout, " ");
    if(i!=0 && (i%10)==0)
      fprintf(stdout, "\n");
  }
  fprintf(stdout, ")");
  fflush(stdout);
}

void
sat_print_short_clause(satManager_t *m, satClause_t *c, FILE *fp)
{
long i, csize, lit;

  if(fp == 0)   fp = stdout;
  csize = SATSizeClause(c);
  fprintf(fp, "%d %f (", (int) c->size&SATCTypeMask, c->info.activity);
  for(i=0; i<csize; i++) {
    lit = c->lits[i];
    sat_print_literal(m, lit, fp);
    fprintf(fp, " ");
    if(i!=0 && (i%10)==0)
      fprintf(fp, "\n");
  }
  fprintf(fp, ")");
  fflush(fp);
}

void
sat_print_clause_simple(satManager_t *m, satClause_t *c)
{
long i, csize, lit;
long v;
  
  csize = SATSizeClause(c);
  for(i=0; i<csize; i++) {
    lit = c->lits[i];
    v = lit>>1;
    fprintf(stdout, "%c%d:%c", 
                   lit&1 ? '-' : ' ',
                   (int)v,
                   m->values[v]==1 ? '1' : (m->values[v]==0 ? '0' : 'x'));
    fprintf(stdout, " ");
  }
  fflush(stdout);
}

void
sat_print_literal(satManager_t *m, long lit, FILE *fp)
{
long v;
  
  if(fp == 0)   fp = stdout;
  v = lit>>1;
  fprintf(fp, "%c%d:%c@%d", 
                   lit&1 ? '-' : ' ',
                   (int)v,
                   m->values[v]==1 ? '1' : (m->values[v]==0 ? '0' : 'x'),
                   (int)m->levels[v]);
  fflush(fp);
}

void
sat_report_result(satManager_t *m)
{
double nConflicts;

  if(m == 0)    return;

  fprintf(stdout, "CNF read time  : %10g \n", m->readTime);
  fprintf(stdout, "CNF solve time : %10g \n", m->solveTime);
  fprintf(stdout, "Memory usage : %10g MB\n", sat_mem_used(0)/1048576.0);
  fprintf(stdout, "Restart : %ld\n", m->nRestarts);
  fprintf(stdout, "Decisions : random(%0.f), heuristic(%0.f), history(%0.f/%0.f)\n", 
          m->nRandomDecisions, m->nDecisions,
          m->nHistoryDecisions, m->nTHistoryDecisions
          );
  fprintf(stdout, "Implications : %0.f\n", m->nImplications); 
  fprintf(stdout, "Forced Restart : %0.f\n", m->nForceRestart); 
  fprintf(stdout, "Polarity Change : %0.f\n", m->nPolarityChange); 
  fprintf(stdout, "Learned clasues  : %0.f out of %0.f\n", 
          m->nCurLearnedClauses, m->nTotalLearnedClauses);
  fprintf(stdout, "Learned literals : %0.f out of %0.f\n", 
          m->nCurLearnedLits, m->nTotalLearnedLits);
  if(m->allSat) {
    fprintf(stdout, "Blocking clasues  : %0.f out of %0.f\n", 
          m->nCurBlockingClauses, m->nTotalBlockingClauses);
    fprintf(stdout, "Blocking literals : %0.f out of %0.f\n", 
          m->nCurBlockingLits, m->nTotalBlockingLits);
  }
  fprintf(stdout, "Number of first UIP : %ld out of %0.f\n", 
          m->nFirstUip, m->nTotalLearnedClauses);
  fprintf(stdout, "Number of simplify : %d\n", m->nSimplify); 
  nConflicts = m->nTotalLearnedClauses + m->nOmittedConflictClauses;
  
  fprintf(stdout, "Number of conflicts : %ld\n", (long)nConflicts); 
  if (m->nTotalLearnedClauses > 0) {
    fprintf(stdout, "Resolution steps per conflict : %ld\n", (long)(m->depthOfConflict /m->nConflicts)); 
    if (m->nDistillInConflict)
      fprintf(stdout, "Resolution steps per OCI: %ld\n", (long)m->depthOfOTS/m->nDistillInConflict); 
    if (m->nAuxConflictAnalysis)
      fprintf(stdout, "Resolution steps per additional conflict: %ld\n", (long)m->depthOfStrong/m->nAuxConflictAnalysis); 
   }
    fprintf(stdout, "Strengthened clauses due to OCI: %ld\n", m->nDistillInConflict);
    fprintf(stdout, "Eliminated clasues due to OCI: %ld\n", m->nEliminatedClsInConflict);
    fprintf(stdout, "Eliminated literals due to OCI: %ld\n", m->nEliminatedLitsInConflict);
    fprintf(stdout, "Saved conflict clasues: %ld\n", m->nOmittedConflictClauses);
    fprintf(stdout, "Saved conflict literals: %ld\n", m->nOmittedConflictLits);
    fprintf(stdout, "Additional conflict clauses: %ld\n", m->nAuxLearnedClauses);
    fprintf(stdout, "Additional conflict literals: %ld\n", m->nAuxLearnedLits);
    fprintf(stdout, "Additional conflict analysis: %ld\n", m->nAuxConflictAnalysis);

  if (m->allSat == 0) {
    if(m->status == 0) fprintf(stdout, "UNSATISFIABLE\n");
    else if(m->status == 1) {
      fprintf(stdout, "SATISFIABLE\n");
      if (m->printModel)
        sat_print_assignment(m);
    }
  }
}

void 
sat_print_assignment(satManager_t *m)
{
int value;
long i;

  fprintf(stdout, "v ");        
  for(i=1; i<=m->nVars; i++) {
    value = m->values[i];
    if (value >= 2)
      fprintf(stdout, "c WARNING : No assignment on %d!\n", (int)i);
    else
      fprintf(stdout, "%c%ld ", value ? ' ':'-', i);

    if (i % 10 == 0) {
      fprintf(stdout, "\nv ");  
    }       
  }
  fprintf(stdout, "0 \n");      
}

void
sat_print_implication_graph(satManager_t *m, long level)
{
satArray_t *seperator;
satClause_t *ante;
long *stack;
long bi, ei, lit, v, i;

  seperator = m->decisionStackSeperator;
  stack = m->decisionStack;
  if(seperator->size < level) {
    fprintf(stdout, "ERROR : level %d has been assigned\n", (int)level);
    return;
  }

  if(level == 0)bi = 0;
  else          bi = seperator->space[level-1];
  ei = (seperator->size==level) ? m->stackPos : seperator->space[level];
  
  lit = stack[bi];
  v = lit>>1;
  fprintf(stdout, "++++++++++++++++++++++++++++++++\n");
  fprintf(stdout, "* Level %d ", (int)level); 
  sat_print_literal(m, v<<1, 0);
  fprintf(stdout, "\n");
  fprintf(stdout, "++++++++++++++++++++++++++++++++\n");

  for(i=bi+1; i<ei; i++) {
    lit = stack[i];
    v = lit>>1;
    ante = m->antes[v];
    sat_print_literal(m, v<<1, 0);
    fprintf(stdout, "<= ");
    if(ante->size & SATCTheory) 
      fprintf(stdout, "THEORY ");
    if(ante)
      sat_print_clause(m, ante);
    else
      fprintf(stdout, "NO ANTECEDENT\n");

    fprintf(stdout, "\n");
  }
  fflush(stdout);
}

void
sat_print_short_implication_graph(satManager_t *m, long level)
{
satArray_t *seperator;
satClause_t *ante;
long *stack;
long bi, ei, lit, v, i;
char name[1024];
FILE *fp;

  seperator = m->decisionStackSeperator;
  stack = m->decisionStack;
  if(seperator->size < level) {
    fprintf(stdout, "ERROR : level %d has been assigned\n", (int)level);
    return;
  }

  bi = seperator->space[level-1];
  ei = (seperator->size==level) ? m->stackPos : seperator->space[level];

  
  lit = stack[bi];
  v = lit>>1;

  sprintf(name, "%d_%d_%d.txt", (int)level, (int)v, (int)m->nDecisions);
  fp = fopen(name, "w");
  

  fprintf(fp, "++++++++++++++++++++++++++++++++\n");
  fprintf(fp, "* Level %d ", (int)level); 
  sat_print_literal(m, v<<1, fp);
  fprintf(fp, "\n");
  fprintf(fp, "++++++++++++++++++++++++++++++++\n");

  for(i=bi+1; i<ei; i++) {
    lit = stack[i];
    v = lit>>1;
    ante = m->antes[v];
    sat_print_literal(m, v<<1, fp);
    fprintf(fp, "<= ");
    if(ante) {
      if(ante->size & SATCTheory) 
        fprintf(fp, "THEORY ");
      sat_print_short_clause(m, ante, fp);
    }
    else {
      fprintf(fp, "ERROR: no antecedent ");
    }

    fprintf(fp, "\n");
  }
  fflush(fp);
  fclose(fp);
}

void
sat_print_dot_for_implication_graph(
        satManager_t *m,
        satClause_t *c,
        long level,
        int iAllLevel)
{
char name[1024];
FILE *fp;
satArray_t *seperator;
satClause_t *ante;
long *stack;
long bi, ei, lit, v, i, j;
long nlit, nv;
long visit, csize;
int blueColor;

  blueColor = 0;
  visit = 0;
  if(c) {
    visit = 1;
    csize = SATSizeClause(c);
    for(i=0; i<csize; i++) {
      lit = c->lits[i];
      v = lit>>1;
      if(m->levels[v] == level) {
        m->visits[v] = visit;
      }
    }
  }

  seperator = m->decisionStackSeperator;
  stack = m->decisionStack;
  if(seperator->size < level) {
    fprintf(stdout, "ERROR : level %d has been assigned\n", (int)level);
    return;
  }

  bi = seperator->space[level-1];
  ei = (seperator->size==level) ? m->stackPos : seperator->space[level];
  lit = stack[bi];
  v = lit>>1;
  sprintf(name, "%d_%d_%d_%d.dot", (int)level, (int)v, (int)m->nDecisions, iAllLevel);
  fp = fopen(name, "w");
  fprintf(fp, "digraph \"AndInv\" {\n  rotate=90;\n");
  fprintf(fp, "  margin=0.5;\n  label=\"AndInv\";\n");
  fprintf(fp, "  size=\"10,7.5\";\n  ratio=\"fill\";\n");

  bi++;
  for(i=ei-1; i>=bi; i--) {
    lit = stack[i];
    v = lit>>1;
    if(m->visits[v] != visit)   continue;

    ante = m->antes[v];

    if(ante->size & SATCTheory) {
      blueColor = 1;
    }

    csize = SATSizeClause(ante);
    for(j=0; j<csize; j++) {
      nlit = ante->lits[j];
      nv = nlit>>1;

      if(nv == v) continue;
        
      if(m->levels[nv] == level) {
        m->visits[nv] = visit;
        if(blueColor) {
          fprintf(fp,"%d -> %d [color = blue];\n", (int)nv, (int)v);
          blueColor = 0;
        }
        else
          fprintf(fp,"%d -> %d [color = red];\n", (int)nv, (int)v);
      }
      else if(iAllLevel)
        fprintf(fp,"%d.%d -> %d [color = black];\n", (int)nv, (int)m->levels[nv], (int)v);

    }
  }
  fprintf(fp, "}\n");
  fclose(fp);

  if(visit) {
    for(i=ei-1; i>=bi; i--) {
      v = (stack[i]>>1);
      m->visits[v] = 0;
    }
  }

}

void
sat_print_cnf(satManager_t *m, long iter)
{
long nCl, i;
char filename[1024];
FILE *fp;
satArray_t *arr;
/*satClause_t *c; HK */

  arr = m->clauses;
  nCl = 0;
  for(i=0; i<arr->size; i++) {
    /*c = (satClause_t *)arr->space[i]; HK */
    nCl++;
  }
  arr = m->learned;
  for(i=0; i<arr->size; i++) {
    /* c = (satClause_t *)arr->space[i]; HK */
    nCl++;
  }

  sprintf(filename, "tmp%d.cnf", (int)iter);
  fp = fopen(filename, "w");
  fprintf(fp, "p cnf %d %d\n", (int)m->nVars, (int)nCl);
  sat_print_clause_in_dimacs(fp, m->clauses);
  sat_print_clause_in_dimacs(fp, m->learned);

  fclose(fp);
}

void
sat_print_clause_in_dimacs(FILE *fp, satArray_t *arr)
{
long i, j, v, lit, csize;
satClause_t *c;

  for(i=0; i<arr->size; i++) {
    c = (satClause_t *)arr->space[i];
    csize = SATSizeClause(c);
    for(j=0; j<csize; j++) {
      lit = c->lits[j];
      v = lit>>1;
      v = lit&1 ? -v : v;
      fprintf(fp, "%d ", (int)v);
    }
    fprintf(fp, "0\n");
  }
}

void
sat_print_cnf_less_than(FILE *fp, satArray_t *arr, long limit)
{
long i, j, v, lit, csize;
satClause_t *c;

  for(i=0; i<arr->size; i++) {
    c = (satClause_t *)arr->space[i];
    csize = SATSizeClause(c);
    if(csize < limit)   {
      for(j=0; j<csize; j++) {
        lit = c->lits[j];
        v = lit>>1;
        v = lit&1 ? -v : v;
        fprintf(fp, "%d ", (int)v);
      }
      fprintf(fp, "0\n");
    }
  }
}

void
sat_make_dependent_graph(satManager_t *m, satClause_t *c)
{
#if 0 
  if(c->dependent && c->dependent->size > 0) {
    fprintf(stdout, "ERROR\n");
  }
#endif
  c->dependent = sat_array_copy(m->dependent, 0);
}

void
sat_get_dependent_clauses(satManager_t *m, satClause_t *c)
{
long csize, i;
long *pLit, cLit, v;
satClause_t *ante;

  csize = SATSizeClause(c);
  pLit = &(c->lits[0]);
  for(i=0; i<csize; i++) {
    cLit = *pLit++;
    v = cLit >> 1;
    ante = m->antes[v];

    if(ante->size & SATCVisited)        continue;
    ante->size = ante->size | SATCVisited;
    m->dependent = sat_array_insert(m->dependent, (long)ante);
    sat_get_dependent_clauses(m, ante);
  }
  
}

void
sat_generate_unsat_core_main(satManager_t *m)
{
satArray_t *dependent; /*, *arr; */
satClause_t *c, *conflicting;
long i; /*, j, lit, tv, nMarks */
/* long pSize, cLit, *pLit, v, csize; */

  
/**
  conflicting = m->nullClause;
  m->dependent->size = 0;
  conflicting->size = conflicting->size | SATCVisited;
  m->dependent = sat_array_insert(m->dependent, (long)conflicting);
  sat_get_dependent_clauses(m, conflicting);
  dependent = m->dependent;
  for(i=0; i<dependent->size; i++) {
    c = (satClause_t *)dependent->space[i];
    c->size = c->size - SATCVisited;
  }
  sat_undo(m, -1);
  arr = m->clauses;
  for(i=0; i<arr->size; i++) {
    c = (satClause_t *)arr->space[i];
    csize = SATSizeClause(c);
    if(csize == 1) {
      sat_enqueue(m, c->lits[0], c);
    }
  }
  arr = m->learned;
  for(i=0; i<arr->size; i++) {
    c = (satClause_t *)arr->space[i];
    csize = SATSizeClause(c);
    if(csize == 1) {
      sat_enqueue(m, c->lits[0], c);
    }
  }
  m->nullClause = sat_implication(m);
  m->decisionStackSeperator = 
          sat_array_insert(m->decisionStackSeperator, m->stackPos);
          **/


  conflicting = m->nullClause;
  m->dependent->size = 0;
  conflicting->size = conflicting->size | SATCVisited;
  m->dependent = sat_array_insert(m->dependent, (long)conflicting);
  sat_get_dependent_clauses(m, conflicting);
  dependent = m->dependent;
  for(i=0; i<dependent->size; i++) {
    c = (satClause_t *)dependent->space[i];
    c->size = c->size - SATCVisited;
  }

#if 0
  i = m->stackPos - 1;
  tv = 0;
  nMarks = 0;
  lit = 0;
  if(m->coreGeneration)
    m->dependent = sat_array_insert(m->dependent, (long)conflicting);
  do {
    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->marks[v]) {
        m->marks[v] = 1;
        if(m->levels[v] >= SATCurLevel(m))
          nMarks++;
      }
    }
    while(i>=0 && !(m->marks[(m->decisionStack[i--])>>1]));
    if(i < -1) break;
    lit = m->decisionStack[i+1];
    tv = lit>>1; 
    conflicting = m->antes[tv];

    if(m->coreGeneration)
      m->dependent = sat_array_insert(m->dependent, (long)conflicting);
    m->marks[tv] = 0;
    nMarks--;
  } while(nMarks > 0 && i>=0);
#endif

  dependent = m->dependent;
  for(i=0; i<dependent->size; i++) {
    c = (satClause_t *)dependent->space[i];
    if(c->size & SATCVisited)   continue;

    c->size = c->size | SATCVisited;
    sat_generate_unsat_core(m, c);
  }
}


void
sat_check_clause_flag(satManager_t *m)
{
satArray_t *arr;
satClause_t *c;
long i;

  arr = m->clauses;
  for(i=0; i<arr->size; i++) {
    c = (satClause_t *)arr->space[i];
    if(!(c->size & SATCVisited))        continue;
    fprintf(stdout, "%d ", (int) c->size & SATCVisited);
    sat_print_clause(m, c);
    fprintf(stdout, "\n");
  }

  arr = m->learned;
  for(i=0; i<arr->size; i++) {
    c = (satClause_t *)arr->space[i];
    if(!(c->size & SATCVisited))        continue;
    fprintf(stdout, "%d ", (int) c->size & SATCVisited);
    sat_print_clause(m, c);
    fprintf(stdout, "\n");
  }
}

void
sat_generate_unsat_core(satManager_t *m, satClause_t *cl)
{
satArray_t *dependent;
satClause_t *c;
long i;

  dependent = cl->dependent;
  if(dependent == 0)    return;

  for(i=0; i<dependent->size; i++) {
    c = (satClause_t *)dependent->space[i];
    if(c->size & SATCVisited)   continue;

    c->size = c->size | SATCVisited;
    sat_generate_unsat_core(m, c);
  }
}

satArray_t *
sat_generate_unsat_core_clauses_index_array(satManager_t *m)
{
satArray_t *clauses, *coreArray;
long i;
satClause_t *c;

  coreArray = sat_array_alloc(1024);
  
  clauses = m->clauses;
  for(i=0; i<clauses->size; i++) {
    c = (satClause_t *)clauses->space[i];
    if(c->size & SATCVisited) 
      coreArray = sat_array_insert(coreArray, i);
  }

  return(coreArray);
}

int
sat_print_unsat_core(satManager_t *m, char *cnfFilename)
{
FILE *fp;
long i, j, nClauses, lit;
long csize;
char *filename;
satClause_t *c;
satArray_t *clauses;

  filename = malloc(sizeof(char)*(strlen(cnfFilename)+6));
  sprintf(filename, "%s.core", cnfFilename);
  if(!(fp = fopen(filename, "w"))) {
    fprintf(stderr, "ERROR : Can't open CNF file %s\n", 
            filename);
    return(0);
  }

  nClauses = 0;
  clauses = m->clauses;
  for(i=0; i<clauses->size; i++) {
    c = (satClause_t *)clauses->space[i];
    if(c->size & SATCVisited) nClauses++;
  }

  fprintf(fp, "p cnf %d %d\n", (int) m->nVars, (int) nClauses);
  for(i=0; i<clauses->size; i++) {
    c = (satClause_t *)clauses->space[i];
    if(!(c->size & SATCVisited)) continue;
    csize = SATSizeClause(c);
    for(j=0; j<csize; j++) {
      lit = c->lits[j];
      fprintf(fp, "%d ", lit&1 ? (int) -(lit>>1) : (int) (lit>>1));
    }
    fprintf(fp, "0\n");
  }
  fclose(fp);
  free(filename);
  return(1);
}

void
sat_print_dependent_clauses(satManager_t *m, satClause_t *c)
{
long i;
satArray_t *dep;
satClause_t *d;

  fprintf(stdout, "++++++++++++++++++++++++++++++++++++\n");
  sat_print_clause(m, c);
  fprintf(stdout, "\n");
  fprintf(stdout, "++++++++++++++++++++++++++++++++++++\n");
  dep = c->dependent;
  if(dep == 0)  return;

  for(i=0; i<dep->size; i++) {
    d = (satClause_t *)dep->space[i];
    sat_print_clause(m, d);
    fprintf(stdout, "\n");
  }
}

void
sat_print_dependent_graph(satManager_t *m)
{
satArray_t *arr;
satClause_t *c;
long i;

  arr = m->learned;
  for(i=0; i<arr->size; i++) {
    c = (satClause_t *)arr->space[i];
    sat_print_dependent_clauses(m, c);
  }
}

void
sat_check_dependent_clauses(satClause_t *c)
{
long i;
satArray_t *dep;
satClause_t *d;

  dep = c->dependent;
  if(dep == 0)  return;

  for(i=0; i<dep->size; i++) {
    d = (satClause_t *)dep->space[i];
    if(d->size>1000){
      fprintf(stdout, "ERROR\n");
    } 
  }
}

void
sat_check_dependent_graph(satManager_t *m)
{
satArray_t *arr;
satClause_t *c;
long i;

  arr = m->learned;
  for(i=0; i<arr->size; i++) {
    c = (satClause_t *)arr->space[i];
    sat_check_dependent_clauses(c);
  }
}

int
sat_compare_activity(void *activity, const void *xx, const void * yy)
{
double *a;
long x, y;

  x = (long) xx;
  y = (long) yy;
   
  a = (double *)activity;
  return(a[x] > a[y]);
}



#ifdef SatELite

int
sat_eliminate_clauses(satManager_t *m)
{
int cnt;
long next;

  if(m->checkSubsumption == 0)
    return(0);

  while(sat_queue_size(m->subsumptionQueue) > 0 || m->eliminateHeap->size > 0) {
    if(!sat_backward_subsumption_check(m))
      return(0);
    for(cnt = 0; m->eliminateHeap->size > 0; cnt++) {
      next = sat_heap_remove_min(m, m->eliminateHeap);

      if(!sat_eliminate_variable(m, next))
        return(0);
    }
    /** add touched clauses into subsumption queue **/
    sat_collect_subsumption_candidiates(m);
  }

  /** free data structure for eliminating clauses **/
  sat_free_data_for_eliminating_clause(m);

  return(1);
  /** need add function for variable ordering **/
}

void
sat_free_data_for_eliminating_clause(satManager_t *m)
{
int i;
satArray_t *cArr;

  sat_queue_free(m->subsumptionQueue);
  m->subsumptionQueue = 0;
  sat_heap_free(m->eliminateHeap);

  free(m->visits);
  m->visits = 0;

  free(m->nOccurrence);
  m->nOccurrence = 0;

  for(i=0; i<m->nVars; i++) {
    cArr = m->occurrence[i];
    free(cArr);
  }
  free(m->occurrence);
  m->occurrence = 0;
}

void
sat_collect_subsumption_candidiates(satManager_t *m)
{
int i, j, mask;
satArray_t *cArr;
satClause_t *c;

  for(i=0; i<m->nVars; i++) {
    if(m->visits[i]) {
      m->visits[i] = 0;
      sat_cleanup_occurrence_array(m, i);
      cArr = m->occurrence[i];
      for(j=0; j<cArr->size; j++) {
        c = (satClause_t *)cArr->space[j];
        /** To avoid putting same clauses into subsumption queue */
        if((c->size & SATCVisited2) == 0) {
          sat_queue_insert(m->subsumptionQueue, (long)c); 
          c->size = c->size | SATCVisited2;
        }
      }
    }
  }

  mask = ~SATCVisited2 & ~SATCVisited;
  for(i=m->subsumptionQueue->first; i<m->subsumptionQueue->arr->size; i++) {
    c = (satClause_t *)m->subsumptionQueue->arr->space[i];
    c->size = c->size & mask;
  }

}

int
sat_eliminate_variable(satManager_t *m, long v)
{
int csize, i, j;
int count;
long lit;
satArray_t *cArr;
satClause_t *c;
satArray_t *lphase[2];
/** need to figure out what is asymmVar check **/

  if(m->values[v] != 2) return(1);
  sat_cleanup_occurrence_array(m, v);
  cArr = m->occurrence[v];

  /** need to skip when there are too many clauses **/
  
  /** split the occurrence into positive and negative **/
  /** 0 : pos, 1: neg **/
  lphase[0] = sat_array_alloc(1024);
  lphase[1] = sat_array_alloc(1024);
  for(i=0; i<cArr->size; i++) {
    c = (satClause_t *)cArr->space[i];
    csize = SATSizeClause(c);
    for(j=0; j<csize; j++) {
      lit = c->lits[j];
      if(lit>>1 == v) { 
        lphase[lit&1] = sat_array_insert(lphase[lit&1], (long)c);
        break;
      }
    }
  }
  /** Count the number of clauses increased after variable elimination **/
  count = 0;
  for(i=0; i<lphase[0]->size; i++) {
    for(j=0; j<lphase[1]->size; j++) {
      if(!sat_resolvent_is_tautology((satClause_t *)lphase[0]->space[i], (satClause_t *)lphase[1]->space[j], v)) {
        count++;
        if(count >cArr->size) {
          free(lphase[0]);
          free(lphase[1]);
          return(1);
        }
      }
    }
  }
  /** Remove and store original clause **/
  m->elimOrderArray[v] = m->elimOrder++;
  for(i=0; i<cArr->size; i++) {
    if(m->elimClauses[v] == 0)
      m->elimClauses[v] = sat_array_alloc(cArr->size);
    c = (satClause_t *)cArr->space[i];
    m->elimClauses[v] = sat_array_insert(m->elimClauses[v], (long)c);
    sat_delete_clause_for_cs(m, c);
  }
  /** free cArr */
  free(cArr);
  m->occurrence[v] = 0;

  /** Generate resolvent **/
  for(i=0; i<lphase[0]->size; i++) {
    for(j=0; j<lphase[1]->size; j++) {
      m->clearned->size = 0;
      m->clearned = sat_generate_resolvent((satClause_t *)lphase[0]->space[i], (satClause_t *)lphase[1]->space[j], v, m->clearned);
      if(m->clearned->size)
        c = sat_add_clause(m, m->clearned, 0);
    }
  }
  
  free(lphase[0]);
  free(lphase[1]);
  return(sat_backward_subsumption_check(m));
}

int
sat_resolvent_is_tautology(satClause_t *_c1, satClause_t *_c2, long v) 
{
int c1_small;
satClause_t *c1, *c2;
int i, j, c1size, c2size;
long lit1, lit2;

  c1_small = SATSizeClause(_c1) < SATSizeClause(_c2);
  c1 = c1_small ? _c2 : _c1;
  c2 = c1_small ? _c1 : _c2;

  c1size = SATSizeClause(c1);
  c2size = SATSizeClause(c2);
  for(i=0; i<c2size; i++) {
    lit2 = c2->lits[i];
    if(lit2>>1 == v)    continue;
    for(j=0; j<c2size; j++) {
      lit1 = c1->lits[j];
      if((lit1>>1) == (lit2>>1)) {
        if(lit1 == (lit2^1)) 
          return(0);
        else 
          goto next;
      }
    }
    next:;
  }
  return 1;
}

satArray_t *
sat_generate_resolvent(satClause_t *_c1, satClause_t *_c2, long v, satArray_t *resolvent)
{
int c1_small;
satClause_t *c1, *c2;
int i, j, c1size, c2size;
long lit1, lit2;

  c1_small = SATSizeClause(_c1) < SATSizeClause(_c2);
  c1 = c1_small ? _c2 : _c1;
  c2 = c1_small ? _c1 : _c2;

  c1size = SATSizeClause(c1);
  c2size = SATSizeClause(c2);
  for(i=0; i<c2size; i++) {
    lit2 = c2->lits[i];
    if(lit2>>1 == v)    continue;
    for(j=0; j<c2size; j++) {
      lit1 = c1->lits[j];
      if((lit2>>1) == (lit1>>1)) {
        if(lit2 == (lit1^1)) {
          resolvent->size = 0;
          return(resolvent);
        }
        else {
          goto next;
        }
      }
    }
    resolvent = sat_array_insert(resolvent, lit1);
    next:;
  }

  for(i=0; i<c2size; i++) {
    lit2 = c2->lits[j];
    if(lit2>>1 != v)
      resolvent = sat_array_insert(resolvent, lit1);
  }
  
  return(resolvent);

}

void
sat_cleanup_occurrence_array(satManager_t *m, long v)
{
int i, j;
satArray_t *arr;
satClause_t *c;

  arr = m->occurrence[v];
  for(i=j=0; i<arr->size; i++) {
    c = (satClause_t *)arr->space[i];
    /** 
    tmp = ((c->size & SATCVisited) == 0) ? (arr->space[j++] = arr->space[i], 1) : 1;
    **/
    if((c->size & SATCVisited) == 0)
      arr->space[j++] = arr->space[i];
  }

  arr->size -= (i-j);
  m->occurrence[v] = arr;
}

int
sat_backward_subsumption_check(satManager_t *m)
{
int i, j;
long lit, best, v, csize;
satClause_t *c, *ct;
satArray_t *cArr;

  while(sat_queue_size(m->subsumptionQueue)> 0 || m->bsAssigns < m->stackPos) {
    if(sat_queue_size(m->subsumptionQueue) == 0 && m->bsAssigns < m->stackPos) {
      lit = m->decisionStack[m->bsAssigns++];
      m->clearned->size = 1;
      m->clearned->space[0] = lit;
      c = sat_new_clause(m->clearned, 0);
      sat_queue_insert(m->subsumptionQueue, (long)c);
    }
    c = (satClause_t *)sat_queue_pop(m->subsumptionQueue);
    if(c->size & SATCVisited)   continue;

    best = (c->lits[0])>>1;
    csize = SATSizeClause(c);
    for(i=1; i<csize; i++) {
      lit = c->lits[i];
      v = lit>>1;
      if(m->occurrence[v]->size < m->occurrence[best]->size)
        best = v;
    }
    
    sat_cleanup_occurrence_array(m, best);
    cArr = m->occurrence[best];
    for(i=0; i<cArr->size; i++) {
      if(c->size & SATCVisited) break;
      ct = (satClause_t *)cArr->space[i];
      if(!(ct->size & SATCVisited) && ct != c) {
        lit = sat_subsumption_check(m, c, ct);
        if(lit == 0) {
          m->nSubsumedClauses++;
          sat_delete_clause_for_cs(m, ct);
        }
        else if(lit>0) {
          m->nSubsumedDeletedLiterals++;
          if(!sat_strengthen_clause(m, ct, lit^1))
            return(0);
          if((lit>>1) == best)
            j--;
        }

      }
    }
  }
  return(1);
}

void
sat_delete_literal_from_clause(satClause_t *c, long lit)
{
int i, csize;
long abstract;
long tlit;
  
  csize = SATSizeClause(c);
  abstract = 0;
  for(i=0; i<csize && c->lits[i] != lit; i++) {
    tlit = c->lits[i];
    if(tlit == lit)     break;
    abstract |= 1 << (SATVar(tlit) & 31);
  }
  csize--;
  for(; i<csize; i++)  {
    tlit = c->lits[i+1];
    abstract |= 1 << (SATVar(tlit) & 31);
    c->lits[i] = tlit;
  }
  c->info.abstract = abstract;
  c->size = (csize << SATCsizeShift) | (c->size & SATCMask);
}

int
sat_strengthen_clause(satManager_t *m, satClause_t *c, long lit)
{
long tlit;
int csize;
int index;
satArray_t *arr;
satClause_t *conflicting;

  sat_queue_insert(m->subsumptionQueue, (long)c);
  if(c->lits[0] == lit || c->lits[1] == lit) {
    csize = SATSizeClause(c);
    if(csize == 2) {
      sat_delete_clause_for_cs(m, c);
      sat_delete_literal_from_clause(c, lit);      
    }
    else {
      sat_delete_literal_from_clause(c, lit);      
      /** delete clasue c from watched literal of lit **/
      sat_array_delete_elem(m->wls[lit^1], (long)c);

      /** add clause c to watched literal of tlit **/
      tlit = c->lits[1];
      index = (tlit)^1;
      arr = m->wls[index];
      m->wls[index] = sat_array_alloc_insert(arr, (long)c);
    }
  }
  else {
    sat_delete_literal_from_clause(c, lit);      
  }

  sat_array_delete_elem(m->occurrence[lit>>1], (long)c);
  m->nOccurrence[lit]--; 
  if(m->elimOrderArray[lit>>1] == 0) /** if variable is not eliminated **/
    sat_heap_update(m, m->eliminateHeap, lit>>1);
  
  csize = SATSizeClause(c);
  if(csize != 1) return(1);

  sat_enqueue_check(m, c->lits[0], 0);
  conflicting = sat_implication(m);
  if(conflicting)       {
    m->status = 0;
    return(0);
  }
  
  return(1);
}

void
sat_delete_clause_for_cs(satManager_t *m, satClause_t *c)
{
long j, csize, lit;

  csize = SATSizeClause(c);
  for(j=0; j<csize; j++) {
    lit = c->lits[j]; 
    m->nOccurrence[lit]--; 
    if(m->elimOrderArray[lit>>1] == 0) /** if variable is not eliminated **/
      sat_heap_update(m, m->eliminateHeap, lit>>1);
  }

  sat_delete_watched_literal(m, c);
  if(c->dependent)
    free(c->dependent);
}


long
sat_subsumption_check(satManager_t *n, satClause_t *c, satClause_t *ct)
{
long lit;
int i, j;

  if((SATSizeClause(ct) < SATSizeClause(c)) ||
     (c->info.abstract & ~ct->info.abstract)) 
    return(-1);

  lit = 0;
  for(i=0; i<SATSizeClause(c); i++) {
    for(j=0; j<SATSizeClause(ct); j++) {
      if(c->lits[i] == ct->lits[j])     goto cond;
      else if(lit == 0 && c->lits[i] == ~ct->lits[j]) {
        lit = c->lits[i];
        goto cond;
      }
    }
    return(-1);
    cond:;
  }
  return(lit);
}
#endif

#ifdef CHECK_EQUIVALENCE_RELATION
void
sat_clean_up_equi_job(satManager_t *m, satArray_t *save0)
{
long j, lit, v;

  for(j=0; j<save0->size; j++) {
    lit = save0->space[j];
    v = lit>>1;
    m->dummy[v] = 1;
    m->equi[v] = 0;
  }

  j = m->decisionStackSeperator->space[0];
  for(; j<m->stackPos; j++) {
    lit = m->decisionStack[j];
    v = lit>>1;
    m->dummy[v] = 1;
    m->equi[v] = 0;
  }
}

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

  conflicting = 0;

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

    if(wl == 0) continue;

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

      iLit = lit ^ 1;
      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 = SATSizeClause(c);
        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);
            goto foundWatch;
          }
        }

        *j++ = c;
        if((m->values[first>>1]^SATSign(first)) == 0) {
          conflicting = c;
          m->curPos = m->stackPos;
          while(i<end)  *j++ = *i++;
        }
        else {
          sat_enqueue(m, first, c);
          m->equi[first>>1] += m->values[first>>1] + 4;
        }
      }
foundWatch:;
    }
    wl->size -= i-j;
  }
  return(conflicting);
}
void
sat_check_equivalent_relation(satManager_t *m)
{
long i, j, k;
long lit, v;
long sSize;
long nEqui, nPos, nNeg;
long mapping;
long size;
satClause_t *c;
satArray_t *save0, *qArr;
satArray_t *candidate;
satHeap_t *h;

  h = m->variableHeap;
  size = m->nVars * 5 / 100;
  candidate = sat_array_alloc(size);
  i=0;
  while(i<size) {
    v = sat_heap_remove_min(m, m->variableHeap);
    candidate = sat_array_insert(candidate, v);
    i++;
  }

  save0 = sat_array_alloc(1024);
  qArr = sat_array_alloc(1024);
  nPos = nNeg = nEqui = 0;

/**
  for(i=1; i<=m->nVars; i++) {
**/
  for(k=0; k<candidate->size; k++) {
    i = candidate->space[k];
    if(m->values[i] < 2)  continue;
    if(m->dummy[i])  continue;

    save0->size = 0;
    qArr->size = 0;
    m->decisionStackSeperator = 
          sat_array_insert(m->decisionStackSeperator, m->stackPos);
    sat_enqueue(m, (i<<1)+1, 0);
    c = sat_check_equivalent_relation_aux(m);
    if(c) {
      sat_clean_up_equi_job(m, save0);
      sat_undo(m, 0);
      sat_enqueue(m, (i<<1), 0);
      c = sat_implication(m);
      if(c)     {
        m->status = 0;
        return;
      }
      continue;
    }
    sSize = m->stackPos-m->decisionStackSeperator->space[0];
    save0 = sat_array_realloc(save0, sSize);
    memcpy(&(save0->space[0]), &(m->decisionStack[m->decisionStackSeperator->space[0]]), sizeof(long)*sSize);
    save0->size = sSize;
    sat_undo(m, 0);

    m->decisionStackSeperator = 
          sat_array_insert(m->decisionStackSeperator, m->stackPos);
    sat_enqueue(m, (i<<1), 0);
    c = sat_check_equivalent_relation_aux(m);
    if(c) {
      sat_clean_up_equi_job(m, save0);
      sat_undo(m, 0);
      sat_enqueue(m, (i<<1)+1, 0);
      c = sat_implication(m);
      if(c)     {
        m->status = 0;
        return;
      }
      continue;
    }

    j = m->decisionStackSeperator->space[0];
    for(; j<m->stackPos; j++) {
      lit = m->decisionStack[j];
      v = lit>>1;
      if(m->equi[v] < 8)        continue;
      if(m->equi[v] == 8) {
        qArr = sat_array_insert(qArr, ((v<<1) + 1));
        nNeg++;
/**
        fprintf(stdout, "%d is always '0' regardless of variable %d\n", (int)v, (int)i);
           set variable to 0
**/
      }
      else if(m->equi[v] == 10) {
        qArr = sat_array_insert(qArr, (v<<1));
        nPos++;
/**
        fprintf(stdout, "%d is always '1' regardless of variable %d\n", (int)v, (int)i);
          set variable to 1
**/
      }
      else {
        if(m->values[i] == m->values[v])m->maps[v] = i;
        else                            m->maps[v] = -i;
        nEqui++;
/**
        fprintf(stdout, "equivalence relation between %d and %d\n", (int)i, (int)v);
          equivalence relation between i, v
          to identify more details, check values...
**/
      }
    }


    sat_clean_up_equi_job(m, save0);
    sat_undo(m, 0);

    for(j=0; j<qArr->size; j++) {
      lit = qArr->space[j];
      sat_enqueue(m, lit, 0);
    }
    if(qArr->size) {
      j = m->stackPos;
      c = sat_implication(m);
      if(c)     {
        m->status = 0;
        return;
      }
    }
  }

  memset(m->dummy, 0, sizeof(char)*(m->nVars+1));
  free(save0);
  free(qArr);

  for(i=0; i<candidate->size; i++) {
    v = candidate->space[i];
    if(h->indices[v] < 0 && m->values[v] == 2) 
      sat_heap_insert(m, m->variableHeap, v);
  }
  free(candidate);

  fprintf(stdout, "%d %d %d equivalent cases are detected\n", (int)nPos, (int)nNeg, (int)nEqui);
  if(nEqui) {
    for(i=1; i<=m->nVars; i++) {
      mapping = sat_get_mapped_index(m, i);
      m->maps[i] = mapping;
    }
    sat_update_equivalent_class(m, m->clauses, 0);
    sat_update_equivalent_class(m, m->learned, 1);
  }
}

void
sat_update_equivalent_class(satManager_t *m, satArray_t *arr, long learned)
{
satClause_t *c, *nc;
long i, csize, j;
long k;
long v, nv, sign, nvsign;
long lit;
long nModified;
long modified;
satArray_t *litArr;
  
  litArr = sat_array_alloc(1024);
  nModified = 0;
  for(i=j=0; i<arr->size; i++) {
    c = (satClause_t *)arr->space[i];
    csize = SATSizeClause(c);
    modified = 0;
    for(k=0; k<csize; k++) {
      lit = c->lits[k];
      sign = lit&1;
      v = lit>>1;
      nv = m->maps[v];
      if(v != nv) {
        modified = 1;
        break;
      }
    }

    if(modified) {
      litArr->size = 0;
      for(k=0; k<csize; k++) {
        lit = c->lits[k];
        sign = lit&1;
        v = lit>>1;
        nv = m->maps[v];
        if(v != nv) {
          nvsign = (nv<0) ? 1 : 0;
          nv = (nv<0) ? -nv : nv;
          litArr = sat_array_insert(litArr, (nv<<1) + (nvsign^sign));
        }
        else {
          litArr = sat_array_insert(litArr, lit);
        }
      }
      nc = sat_add_clause_only(m, litArr, learned);
      if(nc) {
        arr->space[j++] = (long)nc;
        nModified++;
      }
      sat_delete_clause(m, c);
    }
    else 
      arr->space[j++] = arr->space[i];
  }
  arr->size -= (i-j);
/**
  fprintf(stdout, "%d were modified and %d were satisfied\n", nModified, (i-j));
**/
  free(litArr);
}

long
sat_get_mapped_index(satManager_t *m, long index)
{
long mapping;

  mapping = m->maps[index];
  if(index == mapping)  return(m->maps[index]);
  if(mapping < 0)       return(-(sat_get_mapped_index(m, -mapping)));
  else                  return(sat_get_mapped_index(m, mapping));
}

#endif