solver.cpp

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

      }//end if else relate==0,1,-1
      
    }
    
    //reset various fields.
    reason[v] = NULL;
    level[v] = 0;
    status[v] = 0;
    //put the variable back in the variable heap.
    undo(my_m->var_order_heap,v);      
  }//end main while loop
  
  my_m->assign_top = stack;
  my_m->decision_level = dest-1; //restore the decision level so that the next decision is made at level dest.  
}//end function backtrack

/*
 * Apply unit propagation to all literals currently on the assignment stack.
 * This function is intended to be called after we finish reading the input file.
 *
 * Return 1 iff a conflict is found.
 */
char process_unit_literal_queue()
{
  //check the implication queue to see if there is any enqueued implication.
  my_var v = dequeue(my_m->imp);

  if(v!=0){
    //if there is, call bcp.
    my_m->simplify_orig_kb = 1;
    my_m->simplify_learned_kb = 1;
    my_m->stack_offset--;
    int res = bcp(my_m->status[v]);    
    my_m->stack_offset = 0;
    return res;
  }
  
  //no enqueued implication, return 1.
  return 1;
}//end function process unit literal queue

/*
 * Perform unit propagation starting at the assignment of literal l.
 * Return 1 if no conflict arises, otherwise return 0.
 *
 * In case of conflict, call analyze_conflict before returning.
 */
char bcp(my_lit l)
{
  //last points to the most recent implication on the assignment stack.
  my_lit* last = my_m->assign_top;//第一次BCP之前始终为0，之后再是最近的
  int* level = my_m->level;
  my_lit* status = my_m->status;
  my_clause** reason = my_m->reason;
  my_clause*** watched = my_m->watched;
  int* watched_size = my_m->watched_size;  
  int slevel = level[var(l)];
  implication_queue* q = my_m->imp;
  
  //put this literal (l) into the priority queue 
  undo(q,var(l));

  *(last++) = l;

  status[var(l)] = l;
  
  //usually, stack_offset is 0. It could be > 0 only at the first call 
  //to bcp when we implications enqueued in the assignment stack (see process_unit_literal_queue).
  //stack_offset has compensated for *(last++) above
  last += my_m->stack_offset;

  my_var v;
  
  //keep dequeuing variable from the implication queue
  while((v=dequeue(q))!=0){//到680
    my_lit lit = status[v];
    my_lit neg_lit = neg(lit);
    int wi = watched_index(neg_lit); //wi is the array index of neg_lit
    //since neg_lit is now false, we need to traverse its watched list.
    
    //the watched list of neg_lit
    my_clause** watched_list = watched[wi];
    my_clause** pointer = watched_list;
    my_clause** end = watched_list+watched_size[wi];
    
    //for each clause in the watched list of neg_lit
    //find a new literal to watch
    while(watched_list<end){//到676

      my_clause* clause = *(watched_list++);
      my_lit* lits = clause->lits;

      my_lit first_lit = lits[1];
      
      //make sure that neg_lit is in the second position in the array,只对前两个lit进行监视
      if(first_lit!=neg_lit){
	lits[1] = lits[0];
	lits[0] = first_lit;		
      }
      
      if(set(lits[0])){//这个子句早就成立 了
	//this clause is already satisfied, skip it
	//put it in the same watched list (even though this current literal is already falsified!)	为什么不删除?    
	
	*(pointer++) = clause;
	continue;
      }
      
      int clause_size = clause->size;
	  
      //search for an un-falsified literal in lits[2...n]
      //note that if clause_size==2, then there is nothing to search.
      //the current clause is guaranteed to be either unit or empty.
      if(clause_size>2){//到617
	
	char found = 0;
	my_lit temp = lits[1];
	    
	int k = 2;
	for(;k<clause_size;k++){
	  my_lit temp2 = lits[k];
	  if(unresolved(temp2)){//统一只能前两个lit 监视出子句		
	    lits[1] = temp2;
	    lits[k] = temp;
	    //add this current clause to the watched list of the new found literal.
	    add_watched_clause(temp2,clause);//把这个clause移到temp2上去了
	    
	    found = 1;
	    break;
	  }
	}//end for k

	if(found){
	  //done with this clause, move on to the next clause
	  continue;
	}
	
      }//end if clause_size > 2
      
      //at this point, we know we could not find a new unresolved literal from lits[2..n]
      //(this is because alls of them are resolved or none of them even exits)
      //all we have to do now is check whether there is a conflict or not
      //basically, if lit[0] is free, we have a unit clause
      //if lit[0] is falsified, we have a contradiction!
	
      my_lit other_lit = lits[0];
      if(status[var(other_lit)]==neg(other_lit)){//到654
	
	//here, we must pop everything out of the queue
	//move stack_top to last
	//because every literal on the stack has a chance of participating in the conflict
	//[even if it is not yet processed]
	
	while((v=dequeue(q))!=0){
	}
	
	my_m->assign_top = last;
	
	//move the rest of neg_list watched clauses into their appropriate positions
	*(pointer++) = clause;
	while(watched_list<end){
	  *(pointer++) = *(watched_list++);
	}
	      
	watched_size[wi] -= watched_list-pointer;	//总数减去被别人监视的子句的所有子句包括已成立、有错误的、还unit子句
	
	//set the conflicting clause to this clause so
	//that we can later perform conflict analysis correctly.
	my_m->conflicting_clause = clause;

	assert(last==my_m->assign_top);	      
	
	return 0;	
      }else{//674
	
	//we have a unit implication in this case
	my_lit unit_lit = other_lit;
	my_var unit_var = var(unit_lit);
	    
	if(status[unit_var]==0) {
	  //this literal is implied for the first time
	  
	  reason[unit_var] = clause;	  
	  status[unit_var] = unit_lit;
	  level[unit_var] = slevel;

	  //put this unit variable into the implication queue
	  undo(q,unit_var);
	  *(last++) = unit_lit;
	  
	}//end if else unit for the first time
	    
	*(pointer++) = clause;
      }//end if else
	  
    }//end while more clauses in watched list of neg_lit		
    
    watched_size[wi] -= watched_list-pointer;//总数减去被别人监视的子句的所有子句包括已成立、有错误的、还unit子句

  }//end while more literal to process
  
  my_m->assign_top = last;
  return 1;
}//end function bcp

