zchaff_solver.cpp

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

    
    for (;top_unsat_cls->status()!=ORIGINAL_CL;top_unsat_cls--) {
        CClause &cl=*top_unsat_cls;
        if(cl.status()!=CONFLICT_CL)
	    continue;
        cls_sat=false;
	if(cl.sat_lit_idx()<cl.num_lits()&&literal_value(cl.literal(cl.sat_lit_idx()))==1)
            cls_sat=true;
	if(!cls_sat){	
	    for (i=0,sz=cl.num_lits(); i<sz; ++i){
	        if (literal_value(cl.literal(i)) == 1 ) {
        	    cls_sat=true;
		    cl.sat_lit_idx()=i;
		    break;
	    	}
	    }
	}
	if(!cls_sat){
            for (i=0, sz= cl.num_lits(); i<sz; ++i){
	        var_idx=cl.literal(i).var_index();
	        score=0;
	        if (variable(var_idx).value() == UNKNOWN){
                    score=variable(var_idx).score();
		    if(score>max_score){
		        max_score=score;
		        s_var=2*var_idx;
		    }    
		}
            }
	    break;
	}
    }
    if(max_score!=-1){    
        ++dlevel();
        if (dlevel() > _stats.max_dlevel) 
	    _stats.max_dlevel = dlevel();
	CVariable &v=variable(s_var>>1);		
        if(v.score(0)<v.score(1))
    	    s_var+=1;
        else if(v.score(0)==v.score(1)){
            if(v.two_lits_count(0)>v.two_lits_count(1))
                s_var+=1;
            else if(v.two_lits_count(0)==v.two_lits_count(1))
                s_var+=rand()%2;
        }
	assert(s_var >=2 );					
        queue_implication(s_var, NULL_CLAUSE, dlevel());
	++_stats.num_decisions_stack_conf;
        return true;
    }
    _stats.restarts_since_vsids=0;    
   DBG2(
	cout << "Ordered Vars ";
	for (unsigned i=0; i< _ordered_vars.size(); ++i)
	cout << (_ordered_vars[i].first - & variables()[0]) << " ";
	cout << endl;
	);

    CHECK(
	int free = 0;
	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);
	    if (_ordered_vars[i].first->value() == UNKNOWN) ++free;
	}
	assert (free == num_free_variables());
	);

    for (unsigned i=_max_score_pos; i<_ordered_vars.size(); ++i) {
	CVariable & var = *_ordered_vars[i].first;
	if (var.value()==UNKNOWN && var.is_branchable()) {
	    //move th max score position pointer
	    _max_score_pos = i;
	    //make some randomness happen
	    if (--_stats.current_randomness < _params.decision.base_randomness)
		_stats.current_randomness = _params.decision.base_randomness;

	    int randomness = _stats.current_randomness;
	    if (randomness >= num_free_variables())
		randomness = num_free_variables() - 1;
	    int skip =rand()%(1+randomness);
	    int index = i;
	    while (skip > 0) {
		++index;
		if (_ordered_vars[index].first->value()==UNKNOWN && 
		    _ordered_vars[index].first->is_branchable())
		    --skip;
	    }
	    CVariable * ptr = _ordered_vars[index].first;
	    assert (ptr->value() == UNKNOWN && ptr->is_branchable());
	    int sign=0;
//	    sign = ptr->score(0) > ptr->score(1) ? 0 : 1;
	    if(ptr->score(0) < ptr->score(1))
		sign += 1;
            else if(ptr->score(0) == ptr->score(1)){
                if(ptr->two_lits_count(0)>ptr->two_lits_count(1))
                   sign+=1;
                else if(ptr->two_lits_count(0)==ptr->two_lits_count(1))
                   sign+=rand()%2;
            }
//	    sign = (random() > (RAND_MAX >> 1))? 0: 1;
	    int var_idx = ptr - &(*variables().begin());
	    s_var = var_idx + var_idx + sign;
	    break;
	}
    }

    assert (s_var >= 2); //there must be a free var somewhere
    ++dlevel();
    if (dlevel() > _stats.max_dlevel) 
	_stats.max_dlevel = dlevel();
    ++_stats.num_decisions_vsids;
    DBG0 (cout << "**Decision " << _stats.num_decisions << " at Level " << dlevel() ;
	  cout <<": " << s_var << "\ti.e. " << (s_var&0x1?"-":" ") ;
	  cout <<(s_var>>1)  << endl; );
    _implication_id = 0;
    queue_implication(s_var, NULL_CLAUSE, dlevel());
    return true;
}

