solver.cpp

最快速的可满足性分析工具软件

/* 
 * solver.cpp: The file that contains all the core functions for a SAT solver.
 * We intend to make this file as self-contained as possible including any 
 * low-level function that are unnecessary to the main execution flow.
 * 
 * The following functions are in this file:
 * - solve (the main solving function)
 * - select_variable
 * - set_decision
 * - bcp (unit propagation)
 * - backtrack
 * - analyze_conflict 
 * - derive_conflict_clause
 * - removable (helper for derive_conflict_clause)
 * - assert_conflict_clause
 * - get_luby (for restarting)
 * - process_unit_literal_queue
 *
 */
#include <stdlib.h>
#include <stdio.h>
#include <iostream>
#include <assert.h>
#include <math.h>

#include "flags.h"
#include "structures.h"
#include "constants.h"

extern my_manager* my_m;
clock_t start_time,end_time;

#if(TIME_OUT)
extern double time_out;  //time out limit
extern clock_t start_t;  //the starting time of the solver
#endif

/*
 * Return the ith number of the luby sequence.
 * This function is called to determine the restarting schedule.
 *
 */
int get_luby(int i)
{
  if(i==1){return my_m->luby_unit;}  
  double k = log2(i+1);
  
  if(k==round(k)){
    return (int)(pow(2,k-1))*my_m->luby_unit;
  }else{
    k = (int)floor(k);
    return get_luby(i-(int)pow(2,k)+1);
  }
}//end function get luby

/*
 * Helper function for derive_conflict_clause.
 * Used to perform conflict clause minimization.
 * Return 1 if literal l can be removed from the current
 * conflict clause (in cdc) without introducing any new
 * literal.
 *
 * minl is a simple hash function which could quickly tell
 * us that l cannot be removed.
 * 
 *
 * stack contains the literals yet to be resolved away.
 * save contains the indices of variables on the stack.
 *
 * The main idea for this function is the keep resolving away literals 
 * on the stack until none is left. If at the end of the process,
 * no new literal is introduced, the literal can be removed.
 * Otherwise, the literal cannot be removed.
 *
 * This process of conflict minimization is really a partial implementation
 * of the AllUIP approach. We perform additional resolutions on all literals 
 * at lower level of see if the contribution from each level can be represented
 * with fewer literals or not.
 */
inline char removable(my_lit l,unsigned int minl)
{  
  //this seen array currently contains a 1-flag for each literal in the conflict clause.
  char* seen = my_m->seen;
  my_lit* stack = my_m->stack;
  int stack_index = 0;
  int stack_size = my_m->stack_size;
  int* save = my_m->save;
  int save_size = my_m->save_size;
  int size = 0;
  my_clause** reasons = my_m->reason;
  int* levels = my_m->level;
  
  //initially, the stack contains only the literal in question
  stack[stack_index++] = l;
  
  //main while loop
  //loop until all literals on the stack have been resolved away.
  while(stack_index>0){
    stack_index--;
    
    //pop a literal from the stack
    my_lit cur = stack[stack_index];
    my_var cur_v = var(cur);
    //inspect its reason
    my_clause* reason = reasons[cur_v];

    my_lit* lits = reason->lits;
    int rsize = reason->size;    
    int begin = 1;//是否因为第一个是要考察的literal 本身?

    //for each literal in the reason
    for(int i=begin;i<rsize;i++){     
      my_lit cur_lit = lits[i];
      my_var index = var(cur_lit); //the variable index of this literal
      int level = levels[index];

      //if seen[index]==1, this literal already involved in the conflict analysis. 
      //if seen[index]==0, this literal is not in the conflict. But, perhaps, all its antecedents are involved. We need to keep on looking.

      if(!seen[index]&& level != 1){

	//At this point, we know this literal is not directly in the conflict analysis (because seen is 0).
	//Here we check if this literal's antecedents are all be involved in the conflict analysis.
	//if this literal is a decision literal (the else case below), too bad. It does not even have any antecedent. Return false.
	//if (1<< (this literal's level)) & minl == 0 (also the else case), it means (guarantees) no literal of the level were present in the conflict analysis.
	//this just implies that this current literal (cur_lit) can never satisfy the condition above, return false.	
	//otherwise, this literal MAY have all antecedent present in the conflict analysis, push it on the stack for further inspection.
	if( (reasons[index]!=NULL) && ((1<< (level)) & minl)){
	  //this literal is promising, push it on the stack and remember it in save array.
	  seen[index] = 1;
	  
	  if(stack_index>=stack_size){
	    double_stack_len();
	    stack_size = my_m->stack_size;
	    stack = my_m->stack;
	  }

	  if(size>=save_size){
	    double_save_len();
	    save_size = my_m->save_size;
	    save = my_m->save;
	  }

	  stack[stack_index++] = cur_lit;
	  save[size++] = index;
	}else{
	  //this literal, l, is NOT removable
	  //since l is not removable, we need to clean up all the seen entries
	  //that we set in this function call.
	  for(int j=0;j<size;j++){
	    seen[save[j]] = 0;
	  }

	  return 0;
	}//end if else

      }//end if !seen
    }//end for i
  }//end while
  
  //at this point, the literal l can be removed from the conflict clause.
  //Note how we do not clean up the seen array in this case. This is because
  //we know all those set entries have antecedents that meet the removing criteria.
  //We can simply remember this information so that future calls to this function
  //have a chance to do less work.

  return 1;
}//end function removable

