zchaff_solver.cpp

这是一种很好的SAT解析器。通过它

		break;
	    }
	    if (ptr->is_watched()) {
		other_watched = ptr;
		continue;
	    }
	    if (literal_value(*ptr) == 0) {
				//keep track of the 0 literal with max decision level
		int ptr_dl = variable(ptr->var_index()).dlevel();
		if ( ptr_dl > max_dl) {
		    max_dl = ptr_dl;
		    max_ptr = ptr;
		}
		continue;
	    }
	    //now it's value is either 1 or unknown
	    int v1 = ptr->var_index();
	    int sign = ptr->var_sign();
	    variable(v1).watched(sign).push_back(ptr);
	    watched->unwatch();
	    ptr->set_watch(dir);

	    *itr = watchs.back();
	    watchs.pop_back();
	    --itr;
	    break;
	}
    }
}

void CSolver::unset_var_value(int v)
{
    if (v == 0) return;
    DBG1(cout <<"Unset var " << (variable(v).value()?"+":"-") << v << endl;);
    CVariable & var = variable(v);
    var.set_value(UNKNOWN);
    var.set_antecedent(NULL_CLAUSE);
    var.set_dlevel( -1);
    var.assgn_stack_pos() = -1;

    if (var.is_branchable()) {
	++num_free_variables();
	if (var.var_score_pos() < _max_score_pos)
	    _max_score_pos = var.var_score_pos();
    }
}

int CSolver::find_max_clause_dlevel(ClauseIdx cl)
{
//if cl has single literal, then the dlevel for it should be 0
//thus, we need to set initial max_level = 0 instead
//of -1 because if clause has single literal, then the
//loop will found no literal with value UNKNOWN
    int max_level = 0;
    if (cl == NULL_CLAUSE) 
	return dlevel();
    for (unsigned i=0, sz= clause(cl).num_lits(); i<sz;  ++i) {
	int var_idx =((clause(cl).literals())[i]).var_index();
	if (variable(var_idx).value() != UNKNOWN) {
	    if (max_level < variable(var_idx).dlevel())
		max_level = variable(var_idx).dlevel();
	}
    }
    return max_level; 
}

void CSolver::dump_assignment_stack(ostream & os ) {
    os << "Assignment Stack:  ";
    for (int i=0; i<= dlevel(); ++i) {
	os << "(" <<i << ":";
	for (unsigned j=0; j<(*_assignment_stack[i]).size(); ++j )
	    os << ((*_assignment_stack[i])[j]&0x1?"-":"+")
		 << ((*_assignment_stack[i])[j] >> 1) << " ";
	os << ") " << endl;
    }
    os << endl;
}

void CSolver::dump_implication_queue(ostream & os) 
{
    _implication_queue.dump(os);
}

void CSolver::delete_clause_group (int gid)
{
    assert( is_gid_allocated(gid) );
    if (_stats.been_reset==false)
	reset(); //if delete some clause, then implication queue are invalidated
    for (vector<CClause>::iterator itr1 = clauses().begin(); 
	 itr1 != clauses().end(); ++itr1) {
	CClause & cl = * itr1;
	if (cl.status() != DELETED_CL) {
	    if (cl.gid(gid) == true) {
		mark_clause_deleted(cl);
	    }
	}
    }
    //delete the index from variables
    for (vector<CVariable>::iterator itr = variables().begin(); 
	 itr != variables().end(); ++ itr) {
	for (unsigned i=0; i<2; ++i) { //for each phase
	    //delete the lit index from the vars
#ifdef KEEP_LIT_CLAUSES
	    vector<ClauseIdx> & lit_clauses = (*itr).lit_clause(i);
	    for (vector<ClauseIdx>::iterator itr1 = lit_clauses.begin();
		 itr1 != lit_clauses.end(); ++ itr1) 
		if ( clause(*itr1).status() == DELETED_CL ) {
		    *itr1 = lit_clauses.back();
		    lit_clauses.pop_back();
		    -- itr1;
		}
#endif
	    //delete the watched index from the vars
	    vector<CLitPoolElement *> & watched = (*itr).watched(i);
	    for (vector<CLitPoolElement *>::iterator itr1 = watched.begin(); 
		 itr1 != watched.end(); ++itr1) 
		if ( (*itr1)->val() <= 0) {
		    *itr1 = watched.back();
		    watched.pop_back();
		    --itr1;
		}
	}
    }
    free_gid(gid);
}