int CSolver::preprocess(void) 
{
    unsigned int i, sz;
    assert(dlevel() == 0);
    //1. detect all the unused variables
    vector<int> un_used;
    for (i=1, sz=variables().size(); i<sz; ++i) {
	CVariable & v = variable(i);
	if (v.lits_count(0) == 0 && v.lits_count(1) == 0) {
	    un_used.push_back(i);
	    queue_implication(i+i, NULL_CLAUSE, 0);
	    int r = deduce();
	    assert (r == NO_CONFLICT);
	}
    }
    if (_params.verbosity>1 && un_used.size() > 0) {
	cout << un_used.size()<< " Variables are defined but not used " << endl;
	if (_params.verbosity > 2) {
	    for (unsigned i=0; i< un_used.size(); ++i)
		cout << un_used[i] << " ";
	    cout << endl;
	}
    }

    //2. detect all variables with only one phase occuring (i.e. pure literals)
    vector<int> uni_phased;
    for (i=1, sz=variables().size(); i<sz; ++i) {
	CVariable & v = variable(i);
	if (v.value() != UNKNOWN)
	    continue;
	if (v.lits_count(0) == 0){ //no positive phased lits.
	    queue_implication( i+i+1, NULL_CLAUSE, 0);
	    uni_phased.push_back(-i);
	}
	else if (v.lits_count(1) == 0){ //no negative phased lits.
	    queue_implication( i+i, NULL_CLAUSE, 0);
	    uni_phased.push_back(i);
	}
    }
    if (_params.verbosity>1 && uni_phased.size() > 0) {
	cout << uni_phased.size()<< " Variables only appear in one phase." << endl;
	if (_params.verbosity > 2) {
	    for (i=0; i< uni_phased.size(); ++i)
		cout << uni_phased[i] << " ";
	    cout <<endl;
	}
    }
    //3. Unit clauses
    for (i=0, sz=clauses().size(); i<sz; ++i) {
	if (clause(i).status()!=DELETED_CL)
	    if (clause(i).num_lits() == 1){ //unit clause
		if (variable(clause(i).literal(0).var_index()).value() == UNKNOWN)
		    queue_implication(clause(i).literal(0).s_var(), i, 0);
	    }
    }
    if(deduce()==CONFLICT) {
    	cout << " CONFLICT during preprocess " <<endl;
#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();
		    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;
		}
	    }
	}
	verify_out << "CONF: " << clause(_conflicts[0]).id() << " ==";
	for (unsigned i=0; i< clause(_conflicts[0]).num_lits(); ++i) {
	    int svar = clause(_conflicts[0]).literal(i).s_var();
	    verify_out << " " << svar;
	}
#endif
	return CONFLICT;
    }
    
    cout<<_assignment_stack[0]->size()<<" vars set during preprocess; "<<endl;
    return NO_CONFLICT;    
}

void CSolver::mark_var_unbranchable(int vid)
{
    
    if (variable(vid).is_branchable()==true) {
	variable(vid).disable_branch();
	if (variable(vid).value()==UNKNOWN)
	    --num_free_variables();
    }
}

void CSolver::mark_var_branchable(int vid)
{
    CVariable & var = variable(vid);
    if (var.is_branchable()==false) {
	var.enable_branch();
	if (var.value() == UNKNOWN) {
	    ++ num_free_variables();
	    if (var.var_score_pos() < _max_score_pos)
		_max_score_pos = var.var_score_pos();
	}
    }
}

ClauseIdx CSolver::add_orig_clause (int * lits, int n_lits, int gid)
{
    int cid = add_clause_with_gid(lits, n_lits, gid);
    if (cid >= 0){
	clause(cid).set_status(ORIGINAL_CL);
	clause(cid).activity()=0; // just to initialize
    }	
    return cid;
}

ClauseIdx CSolver::add_clause_with_gid (int * lits, int n_lits, int gid)
{
    assert (dlevel() >= 0);
    unsigned gflag;
    if (gid == PERMANENT_GID ) 
	gflag = 0;
    else if (gid == VOLATILE_GID)
	gflag = (~0x0);
    else {
	assert (gid <= WORD_WIDTH && gid > 0);
	gflag = (1 << (gid- 1));
    }
    ClauseIdx cid = add_clause( lits, n_lits, gflag);
    if (cid < 0) {
	_stats.is_mem_out = true;
	_stats.outcome = MEM_OUT;
	return cid;
    }
    return cid;
}

