zchaff_solver.cpp

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

		    back_track(orig_dl + 1);
		    _conflicts.push_back(cl);
		}
	    }
	}
	else {
	    //so the variable have been assigned before
	    if(var.antecedent()!=NULL_CLAUSE&&clause(cl).num_lits() < clause(var.antecedent()).num_lits()) 
	    	var.antecedent()=cl;
	    if (var.dlevel() <= dl) continue;
	    int old_dl = var.dlevel();
	    int old_pos = var.assgn_stack_pos();
	    assert ((*_assignment_stack[old_dl])[old_pos] == lit);
	    (*_assignment_stack[old_dl])[old_pos] = 0; //insert a bubble
	    unset_var_value(vid);
	    set_var_value(vid, !(lit& 0x1), cl, dl);
	    //var.assgn_stack_pos() = _assignment_stack[dl]->size();
	    //_assignment_stack[dl]->push_back(lit);
	}
    }
    //if loop exited because of a conflict, we need to clean implication queue
    while(!_implication_queue.empty()) 
	_implication_queue.pop();
    return (_conflicts.size()?CONFLICT:NO_CONFLICT);
}


void CSolver::verify_integrity(void) 
{	
    for (unsigned i=1; i< variables().size(); ++ i) {
	if (variable(i).value() != UNKNOWN) {
	    int pos = variable(i).assgn_stack_pos();
	    int value = variable(i).value();
	    int dlevel = variable(i).dlevel();
	    assert ((*_assignment_stack[dlevel])[pos] == (int) (i+i+1-value));
	}
    }
    for (unsigned i=0; i< clauses().size(); ++i) {
	if (clause(i).status() == DELETED_CL)
	    continue;
	CClause & cl = clause(i);
	int num_0 = 0;
	int num_1 = 0;
	int num_unknown = 0;
	int watched[2]; 
	int watch_index = 0;
	watched[1] = watched[0] = 0;
	for (unsigned j=0; j< cl.num_lits(); ++j) {
	    CLitPoolElement lit = cl.literal(j);
	    int vid = lit.var_index();
	    if (variable(vid).value() == UNKNOWN)
		++ num_unknown;
	    else {
		if (literal_value(lit) == 0)
		    ++ num_0;
		else 
		    ++ num_1;
	    }
	    if (lit.is_watched()) {
		watched[watch_index] = lit.s_var();
		++watch_index;
	    }
	}
	if (watch_index==0) {
	    assert ( cl.num_lits() == 1);
	    continue;
	}
	assert (watch_index == 2);
	for (unsigned j=0; j< cl.num_lits(); ++j) {
	    CLitPoolElement lit = cl.literal(j);
	    int vid1 = (watched[0]>>1);
	    if (variable(vid1).value() == (unsigned)(watched[0] & 0x1)) {
		if (!lit.is_watched()) {
		    assert (literal_value(lit) == 0);
		    assert (variable(lit.var_index()).dlevel() <= variable(vid1).dlevel());
		}
	    }
	    int vid2 = (watched[1]>>1);
	    if (variable(vid2).value() == (unsigned)(watched[1] & 0x1)) {
		if (!lit.is_watched()) {
		    assert (literal_value(lit) == 0);
		    assert (variable(lit.var_index()).dlevel() <= variable(vid1).dlevel());
		}
	    }
	}
    }
}

void CSolver::mark_vars_of_dl(vector<int> & lits, int dl)
//given a vector of lits (all are "in_new_clause", which is generated by
//last round of mark_vars_at_level, mark_vars_of_dl will mark those which dlevel = dl,
//and put the rest into _conflict_lits
{
    assert (_num_marked == 0);
    DBG1(
	cout << "The Lits involved are : " << endl;
	for (unsigned i=0; i< lits.size(); ++i) {
	    cout << "V: " << (lits[i] & 0x1 ? "-":"+") << (lits[i] >> 1) << ": " 
		 << variable(lits[i]>>1);
	}
	cout << endl << endl;
	);
    
    for (vector<int>::iterator itr = lits.begin(); itr != lits.end(); ++ itr) {
	int v = (*itr)>>1;
	assert (variable(v).new_cl_phase() != UNKNOWN);
	if (variable(v).dlevel() == dl) {
	    -- _num_in_new_cl;
	    variable(v).set_new_cl_phase(UNKNOWN);
	    assert (!variable(v).is_marked());
	    variable(v).set_marked();
	    ++ _num_marked;
	}
	else {
	    assert (variable(v).dlevel() < dl);
	    _conflict_lits.push_back((*itr));
	}
    }
}