void CSolver::reset(void)
{
    if (_stats.been_reset)
    	return;
    if (num_variables()==0) return;
    back_track(0);
    _conflicts.clear();
    while (!_implication_queue.empty())
	_implication_queue.pop();

    _stats.is_solver_started 	= false;
    _stats.outcome		= UNDETERMINED;
    _stats.been_reset 		= true;
}

void CSolver::delete_unrelevant_clauses(void)
{
    /*
    if (CDatabase::_stats.mem_used_up) {
	CDatabase::_stats.mem_used_up = false;
	if (++CDatabase::_stats.mem_used_up_counts < 5) {
	    DBG1(
		cout << "Forced to be more aggressive in clause deletion. " << endl;
		cout <<"MaxUnrel: " << _params.cls_deletion.max_unrelevance 
		<< "  MinLenDel: " << _params.cls_deletion.min_num_lits
		<< "  MaxLenCL : " << _params.cls_deletion.max_conf_cls_size << endl;
		);
	}
    }*/

    unsigned original_del_cls = num_deleted_clauses();
    int num_conf_cls=num_clauses()-init_num_clauses()+num_del_orig_cls();
    int head_count=num_conf_cls/_params.cls_deletion.tail_vs_head;
    int count=0;
    DBG2 (dump());
    for (vector<CClause>::iterator itr1=clauses().begin(); itr1 != clauses().end()-1; ++itr1) {
	CClause & cl = * itr1;
        bool cls_sat_at_dl_0=false;	
	if(cl.status()!=DELETED_CL){ 
	    for (int i=0, sz=cl.num_lits(); i<sz; ++i){
	        if (literal_value(cl.literal(i)) == 1 && variable(cl.literal(i).var_index()).dlevel()==0) {
        	    cls_sat_at_dl_0=true;
		    break;
	        }
	    }
	    if(cls_sat_at_dl_0 ){
		if(cl.status()==ORIGINAL_CL || cl.status()==CONFLICT_CL){
		    // deleting ORIGINAL clauses can change the initial starting value for VSIDS..
		    // deleting CONFLICT clauses will avoid future calls to is_satisfied on these clauses	
		    int val_0_lits = 0, val_1_lits = 0, unknown_lits = 0;
		    for (unsigned i=0; i< cl.num_lits(); ++i) {
		        int lit_value = literal_value (cl.literal(i));
		        if (lit_value == 0 )
		   	    ++val_0_lits;
			if (lit_value == 1) 
			    ++val_1_lits;
			if (lit_value == UNKNOWN) 
		            ++unknown_lits; 	
			if (unknown_lits+val_1_lits > 1 ) { 
			    mark_clause_deleted(cl);
			    break;
			}			
                    }
		    continue;	// if i didn't delete it now, i wont later either
		}
		
	    }
	}
        if (cl.status()!=CONFLICT_CL ) {
            continue;
        }
        
        count++;
	int max_activity=_params.cls_deletion.head_activity-(_params.cls_deletion.head_activity-_params.cls_deletion.tail_activity)*count/num_conf_cls;
	int max_conf_cls_size;//=_params.cls_deletion.head_num_lits+(_params.cls_deletion.tail_num_lits-_params.cls_deletion.head_num_lits)*count/num_conf_cls;
	
		
	if(head_count>0){
	    //max_activity=_params.cls_deletion.head_activity;
	    max_conf_cls_size=_params.cls_deletion.head_num_lits;
            head_count--;
	}
	else{
	    //max_activity=_params.cls_deletion.tail_activity;
	    max_conf_cls_size=_params.cls_deletion.tail_num_lits;
	}
        /*
        //WHY?
        if(cl.activity()<0)
            cl.activity()+=55;
        //if(cl.activity())
            cl.activity()--;
	*/
	if(cl.activity()>max_activity)	
	    continue;

      	int val_0_lits = 0, val_1_lits = 0, unknown_lits = 0,lit_value;
	for (unsigned i=0; i< cl.num_lits(); ++i) {
	    lit_value = literal_value (cl.literal(i));
	    if (lit_value == 0 ) 
		++val_0_lits;
	    else if (lit_value == 1) 
		++val_1_lits;
	    else
		++unknown_lits;
	    if ((unknown_lits>max_conf_cls_size)){
		if((unknown_lits+val_1_lits > 1 )) { 
		    mark_clause_deleted(cl);
		    DBG1 (cout << "Deleting Large clause: " << cl << endl;);
		}
	        else{
		// IF THIS ASSERTION FAILS, and we are just after restart, this tells us a var ought to be assigned
		    assert((dlevel()!=0) || ( unknown_lits!=0 && unknown_lits!=1));
		//    cout<<" SKIP - "<<unknown_lits<<' '<<val_1_lits<<endl;	
	        }
		break;
            }
        }
    }
    // if none were recently marked for deletion...
    if (original_del_cls == num_deleted_clauses()) 
        return;
    
    //delete the index from variables
    for (vector<CVariable>::iterator itr = variables().begin(); 
	 itr != variables().end(); ++ itr) {
	for (unsigned i=0; i<2; ++i) { //for each phase
	    //delete the lit index from the vars
#ifdef KEEP_LIT_CLAUSES
	    vector<ClauseIdx> & lit_clauses = (*itr).lit_clause(i);
	    for (vector<ClauseIdx>::iterator itr1 = lit_clauses.begin();
		 itr1 != lit_clauses.end(); ++ itr1) 
		if ( clause(*itr1).status() == DELETED_CL ) {
		    *itr1 = lit_clauses.back();
		    lit_clauses.pop_back();
		    -- itr1;
		}
#endif
	    //delete the watched index from the vars
	    vector<CLitPoolElement *> & watched = (*itr).watched(i);
	    for (vector<CLitPoolElement *>::iterator itr1 = watched.begin(); 
		 itr1 != watched.end(); ++itr1) {
		if ( (*itr1)->val() <= 0) {
		    *itr1 = watched.back();
		    watched.pop_back();
		    --itr1;
		}
	    }
	}
    }

    for (unsigned i=1; i<variables().size(); ++i) {
	if(variable(i).dlevel()!=0){
	    variable(i).score(0) = variable(i).lits_count(0);
	    variable(i).score(1) = variable(i).lits_count(1);

	    if(variable(i).lits_count(0)==0 && (variable(i).value()==UNKNOWN) ){
	        queue_implication(2*i+1,NULL_CLAUSE,0);
	    }
 	    else if(variable(i).lits_count(1)==0 && (variable(i).value()==UNKNOWN) ){
	        queue_implication(2*i,NULL_CLAUSE,0);
	    }
	}
	else{
	    variable(i).score(0)=variable(i).score(1)=0;	
	}
    }
    update_var_score();
    DBG1(cout << "Deleting " << num_deleted_clauses() - original_del_cls << " Clause ";
	 cout << " and " << num_deleted_literals() - original_del_lits << " Literals " << endl;);
    DBG2 (dump());
}
//============================================================================================
bool CSolver::time_out(void) 
{
    return (get_cpu_time() - _stats.start_cpu_time> _params.time_limit);
}

