zchaff_solver.cpp

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

    vector<int> real_conflict_lits;

    ClauseIdx cl = _conflicts[0];
    DBG0(cout <<"Conflict clause: " << cl << " : " << clause(cl) << endl;);
    mark_vars_at_current_dlevel (cl, -1 /*var*/);
    unsigned gflag = clause(cl).gflag();
    vector <int> & assignments = *_assignment_stack[dlevel()]; //current dl must be the conflict cl.
    for (int i=assignments.size()-1; i >= 0; --i) { //now add conflict lits, and unassign vars
	int assigned = assignments[i];
	if (variable(assigned>>1).is_marked()) {  
	    //this variable is involved in the conflict clause or it's antecedent
	    variable(assigned>>1).clear_marked();
	    -- _num_marked; 
	    ClauseIdx ante_cl = variables()[assigned>>1].get_antecedent();
	    if ( _num_marked == 0 ) { 
				//the first UIP encountered
		real_conflict_lits.push_back(assigned ^ 0x1); //this is the flipped lit
		break;
	    }
	    else {
		assert ( ante_cl != NULL_CLAUSE );
		gflag |= clause(ante_cl).gflag();
		mark_vars_at_current_dlevel(ante_cl, assigned>>1/*var*/);
	    }
	}
    }
    //at this point, real_conflict_lits has the firstUIP, _conflict_lits has the vars involved in other dlevel
    vector<int> current;
    for (int dl = dlevel() - 1; dl > 0; --dl) {
	DBG1(cout << "Processing Dlevel " << dl << endl; );
	current.swap(_conflict_lits);
	_conflict_lits.clear();
	assert (_num_marked == 0);
	mark_vars_of_dl(current, dl);
	if (_num_marked == 0) //conflict does not involve this level
	    continue;
	vector <int> & assignments = *_assignment_stack[dl]; 
	for (int i=assignments.size()-1; i >= 0; --i) { //now add conflict lits, and unassign vars
	    int assigned = assignments[i];
	    if (variable(assigned>>1).is_marked()) {  
				//this variable is involved in the conflict clause or it's antecedent
		variable(assigned>>1).clear_marked();
		-- _num_marked; 
		ClauseIdx ante_cl = variables()[assigned>>1].get_antecedent();
		if ( _num_marked == 0 ) { 
		    //UIP encountered
		    real_conflict_lits.push_back(assigned^0x1);  // add this assignment
		    DBG1(cout << "Put " << (assigned&0x1 ? "+":"-") << (assigned >> 1) << "in conflict clause" << endl;);
		    break; //go on to the next level
		}
		else {
		    assert ( ante_cl != NULL_CLAUSE );
		    gflag |= clause(ante_cl).gflag();
		    mark_vars_at_level(ante_cl, assigned>>1/*var*/, dl);
		}
	    }	    
	}
    }
    assert (_num_marked == 0);
    for (unsigned j=0; j< real_conflict_lits.size(); ++j ) {
	int svar = real_conflict_lits[j];
	assert (variable(svar>>1).new_cl_phase() == UNKNOWN);
	variable(svar>>1).set_new_cl_phase(svar & 0x1);
	_conflict_lits.push_back(svar);
	++ _num_in_new_cl;
    }
    return finish_add_conf_clause(gflag);
}

int CSolver::conflict_analysis_lastUIP(void)
{
    //For experiment purpose only, don't use it 
    ClauseIdx cl = _conflicts[0];
    mark_vars_at_current_dlevel (cl, -1 /*var*/);
    unsigned gflag = clause(cl).gflag();
    vector <int> & assignments = *_assignment_stack[dlevel()]; //current dl must be the conflict cl.
    for (int i=assignments.size()-1; i >= 0; --i) { //now add conflict lits, and unassign vars
	int assigned = assignments[i];
	if (variable(assigned>>1).is_marked()) {  
	    //this variable is involved in the conflict clause or it's antecedent
	    variable(assigned>>1).clear_marked();
	    -- _num_marked; 
	    ClauseIdx ante_cl = variables()[assigned>>1].get_antecedent();
	    if ( ante_cl == NULL_CLAUSE ) { //last UIP is the decision varialbe
		assert (i == 0);	     
		assert (_num_marked == 0); //last UIP is still a UIP
		assert (variable(assigned>>1).new_cl_phase() == UNKNOWN);
		_conflict_lits.push_back(assigned^0x1);  // add this assignment's reverse, e.g. UIP
		++ _num_in_new_cl;
		variable(assigned>>1).set_new_cl_phase((assigned^0x1)&0x1);
	    }
	    else {
		assert ( ante_cl != NULL_CLAUSE );
		gflag |= clause(ante_cl).gflag();
		mark_vars_at_current_dlevel(ante_cl, assigned>>1/*var*/);
	    }
	}
    }
    return finish_add_conf_clause(gflag);
}