void CSolver::mark_vars_at_level(ClauseIdx cl, int var_idx, int dl)
{
    assert (_resolvents.empty() || var_idx != -1);
#ifdef VERIFY_ON	
    _resolvents.push_back(clause(cl).id());
#endif
    for (CLitPoolElement * itr = clause(cl).literals(); (*itr).val() > 0 ; ++ itr) {
	int v = (*itr).var_index();
	if (v == var_idx) 
	    continue;
	else if (variable(v).dlevel() == dl) {
	    if (!variable(v).is_marked()) {
		variable(v).set_marked();
		++ _num_marked;
                if(_mark_increase_score){
                    int tmp=itr->s_var();
                    adjust_variable_order(&tmp,1);
                }
	    }
	}
	else {
	    assert (variable(v).dlevel() < dl);
	    if (variable(v).new_cl_phase() == UNKNOWN){ //it's not in the new cl
                if(variable(v).dlevel()){
		    ++ _num_in_new_cl;
		    variable(v).set_new_cl_phase((*itr).var_sign());
		    _conflict_lits.push_back((*itr).s_var());
                }
	    }
	    else //if this variable is already in the new clause, it must have the same phase 
		assert(variable(v).new_cl_phase() == (*itr).var_sign());
	}
    }
}

int CSolver::analyze_conflicts(void) {
    assert (_conflicts.size() > 0);
    assert(_conflict_lits.size() == 0); 
    assert (_implication_queue.empty());
    assert (_num_marked == 0);
    DBG1(dump_assignment_stack());
    CHECK(verify_integrity());

    if (dlevel() == 0){ //already at level 0. Conflict means unsat.
#ifdef VERIFY_ON
	for (unsigned i=1; i< variables().size(); ++i) {
	    if (variable(i).value() != UNKNOWN) {
		assert (variable(i).dlevel() <= 0); 
		int ante = variable(i).antecedent();
		int ante_id = 0;
		if (ante >= 0) {
		    ante_id = clause(ante).id();
		    assert(clause(ante).status()!=DELETED_CL);
		    verify_out << "VAR: " << i 
			       << " L: " << variable(i).assgn_stack_pos()
			       << " V: " << variable(i).value() 
			       << " A: " << ante_id 
			       << " Lits:";
		    for (unsigned j=0; j< clause(ante).num_lits(); ++j)
			verify_out << " " << clause(ante).literal(j).s_var();
		    verify_out << endl;
		}
	    }
	}
	ClauseIdx shortest;
	shortest=_conflicts.back();
	int len=(int) clause(_conflicts.back()).num_lits();
	while(!_conflicts.empty()){	
		if((int) clause(_conflicts.back()).num_lits() < len ){
			shortest=_conflicts.back();
			len=clause(_conflicts.back()).num_lits();
		}	
		_conflicts.pop_back();
	}
	verify_out << "CONF: " << clause(shortest).id() << " ==";
	for (unsigned i=0; i< clause(shortest).num_lits(); ++i) {
	    int svar = clause(shortest).literal(i).s_var();
	    verify_out << " " << svar;
	}
	verify_out<<endl;
#endif	
	_conflicts.clear();
	back_track(0);
	return -1;
    }
    
    int result;
//    int result = conflict_analysis_firstUIP_resolve_based()
    result = conflict_analysis_firstUIP();
//    int result = conflict_analysis_allUIP();
//    int result = conflict_analysis_decisions_only();
    DBG1( dump_assignment_stack(););
    return result;
}


//when all the literals involved are in _conflict_lits
//call this function to finish the adding clause and backtrack

int CSolver::finish_add_conf_clause(int gflag)
    