void CSolver::adjust_variable_order(int * lits, int n_lits) //note lits are signed vars, not CLitPoolElements
{
    for (int i=0; i<n_lits; ++i) {
	int var_idx = lits[i]>>1;
	int var_sign = lits[i]&0x1;
	CVariable & var = variable(var_idx);
	assert (var.value() != UNKNOWN);
	int orig_score = var.score();
	variable(var_idx).score(lits[i]&0x01)++;
	int new_score = var.score();
	if (orig_score == new_score) 
	    continue;
	int pos = var.var_score_pos();
	int orig_pos = pos;
	assert (_ordered_vars[pos].first == & var);
	assert (_ordered_vars[pos].second == orig_score);
	int bubble_step = _params.decision.bubble_init_step;
	for (pos = orig_pos ; pos >= 0; pos -= bubble_step)
	    if (_ordered_vars[pos].second >= new_score) break;
	pos += bubble_step;
	for ( bubble_step = bubble_step >> 1; bubble_step > 0; bubble_step = bubble_step >> 1) {
	    if ( pos - bubble_step >= 0) {
		if (_ordered_vars[pos - bubble_step].second < new_score)
		    pos -= bubble_step;
	    }
	}
	//now found the position, do a swap
	_ordered_vars[orig_pos] = _ordered_vars[pos];
	_ordered_vars[orig_pos].first->set_var_score_pos(orig_pos);

	_ordered_vars[pos].first = & var;
	_ordered_vars[pos].second = new_score;
	_ordered_vars[pos].first->set_var_score_pos(pos);

	_stats.total_bubble_move += orig_pos - pos;
    }
    CHECK(
	for (unsigned i=0; i< _ordered_vars.size(); ++i) {
	    assert (_ordered_vars[i].second == _ordered_vars[i].first->score());
	    assert (_ordered_vars[i].first->var_score_pos() == i);
	    assert (i==0 || _ordered_vars[i].second <= _ordered_vars[i-1].second );
	    assert (_ordered_vars[i].first->value() != UNKNOWN || _max_score_pos <= i);
	});

}