/*
 * Add the current conflict clause to the knowledge base
 * and apply unit propagation (call bcp) on it.
 * Return 0 iff unit propagation derives a conflict.
 *
 */
char assert_conflict_clause()
{
  if(my_m->vc>VC_THRESHOLD && my_m->decision_level<my_m->decision_lit_size/4){
    half_decision_lit_len();
  }
  
  my_clause* conflict_clause = my_m->conflict_clause;
  int size = conflict_clause->size;
  
  if(size>1){
    //Add this conflict clause to the knowledge base only if it is not unit.
    add_conflict_clause();
  }

  my_lit fuip = conflict_clause->lits[0];
  my_var fuip_var = var(fuip);
  my_m->level[fuip_var] = my_m->assertion_level;
  
  my_m->reason[fuip_var] = (size>1?conflict_clause:NULL);
  
  if(size==1){
    free(conflict_clause->lits);
    free(conflict_clause);
    my_m->conflict_clause = NULL;
    my_m->simplify_orig_kb = 1;
    my_m->simplify_learned_kb = 1;
  }

  my_m->score_inc *= my_m->score_inc_factor;
  my_m->clause_score_inc *= CLAUSE_SCORE_INC_FACTOR;    

  return bcp(fuip);
}//end function assert conflict clause

/*
 * Set literal l to true. Set this literal to be the decision literal of the level.
 * Propagate its effects (by calling bcp).
 * Returns 0 iff bcp can derive a conflict.
 *
 */
char set_decision(my_lit l) 
{
  if(my_m->decision_level > my_m->max_decision_level) {
    my_m->max_decision_level = my_m->decision_level;
  }

  int level = ++(my_m->decision_level);
  ++(my_m->decisions);  
  
  my_var v = var(l);
  my_m->level[v] = level;
  my_m->reason[v] = NULL;
  
  if(level>=my_m->decision_lit_size){
    double_decision_lit_len();
  }

  my_m->decision_lit[level] = my_m->assign_top;  

  return bcp(l);
}//end function set decision

/*
 * Return the free variable with the highest score.
 * Return 0 if no free variable remains.
 *
 */
my_var select_variable()
{

#if(USE_RANDOM_ORDER)
  double random_var_freq = 0.2;
  
  double r = (double)rand()/RAND_MAX;

  if(r < random_var_freq){
    my_var next = my_m->vc*((double)rand()/RAND_MAX)+1;
    if(my_m->level[next]==0){
      return next;
    }//end inner if
  }//end if
#endif

  heap* h = my_m->var_order_heap;

  while(!empty(h)){
    my_var next = get_min_element(h);   //this takes care of restructuring heap
    if(my_m->level[next]==0){
      //if this variable is free, return it
      
      return next;
    }//end if
  }//end while

  //no more free variable:SAT
  return 0;
}//end function select variable