/*
 * Derive an asserting conflict clause.
 * conf is the conflicting clause.
 * clevel is the level of the conflict.
 * *alevel must be set to the assertion level upon return.
 *
 * The idea is to keep resolving literals (at clevel) that are involved in 
 * the conflict by their reasons until we only have 1 literal 
 * at the level of the conflict left.
 *
 */
int derive_conflict_clause(my_clause* conf,int clevel,int* alevel)
{
  //number of literals at clevel.
  int num_lits_at_clevel = 0;
  my_lit next_lit = 0;
  my_lit* next_on_stack = my_m->assign_top;
  
  my_m->seen = (char*)calloc(my_m->vc+1,sizeof(char));//记录已经分析过的变量
  char* seen = my_m->seen;

  int assertion_level = 1;
  my_m->assertion_level = 1;
  
  my_m->cdc_index = 0;  
  my_lit* cdc = my_m->cdc;
  int cdc_size = my_m->cdc_size;
  
  int* levels = my_m->level;
  my_clause** reasons = my_m->reason;

  //save a place for the asserted literal. We will fill this spot later.
  cdc[my_m->cdc_index++] = 0;
  
  if(clevel<=1){
    //conflict is fatal, because it occurs at level 1 (top)    
    cdc[0] = 0;
    cdc[1] = 0;
    free(my_m->seen);
    my_m->seen = NULL;

    *alevel = 0;

    return 0;
  }

  //as long as we have more literals to resolve
  do{//到311　num_lits_at_clevel>0

    //debugging code
    if(conf==NULL){      
      print_location();
      printf("Inside derive conflict clause [%"i64d"]\n",my_m->conflicts);
      printf("Reason of literal [%d] is NULL\n",lit_index(next_lit));
      printf("Decision literal of level %d is [%d], # lits at clevel = %d\n",clevel,lit_index(*(my_m->decision_lit[clevel])),num_lits_at_clevel);
      exit(0);
    }
    
    int size = conf->size;			
    my_lit* lits = conf->lits;    
    int begin = (next_lit==0?0:1);
    
    //usually, we want to skip the first literal in the clause because
    //it is the literal we are resolving on. The only exception is the very first clause.
    for(int i=begin;i<size;i++){//到274
    
      //for each literal in clause conf
      //inspect each literal and decide whether
      //1) to put it in the learned clause OR
      //2) to resolve on it in the future
      my_lit cur_lit = lits[i];      
      int index = var(cur_lit); //variable index of the current literal
      int level = levels[index];
      
      //we can skip this literal if
      // 1) we have seen it before
      // 2) it is falsified at level 1 (we can always resolve away such literal by our top-level implication)
      if(!seen[index] && (level > 1)){//274
	//if we have not seen this variable
	//mark it seen and increase its score
	seen[index] = 1;
	increment_literal_score(cur_lit);  //increase scores of those involve in the conflict
	
	//there are 2 possible actions here
	// 1) if the literal is falsified at clevel, we must keep on resolving it.
	//    In this case, just increment num_lits_at_clevel is enough.
	// 2) if the literal is falsified at a lower level, we must add it to the conflict clause.
	if(level==clevel){
	  //this literal's value was set at clevel
	  num_lits_at_clevel++;

	}else{
	  //this literal's value was set before clevel
	  //add it to the conflict clause	
	  if(my_m->cdc_index>=cdc_size){
	    double_cdc_len();
	    cdc_size = my_m->cdc_size;
	    cdc = my_m->cdc;
	  }
	  
	  //put it in the cdc array
	  cdc[my_m->cdc_index++] = cur_lit;
	  
	}//end if else
      }//end if seen
    }//end for i
    //finish inspecting the current clause
    
    //now, we must find the next variable on stack that is involved in this conflict.
    //a variable is involved if it's seen entry is set to 1.
    while(1){
      next_on_stack--;
      assert(next_on_stack>=my_m->assign);

      int index = var(*next_on_stack);
      
      if(seen[index]){
	break;
      }
    }//end while 1
    
    next_lit = *next_on_stack;      //next_lit is now the next literal in the stack that is involved in the conflict
    my_var next_var = var(next_lit);
    seen[next_var] = 0;  //mark next_lit not seen, because we exclude it from the learned clause
    num_lits_at_clevel--; //coz we just expanded on next_lit
        
    //set conf to be the reason of next_lit
    if(reasons[next_var]!=NULL){
      conf = reasons[next_var];

      if(conf->index>=0){
	//only bump the activity of those clauses learned
	increment_clause_score(conf);
      }

    }else{
      //this should happen only if num_lits_at_clevel==0
      //we should be out of the loop next
      conf = NULL;
    }

  }while(num_lits_at_clevel>0);

  //now, we can put the asserted literal in the first position of the conflict clause.
  cdc[0] = neg(next_lit);
  seen[var(next_lit)] = 1;

  //end main conflict clause derivation
  
  
  //begin conflict clause mininimization
  int size = my_m->cdc_index;
  int i=size,j=size;

  unsigned int minl = 0;

  //first, compute a hash value for the literals in the cdc array
  //The ith bit of minl is 1 if some literal in the cdc array is falsified
  //at a level L such that l%32 == i.
  for (i = 1; i<size; i++){
    my_lit cur = cdc[i];
    int level = levels[var(cur)];
    minl |= 1 << (level & 31);       
  } 

  int start = 1;
  
  for (i = j = start; i < size; i++){
    my_lit cur = cdc[i];
    my_var cur_v = var(cur);
    
    //only retain this literal if either it is a decision literal or if it cannot be removed.
    //otherwise, we skip it (nothing to do in this case).
    if((reasons[cur_v]==NULL) || !removable(cur,minl)){
      int level = levels[cur_v];
      
      if(level>assertion_level){ 
	assertion_level = level; 
      }
      
      cdc[j++] = cdc[i];
    }
  }//end for i=j=X

  *alevel = assertion_level;  

  int final_size = size-(i-j);
  
  free(seen);
  my_m->seen = NULL;

  //i-j is the number of literals in the conflict clause skipped by the minimization step
  return final_size; //return the size of the conflict clause

}//end derive_conflict_clause