void CSolver::decay_variable_score(void) 
{
    unsigned int i, sz;
    for(i=1, sz = variables().size(); i<sz; ++i) {
	CVariable & var = variable(i);
	var.score(0) = var.score(0)/2;//4
	var.score(1) = var.score(1)/2;//4
    }
    for (i=0, sz = _ordered_vars.size(); i<sz; ++i) {
	_ordered_vars[i].second = _ordered_vars[i].first->score();
    }
}

bool CSolver::decide_next_branch(void)
{
    if(dlevel()>0)
        assert(_assignment_stack[dlevel()]->size()>0);
    //cout<<_assignment_stack[dlevel()]->size()<<endl;
    CHECK(verify_integrity());
    if (!_implication_queue.empty()) {
	//some hook function did a decision, so skip my own decision making.
	//if the front of implication queue is 0, that means it's finished
	//because var index start from 1, so 2 *vid + sign won't be 0. 
	//else it's a valid decision.
	return (_implication_queue.front().lit != 0);
    }
    int s_var=0;
    if(_params.shrinking.enable){
        while(!_shrinking_cls.empty()){
	    s_var=_shrinking_cls.begin()->second;
            _shrinking_cls.erase(_shrinking_cls.begin());
	    if(variable(s_var>>1).value()==UNKNOWN){
                _stats.num_decisions++;
                _stats.num_decisions_shrinking++;
	        ++dlevel();
	        queue_implication(s_var^0x01,NULL_CLAUSE,dlevel());
                return true;
	    }
        }
    }
//    add_outside_clauses();
    if (_outside_constraint_hook != NULL)
	_outside_constraint_hook(this);

    if (!_implication_queue.empty())
	return (_implication_queue.front().lit != 0);
    
    ++_stats.num_decisions;
   if (num_free_variables() == 0) //no more free vars
	return false;
     
    bool cls_sat;
    int i,sz,var_idx,score,max_score=-1;