int CSolver::conflict_analysis_firstUIP (void) 
{
    int min_conf_id=_conflicts[0];
    int min_conf_length=-1;
    ClauseIdx cl;
    unsigned gflag; 
    _mark_increase_score=false;
    if(_conflicts.size()>1){
        for(vector<ClauseIdx>::iterator ci=_conflicts.begin();ci!=_conflicts.end();ci++){
            assert (_num_in_new_cl==0);
            assert (dlevel() > 0);
            cl = *ci;
            clause(cl).activity()++;
            DBG0(cout <<"Conflict clause: " << cl << " : " << clause(cl) << endl;);
            mark_vars_at_current_dlevel (cl, -1 /*var*/);
            gflag = clause(cl).gflag();
            vector <int> & assignments = *_assignment_stack[dlevel()]; //current dl must be the conflict cl.
            for (int i=assignments.size()-1; i >= 0; --i) { //now add conflict lits, and unassign vars
                int assigned = assignments[i];
        	    if (variable(assigned>>1).is_marked()) {  
        	        //this variable is involved in the conflict clause or it's antecedent
        	        variable(assigned>>1).clear_marked();
        	        --_num_marked; 
        	        ClauseIdx ante_cl = variables()[assigned>>1].get_antecedent();
        	        if ( _num_marked == 0 ) { 
        		    //the first UIP encountered, conclude add clause
        		    assert (variable(assigned>>1).new_cl_phase() == UNKNOWN);
        		    _conflict_lits.push_back(assigned^0x1);  // add this assignment's reverse, e.g. UIP
        		    ++ _num_in_new_cl;
        		    variable(assigned>>1).set_new_cl_phase((assigned^0x1)&0x1);
        		    break; //if do this, only one clause will be added.
        	        }
        	        else {
        		    assert ( ante_cl != NULL_CLAUSE );
        		    gflag |= clause(ante_cl).gflag();
        		    mark_vars_at_current_dlevel(ante_cl, assigned>>1/*var*/);
                        clause(ante_cl).activity()++;
        	        }
                }
            }
            if(min_conf_length==-1||_conflict_lits.size()<min_conf_length){
                min_conf_length=_conflict_lits.size();
                min_conf_id=cl;
            }
            //cout<<"current is "_conflict_lits.size()<<" Min is "<<_min_conf_clause.size()<<endl;
            
            for(vector<int>::iterator vi=_conflict_lits.begin();vi!=_conflict_lits.end();vi++) {
       	        int s_var = *vi;
    	        CVariable & var = variable(s_var >> 1);
    	        assert (var.new_cl_phase() == (unsigned)(s_var & 0x1));
    	        var.set_new_cl_phase(UNKNOWN);
            }
            _num_in_new_cl=0;
            _conflict_lits.clear();
            _resolvents.clear();
        }
    }
    assert(_num_marked==0);
    cl = min_conf_id;
    clause(cl).activity()+=5;
    DBG0(cout <<"Conflict clause: " << cl << " : " << clause(cl) << endl;);
    _mark_increase_score=true;
    mark_vars_at_current_dlevel (cl, -1 /*var*/);
    gflag = clause(cl).gflag();
    vector <int> & assignments = *_assignment_stack[dlevel()]; //current dl must be the conflict cl.
    for (int i=assignments.size()-1; i >= 0; --i) { //now add conflict lits, and unassign vars
        int assigned = assignments[i];
	if (variable(assigned>>1).is_marked()) {  
	    //this variable is involved in the conflict clause or it's antecedent
	    variable(assigned>>1).clear_marked();
	    --_num_marked; 
	    ClauseIdx ante_cl = variables()[assigned>>1].get_antecedent();
	    if ( _num_marked == 0 ) { 
		//the first UIP encountered, conclude add clause
		assert (variable(assigned>>1).new_cl_phase() == UNKNOWN);
		_conflict_lits.push_back(assigned^0x1);  // add this assignment's reverse, e.g. UIP
		++ _num_in_new_cl;
		variable(assigned>>1).set_new_cl_phase((assigned^0x1)&0x1);
		break; //if do this, only one clause will be added.
	    }
	    else{
		assert ( ante_cl != NULL_CLAUSE );
		gflag |= clause(ante_cl).gflag();
		mark_vars_at_current_dlevel(ante_cl, assigned>>1/*var*/);
                clause(ante_cl).activity()+=5;
            }
        }
    }
    return finish_add_conf_clause(gflag);
}		