{
    unsigned int i,sz;
    int back_dl = 0;
    int unit_lit = -1;
    ClauseIdx added_cl = add_conflict_clause(&(*_conflict_lits.begin()), _conflict_lits.size(), gflag);
    if (added_cl < 0 ) { //memory out.
	_stats.is_mem_out = true;
	_conflicts.clear();
	assert (_implication_queue.empty());
	return 1; 
    }
    int new_cls_len=clause(added_cl).num_lits();
    _stats.sum_sizes_iter += new_cls_len;
    _stats.sum_squares_iter += new_cls_len*new_cls_len;
    _stats.num_conf_cls_iter += 1;
    
    top_unsat_cls=clauses().end();
    top_unsat_cls--;
#ifdef VERIFY_ON
    verify_out << "CL: " <<  clause(added_cl).id() << " <=";
    for (unsigned i=0; i< _resolvents.size(); ++i)
	verify_out << " " <<  _resolvents[i];
    verify_out << endl;
    _resolvents.clear();
#endif

    adjust_variable_order (&(*_conflict_lits.begin()), _conflict_lits.size());
    
    DBG0( cout << "**Add Clause " <<added_cl<< " : "<<clause(added_cl) << endl; );
    if(_params.shrinking.enable){
        if(_shrinking_cls.size())
            _shrinking_cls.clear();
        if(_shrinking_conf_cls_length){
            int benefit=_shrinking_conf_cls_length-_conflict_lits.size();
            _shrinking_benefit+=benefit;
            _shrinking_conf_cls_length=0;
            _recent_shrinkings.push(benefit);
            if(_recent_shrinkings.size()>20){
                _shrinking_benefit-=_recent_shrinkings.front();
                _recent_shrinkings.pop();
            }
        }
        if(_conflict_lits.size()>_params.shrinking.size){
            _shrinking_cls.clear();
            for(i=0,sz=_conflict_lits.size();i<sz;i++)
                _shrinking_cls.insert(pair<int,int>(variable(_conflict_lits[i]>>1).dlevel(),_conflict_lits[i]));
            int prev_dl=_shrinking_cls.begin()->first;
            multimap<int,int>::iterator mmi,next;
            mmi=_shrinking_cls.end();
            mmi--;
            int last_dl=mmi->first;
            bool found_break=false;
            for(mmi=_shrinking_cls.begin();mmi!=_shrinking_cls.end()&&mmi->first!=last_dl;){
                if(mmi->first-prev_dl>2){
                    found_break=true;
                    break;
                }
                prev_dl=mmi->first;
                next=mmi;
                next++;
                _shrinking_cls.erase(mmi);
                mmi=next;
            }
            if(found_break&&_shrinking_cls.size()>0&&prev_dl<dlevel()-1){
                _shrinking_conf_cls_length=_conflict_lits.size();
                _stats.num_shrinkings++;
                back_dl=prev_dl;
                back_track(back_dl+1);
                _conflicts.clear();
                _resolvents.clear();
                _num_in_new_cl=0;
                for(i=0,sz=_conflict_lits.size();i<sz;i++)
    	            variable(_conflict_lits[i]>>1).set_new_cl_phase(UNKNOWN);
                _conflict_lits.clear();
                if(_stats.num_shrinkings%20==0&&_recent_shrinkings.size()==20){
                    if(_shrinking_benefit>800)
                       _params.shrinking.size-=5;
                    else if(_shrinking_benefit<600)
                       _params.shrinking.size+=10;
                }
                
                return back_dl;
            }
        }
    }
    for (i=0; i< clause(added_cl).num_lits(); ++i) {
	int vid = clause(added_cl).literal(i).var_index();
	int sign =clause(added_cl).literal(i).var_sign();
	assert (variable(vid).value() != UNKNOWN);
	assert (literal_value(clause(added_cl).literal(i)) == 0);
	int dl = variable(vid).dlevel();
	if ( dl < dlevel()) {
	    if (dl > back_dl) 
		back_dl = dl;
	}
	else {
	    assert (unit_lit == -1);
	    unit_lit = vid + vid + sign; 
	}
    }
    if(back_dl==0) {
    	_stats.next_restart = _stats.num_backtracks + _stats.restart_incr;
    	_stats.next_cls_deletion =_stats.num_backtracks + _params.cls_deletion.interval;
    }

    back_track(back_dl + 1);
    queue_implication(unit_lit, added_cl, back_dl);
	    
    for (i=1; i< _conflicts.size(); ++i) //after resolve the first conflict, others must also be resolved
	assert(!is_conflicting(_conflicts[i]));
    _conflicts.clear();

    while (_conflict_lits.size()) {
	int svar = _conflict_lits.back();
	_conflict_lits.pop_back();
	CVariable & var = variable(svar >> 1);
	assert (var.new_cl_phase() == (unsigned)(svar & 0x1));
	-- _num_in_new_cl;
	var.set_new_cl_phase(UNKNOWN);
    }
    assert (_num_in_new_cl == 0);
    DBG0(cout << "Conflict Analasis: conflict at level: " << back_dl + 1;
	 cout << "  Assertion Clause is " << added_cl<< endl; );

    return back_dl;
}

int CSolver::conflict_analysis_grasp (void)
{
    fatal(_POSITION_, "Not implemented in this version");
    return 0;
}

int CSolver::conflict_analysis_decisions_only (void)
{
    //For experiment purpose only, don't use it 
    unsigned int i;
    ClauseIdx cl = _conflicts[0];
    int gflag = clause(cl).gflag();
    vector<int> involved_lits;
    for (i=0; i < clause(cl).num_lits(); ++i) {
	int svar = clause(cl).literal(i).s_var();
	++ _num_marked;
	variable(svar>>1).set_marked();
	involved_lits.push_back(svar);
    }
    for (i=0; i<involved_lits.size(); ++i) {
	int vid = involved_lits[i] >> 1;
	if (variable(vid).get_antecedent() != NULL_CLAUSE) {
	    //it's not a decision variable
	    CClause & c = clause(variable(vid).get_antecedent());
	    gflag |= c.gflag();
	    for (unsigned j=0; j< c.num_lits(); ++j) {
		int lit = c.literal(j).s_var();
		if (variable(lit>>1).is_marked()==false) {
		    ++ _num_marked;
		    variable(lit>>1).set_marked();
		    involved_lits.push_back(lit);
		}
	    }
	}
    }
    for (vector<int>::iterator itr = involved_lits.begin(); 
	 itr != involved_lits.end(); ++itr) {
	int svar = *itr;
	if (variable(svar>>1).get_antecedent() == NULL_CLAUSE) {
	    ++ _num_in_new_cl;
	    variable(svar>>1).set_new_cl_phase(svar & 0x1);
	    _conflict_lits.push_back(svar);
	}
	assert (variable(svar>>1).is_marked());
	-- _num_marked;
	variable(svar>>1).clear_marked();
    }
    assert (_num_marked == 0);
		    		
    return finish_add_conf_clause(gflag);
}

int CSolver::conflict_analysis_allUIP (void)
{
    //For experiment purpose only, don't use it