ClauseIdx CSolver::add_conflict_clause (int * lits, int n_lits, int gflag)
{
    ClauseIdx cid = add_clause(lits, n_lits, gflag);
    if (cid >= 0) {
	clause(cid).set_status(CONFLICT_CL);
	clause(cid).activity()=0;
    }
    else {
	_stats.is_mem_out = true;
	_stats.outcome = MEM_OUT;
    }
    return cid;
}

void CSolver::real_solve(void)
{
    while(_stats.outcome == UNDETERMINED) {
	run_periodic_functions();
	if (decide_next_branch()) {
	    while (deduce()==CONFLICT) { 
	        int blevel;
		blevel = analyze_conflicts();
		if (blevel < 0) {
		    _stats.outcome = UNSATISFIABLE;
		    return;
		}
	    }
	}
	else {
            if(_sat_hook != NULL && _sat_hook(this))
                continue;
	    _stats.outcome = SATISFIABLE;
	    return;
	}
	if (time_out()) { 
	    _stats.outcome = TIME_OUT;
	    return; 
	}
	if (_force_terminate) { 
	    _stats.outcome = ABORTED;
	    return; 
	}
	if (_stats.is_mem_out) {
	    _stats.outcome = MEM_OUT;
	    return; 
	}	    
    }
}

int CSolver::solve(void)
{
//    DBG1(dump());
    if (_stats.outcome == UNDETERMINED) {
	init_solve();
	//preprocess 
	DBG1(dump_assignment_stack(););
	if(preprocess()==CONFLICT) 
	    _stats.outcome = UNSATISFIABLE;
	else //the real search
	    real_solve();
        cout<<endl;
	_stats.finish_cpu_time = get_cpu_time();
    }
    int result = _stats.outcome;
//    _stats.outcome = UNDETERMINED;
    return result;
}

void CSolver::back_track(int blevel)
{
    DBG1(cout << "Back track to " << blevel <<" ,currently in "<< dlevel() << " level" << endl;);
    DBG2 (dump());
    CHECK(verify_integrity());
    assert(blevel <= dlevel());
    for (int i=dlevel(); i>= blevel; --i) {
	vector<int> & assignments = *_assignment_stack[i];
	for (int j=assignments.size()-1 ; j>=0; --j) 
	    unset_var_value(assignments[j]>>1);
	assignments.clear();
    }
    dlevel() = blevel - 1;
    if (dlevel() < 0 ) 
	dlevel() = 0;
    ++_stats.num_backtracks;
    DBG2 (dump());
    CHECK(verify_integrity());
}

int CSolver::deduce(void) 
{
    while (!_implication_queue.empty() && _conflicts.size()==0) {
	DBG2(dump_implication_queue(););
	const CImplication & imp = _implication_queue.front();
	int lit = imp.lit;
	int vid = lit>>1;
	int dl = imp.dlevel;
	ClauseIdx cl = imp.antecedent;
	_implication_queue.pop();
	CVariable & var = variable(vid);
	if ( var.value() == UNKNOWN) { // an implication
	    set_var_value(vid, !(lit&0x1), cl, dl);
	    //var.assgn_stack_pos() = _assignment_stack[dl]->size();
	    //_assignment_stack[dl]->push_back(lit);
	    CHECK(verify_integrity());
	}
	else if (var.value() == (unsigned)(lit&0x1) ) { //a conflict
	    //note: literal & 0x1 == 1 means the literal is in negative phase
	    //when a conflict occure at not current dlevel, we need to backtrack
	    //to resolve the problem.
	    //conflict analysis will only work if the conflict occure at 
	    //the top level (current dlevel)
	    if (dl == dlevel()) {
		_conflicts.push_back(cl);
		continue;
	    }
	    else {
		assert (dl < dlevel());
		int orig_dl = var.dlevel();
		vector<CImplication> still_valid;
		if (orig_dl < dl) //this means other implication will take care of it.
		    continue;
		if (orig_dl > dl) {
		    //in this case, backtrack to orig_dl level, and do the implication need to be done
		    while (!_implication_queue.empty()) {
			if (_implication_queue.front().dlevel < orig_dl ) 
			    still_valid.push_back(_implication_queue.front());
			_implication_queue.pop();
		    }
		    for (unsigned i=0; i< still_valid.size(); ++i) 
			_implication_queue.push(still_valid[i]);
		    back_track(orig_dl);
		    set_var_value(vid, !(lit&0x1), cl, dl);
		    //var.assgn_stack_pos() = _assignment_stack[dl]->size();
		    //_assignment_stack[dl]->push_back(lit);
		}
		else { 
		    assert (orig_dl == dl);
		    //in this case, backtrack to that dlevel and it's a conflict clause