void CSolver::print_cls(ostream & os)
{
    for (unsigned i=0; i< clauses().size(); ++i) {
	CClause & cl = clause(i);
	if (cl.status() == DELETED_CL)
	    continue;
	if (cl.status() == ORIGINAL_CL)
	    os <<"0 ";
	else {
	    assert (cl.status() == CONFLICT_CL);
	    os << "A ";
	}
	for (int i=1; i< 33; ++i) 
	    os <<( cl.gid(i) ? 1:0);
	os << "\t";
	for (unsigned j=0; j< cl.num_lits(); ++j)
	    os << (cl.literal(j).var_sign() ? "-":"") << cl.literal(j).var_index() << " ";
	os <<"0" <<  endl;
	    
    }
}


int CSolver::mem_usage(void) 
{
    int mem_dbase = CDatabase::mem_usage();
    int mem_assignment = 0;
    for (int i=0; i< _stats.max_dlevel; ++i)
	mem_assignment += _assignment_stack[i]->capacity() * sizeof(int);
    mem_assignment += sizeof(vector<int>)* _assignment_stack.size();
    return mem_dbase + mem_assignment;
}

void CSolver::clean_up_dbase(void)
{
    assert (dlevel() == 0);
    assert (_stats.is_solver_started == false);

    int mem_before = mem_usage();
    //1. remove all the learned clauses

    for (vector<CClause>::iterator itr1=clauses().begin(); itr1 != clauses().end()-1; ++itr1) {
	CClause & cl = * itr1;
	if(cl.status()!=ORIGINAL_CL)
            mark_clause_deleted(cl);
    }
    //delete_unrelevant_clauses() is specialized using berkmin deletion strategy.

    //2. free up the mem for the vectors if possible
    for (unsigned i=0; i< variables().size(); ++i) {
	for (int j=0; j< 2; ++j ) { //both phase
	    vector<CLitPoolElement *> watched;
	    vector<CLitPoolElement *> & old_watched = variable(i).watched(j);
	    watched.reserve(old_watched.size());
	    for (vector<CLitPoolElement *>::iterator itr = old_watched.begin(); 
		 itr != old_watched.end(); ++itr)
		watched.push_back(*itr);
	    //because watched is a temp mem allocation, it will get deleted
	    //out of the scope, but by swap it with the old_watched, the contents are reserved.
	    old_watched.swap(watched); 
#ifdef KEEP_LIT_CLAUSES
	    vector<int> lits_cls;
	    vector<int> & old_lits_cls = variable(i).lit_clause(j);
	    lits_cls.reserve(old_lits_cls.size());
	    for (vector<int>::iterator itr = old_lits_cls.begin(); itr != old_lits_cls.end(); ++itr)
		lits_cls.push_back(*itr);
	    old_lits_cls.swap(lits_cls); 
#endif
	}
    } 
    int mem_after = mem_usage();
    if (_params.verbosity > 0) 
	cout << "Database Cleaned, releasing (approximately) " 
	     << mem_before - mem_after << " Bytes" << endl;
}

void CSolver::update_var_score(void) {
    unsigned int i,sz;
    for (i=1, sz=variables().size(); i<sz; ++i) {
	_ordered_vars[i-1].first = & variable(i);
	_ordered_vars[i-1].second = variable(i).score();
    }
    DBG2(
	cout << "Before Update ";
	for (int i=0; i< _ordered_vars.size(); ++i)
	cout << (_ordered_vars[i].first - & variables()[0]) << "(" << _ordered_vars[i].first->score() << ") ";
	cout << endl;
	);
    ::stable_sort(_ordered_vars.begin(), _ordered_vars.end(), cmp_var_stat);
    DBG2(
	cout << "After Update";
	for (int i=0; i< _ordered_vars.size(); ++i)
	cout << (_ordered_vars[i].first - & variables()[0]) << "(" << _ordered_vars[i].first->score() << ") ";
	cout << endl;
	);
    for (i=0, sz= _ordered_vars.size(); i<sz; ++i) 
	_ordered_vars[i].first->set_var_score_pos(i);
    _max_score_pos = 0;
}
	