/*
 * The main solving function.
 * Solve the SAT problem stored in the manager my_m.
 * Return 1 if SAT, 0 if UNSAT, and -1 if UNKNOWN (timeout).
 *
 * The idea is to keep making decisions until either a solution 
 * or a conflict is found. 
 * 
 * If a solution is found, return.
 * If a conflict is found, perform conflict analysis, backtrack, 
 * and apply bcp to the new cluase. This is repeated until no
 * conflict remains. Then the solver continue to the loop.
 * 
 */
int solve()
{
  start_time = clock();
  
  my_m->previous_decision_count = 0;
  my_m->previous_conflicts = 0;
  my_m->previous_reduce_kb_count = 0;
  my_m->previous_simplify_kb_count = 0;
  
  //we use the value of result to determine when to return from this function
  //result==-2 means that we have not found a solution.
  int result = -2;
    
  //this is the main loop. Each iteration is 1 decision
  while(1){        

    if(result==0){
      //UNSAT, break and return.
      break;
    }


    /******************************************
     *
     * Loop invariant: 
     * At this point of the loop, the 
     * solver state is closed under
     * unit resolution and is 1-consistent.
     * In other words, unit propagation
     * cannot derive any implication at
     * this point, and there is no 
     * conflict.
     * 
     * 
     * The next thing we do is to check whether 
     * it is time to restart or not, then we
     * check if it is time to manage the knowledge 
     * base or not (simplify, delete,...).
     * After all these, we pick a decision variable
     * and make a decision on it.
     *
     *******************************************/

#if(TIME_OUT)
    //rough implementation of timeout
    if(my_m->decisions%2000==0 && time_out>0){
      double elapsed = get_cpu_time();
      if(elapsed > time_out){
	backtrack(2);
	return -1;
      }
    }
#endif//endif time out

    if(my_m->conflicts>=my_m->next_restart_conflict){	
      //time to restart
      //note how we do not change the value of result (-2).
	
      print_progress();

      backtrack(2);

      my_m->restart++;

      int restart = my_m->restart;
      my_m->restart_conflict_incr = get_luby(restart+1);
      my_m->next_restart_conflict = my_m->conflicts + (int)my_m->restart_conflict_incr;
	
      simplify_original_kb();
    }//endif meet restart criteria

    if(my_m->simplify_learned_kb && my_m->decision_level==1 && my_m->conflicts >= my_m->num_conflicts_for_next_simplify){
      simplify_kb();
    }

    int num_assigned = (my_m->assign_top - my_m->assign);
      
    if(my_m->cur_cdc_count >= my_m->max_learned_clauses + num_assigned){
      reduce_kb();
    }

    /*****************************************************
     *
     * End checking restarting criteria and managing KB.
     *
     *****************************************************/
    
    //Jump directly to the label "pre_decision" if you want a clean way of bypassing the call to select_variable
    
    my_lit literal;
      
    //select a variable as the decision variable
    my_var dec_var = select_variable();
    
    if(dec_var==0){      
      //solution found!!
      result = 1;      	
      print_progress();
      
#if(VERIFY_SOLUTION)
      save_solution();
#endif
      print_progress_footer();
	
      if(my_m->print_mode==2){
	print_solution();
      }
	
      backtrack(2);
      break;
    }//endif solution found      
    
    //decide which phase of dec_var to try first
    if(my_m->saved[dec_var]==0 || !my_m->save_progress){	
      literal = nlit(dec_var);
    }else{	
      literal = my_m->saved[dec_var];
    }//end if else use saved phase or not
      
    //literal must be already set at this point!
    //pre_decision: //currently, this label is not used

    //make the decision
    char res = set_decision(literal);                
    //res is 1 if everything was okay, 0 if there was a conflict

    //deal with conflict, if any.
    while(res!=1){//948
      //at this point, the current state of the solver has a conflict.
      
      //analyze the conflict (derive conflict clause).
      analyze_conflict(my_m->conflicting_clause,my_m->decision_level);

      if(my_m->assertion_level==0){
	//UNSAT!
	result = 0;
	break;
      }
      
      //backtrack to the assertion level (erase upto assertion level+1)
      backtrack((my_m->assertion_level)+1);
      //assert the conflict clause
      res = assert_conflict_clause();
      //at this point of the program, we are done with the assertion (may have resulted in success or another conflict)
    }//end while conflict
      
    //at this point, we do not have a contradiction
    //in the current state.
      
  }//end while not time to restart or solution found
    
  //at this point, result is either 0 or 1.
  return result;

}//end function solve