/*
 * Analyze the current conflict (from conflicting_clause) at clevel.
 * At the end, set my_m->conflict_clause to the derived conflict clause
 * and set my_m->assertion_level to the corresponding assertion level 
 * and set my_m->conflict_level to be clevel.
 * 
 * Another side-effect of this is to determine whether to turn progress saving
 * on or off. This is determined based on the value of my_m->next_sp_switch.
 */
void analyze_conflict(my_clause* conflicting_clause,int clevel)
{
  //control progress saving here.
  if(my_m->conflicts>=my_m->next_sp_switch){
    //flip the status of save_progress
    my_m->save_progress = 1-my_m->save_progress;
        
    //update threshold values
    int inc = 0;
    if(my_m->save_progress){
      //OFF==>ON
      my_m->on_th += my_m->on_th_inc;    
      inc = my_m->off_th;
    }else{
      //ON==>OFF
      my_m->off_th += my_m->off_th_inc;
      inc = my_m->on_th;
    }
    
    //schedule the next switch
    my_m->next_sp_switch += inc;
  }
  //done switching progress saving

  //begin conflict analysis
  
  my_m->conflict_level = clevel;
  ++my_m->conflicts;

  int assertion_level = 0;
  
  //derive an asserting conflict clause
  int size = derive_conflict_clause(conflicting_clause,clevel,&assertion_level);
  my_m->assertion_level = assertion_level;

  if(size>0){
    //a normal conflict clause
    //put it in a clause structure, initialize it and return.
    my_clause* conflict_clause = (my_clause*)calloc(1,sizeof(my_clause));
    my_lit* lits = (my_lit*)calloc(size,sizeof(my_lit));
    my_lit* cdc = my_m->cdc;
    
      
    for(int i=0;i<size;i++){
      lits[i] = cdc[i];
    }
    
    conflict_clause->size = size;
    conflict_clause->index = 1;
    conflict_clause->lits = lits;
    
    my_m->conflict_clause = conflict_clause;           
  }else{
    //size==0, this problem is UNSAT.
    //set assertion level to 0, the main solving function will take care of this.
    my_m->assertion_level=0;
    my_m->conflict_clause = NULL;
  }
  
}//end function analyze_conflict

/* 
 * Undo all literals at level above and including level.
 * After returning from this function, the decision level 
 * should be dest-1. Hence, the subsequent decision will be
 * made at level dest--the last level erased.
 * 
 */
void backtrack(int dest)
{
  //check this, otherwise, erase level will erase assignments of previous levels
  if(my_m->decision_level<dest){
    //this may happen if the solver tries to restart while at level 1 (top).
    return;
  }
  
  my_lit* target = my_m->decision_lit[dest];
  my_lit* stack = my_m->assign_top;
  int* level = my_m->level;
  my_lit* status = my_m->status;
  my_clause** reason = my_m->reason;
  my_lit* saved = my_m->saved;
  
  //for each assignment on the stack down to level dest.
  while(stack>target){

    stack--;
    my_lit l = *(stack);   
    my_var v = var(l);
    
    if(my_m->save_progress==1){
      //consider saving progress
      char relate = 0; 
      //even though by default, we save all assignments,
      //it is possible to be more selective in what we save.
      
      if(relate==0){
	//save progress
	saved[v] = l;
	
      }else if(relate==1){
	saved[v] = 0;
	
      }else if(relate==-1){
	//flip
	saved[v] = neg(l);