void CSolver::restart (void){

    _stats.num_restarts += 1;
    if (_params.verbosity > 1 ) 
	cout << "Restarting ... " << endl;

//	To exploit the distribution, 
//	RESTART WITH A NEW INDEPENDENT SEED.. umm how do i do that?
//	
//	here are some choices -> choice of decision variables randomly from a set
	

    if(dlevel()>0)
	back_track(1);

    _stats.restarts_since_vsids +=1;

    assert(dlevel()==0);
/*
    if (dlevel() > 1) {
	if(rand()%2){
		cout << "Backtrack to dlevel 1" <<" from " << dlevel()<< endl;
		back_track(1); //backtrack to level 0. restart.	
	}
	else{
		cout << "Backtrack to  dlevel "<<dlevel()/2 <<" from " << dlevel()<< endl;
		back_track(dlevel()/2);	
	}
    }
*/
    
}

void CSolver::set_up_resolve(ClauseIdx conf_cl, set<CVariable *, cmp_var_assgn_pos> & conf_lits)
{
    assert (_conflict_lits.empty());
    assert (conf_lits.empty());
    CClause & cl = clause(conf_cl);
    for (CLitPoolElement * lit = cl.first_lit(); lit->is_literal(); ++lit) 
	conf_lits.insert(& variable(lit->var_index()));
}

unsigned CSolver::resolve_one_lit(set<CVariable *, cmp_var_assgn_pos> & conf_lits)
{
    assert (!conf_lits.empty());
    CVariable * vptr = (* conf_lits.begin());
    unsigned vid = vptr - &variable(0);
    conf_lits.erase(conf_lits.begin());
    int cl_idx = vptr->antecedent();
    assert (cl_idx != NULL_CLAUSE);
    CClause & cl = clause(cl_idx);
    for (CLitPoolElement * lit = cl.first_lit(); lit->is_literal(); ++lit) {
	if (lit->var_index() != vid) {
	    conf_lits.insert(&variable(lit->var_index()));
	}
    }
    return cl.gflag();
}

bool CSolver::is_uip_reached(set<CVariable *, cmp_var_assgn_pos> & conf_lits)
{
    assert (!conf_lits.empty());
    if (conf_lits.size() == 1) return true;
    set<CVariable *, cmp_var_assgn_pos>::iterator itr = conf_lits.begin();
    CVariable * v1 = *itr;
    ++itr;
    CVariable * v2 = *itr;
    assert (v1->dlevel() >= v2->dlevel());
    if (v1->dlevel() != v2->dlevel())
	return true;
    return false;
}

int CSolver::conflict_analysis_firstUIP_resolve_based(void)
{
    assert (dlevel() > 0);
    ClauseIdx cl = _conflicts[0];
    unsigned gflag = clause(cl).gflag();
    set<CVariable *, cmp_var_assgn_pos> conf_lits;
    set_up_resolve(cl, conf_lits);
    while(!is_uip_reached(conf_lits))
	gflag |= resolve_one_lit(conf_lits);
    vector<int> cls_lits;
    for (set<CVariable *, cmp_var_assgn_pos>::iterator itr = conf_lits.begin();
	 itr != conf_lits.end(); ++itr) {
	int vid = (*itr) - &variable(0);
	int sign = variable(vid).value();
	cls_lits.push_back(vid + vid + sign);
    }
    ClauseIdx added_cl = add_conflict_clause(&(*cls_lits.begin()), cls_lits.size(), gflag);
    if (added_cl < 0 ) { //memory out.
	_stats.is_mem_out = true;
	_conflicts.clear();
	assert (_implication_queue.empty());
	return 1; 
    }
    adjust_variable_order (&(*cls_lits.begin()), cls_lits.size());
    int back_dl = 0;
    int unit_lit = cls_lits[0];
    if (cls_lits.size() > 1) {
	back_dl = variable(cls_lits[1]>>1).dlevel();
    }
    DBG0( cout << "**Add Clause " <<added_cl<< " : "<<clause(added_cl) << endl; );
    back_track(back_dl + 1);
    queue_implication(unit_lit, added_cl, back_dl);
	    
    for (unsigned i=1; i< _conflicts.size(); ++i) //after resolve the first conflict, others must also be resolved
	assert(!is_conflicting(_conflicts[i]));
    _conflicts.clear();
    DBG0(cout << "Conflict Analasis: conflict at level: " << back_dl + 1;
	 cout << "  Assertion Clause