asap_solver.cpp

命题逻辑的求解器,2004年SAT竞赛第一名的求解器

    }
    //now delete the index from variables
    if (original_num_deleted == num_deleted_clauses()) 
	return ; //didn't delete anything
    for (vector<CVariable>::iterator itr = variables().begin(); 
	 itr != variables().end(); ++ itr) {
	for (int i=0; i<2; ++i) { //for each phase
	    //delete the h_t index from the vars
	    vector<CLitPoolElement *> & ht_ptr = (*itr).ht_ptr(i);
	    for (vector<CLitPoolElement *>::iterator my_itr = ht_ptr.begin(); 
		 my_itr != ht_ptr.end(); ++my_itr) {
		if ( (*my_itr)->val() <= 0) {
		    *my_itr = ht_ptr.back();
		    ht_ptr.pop_back();
		    --my_itr;
		}
	    }
	}
    }
    CHECK(cout << "Deleting " << num_deleted_clauses() - original_num_deleted << " Clause ";
      cout << " and " << num_deleted_literals() - original_del_lits << " Literals " << endl;);
    CHECK_FULL (dump());
}
//============================================================================================
bool CSolver::time_out(void) 
{
    if ( (current_cpu_time() - _stats.start_cpu_time)/1000.0 > _params.time_limit )
	return true;
    return false;
}

inline bool compare_var_stat(const pair<CVariable *,int> & v1, 
			    const pair<CVariable *,int> & v2) 
{	
    if (v1.second > v2.second) return true;
    return false;
}

void CSolver::update_var_stats(void) 
{
    for(int i=1; i< variables().size(); ++i) {
	CVariable & var = variable(i);
	var.score(0) = var.score(0)/2 + var.lits_count(0) - _last_var_lits_count[0][i];
	var.score(1) = var.score(1)/2 + var.lits_count(1) - _last_var_lits_count[1][i];
	_last_var_lits_count[0][i] = var.lits_count(0);
	_last_var_lits_count[1][i] = var.lits_count(1);
	_var_order[i-1] = pair<CVariable * , int>( &var, var.score());
    }
    ::stable_sort(_var_order.begin(), _var_order.end(), compare_var_stat);
    for (int i=0; i<_var_order.size(); ++i) 
	_var_order[i].first->var_score_pos() = i;
    _max_score_pos = 0;
}

bool CSolver::decide_next_branch(void)
{
    ++_stats.num_decisions;
    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.
	_max_score_pos = 0; //reset the max_score_position.
	return _implication_queue.front().first;
    }
	
    int s_var = 0;

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

	    int randomness = _params.randomness;
  	    if (randomness >= num_free_variables())
  		randomness = num_free_variables() - 1;
	    int skip =random()%(1+randomness);
	    int index = i;
	    while (skip > 0) {
		++index;
		if (_var_order[index].first->value()==UNKNOWN)
		    --skip;
	    }
	    CVariable * ptr = _var_order[index].first;
	    assert (ptr->value() == UNKNOWN);
	    int sign = ptr->score(0) > ptr->score(1) ? 0 : 1;
	    int var_idx = ptr - variables().begin();
	    s_var = var_idx + var_idx + sign;
	    break;
	}
    }

    if (s_var<2) //no more free vars, solution found,  quit
	return false;
    ++dlevel();
    if (dlevel() > _stats.max_dlevel) _stats.max_dlevel = dlevel();
    CHECK (cout << "**Decision at Level " << dlevel() ;
	   cout <<": " << s_var << "\te.g. " << (s_var&0x1?"-":" ") ;
	   cout <<(s_var>>1)  << endl; );
    queue_implication(s_var, NULL_CLAUSE);
    return true;
}

int CSolver::preprocess(void) 
{
    //1. detect all the unused variables
    vector<int> un_used;
    for (int 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);
	    v.value() = 1; 
	    v.dlevel() = -1;
	}
    }
    num_free_variables() -= un_used.size();
    if (_params.verbosity>1 && un_used.size() > 0) {
	cout << un_used.size()<< " Variables are defined but not used " << endl;
	if (_params.verbosity > 2) {
	    for (int i=0; i< un_used.size(); ++i)
		cout << un_used[i] << " ";
	    cout << endl;
	}
    }
    //2. detect all variables with only one phase occuring
    vector<int> uni_phased;
    for (int 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);
	    uni_phased.push_back(-i);
	}
	else if (v.lits_count(1) == 0){ //no negative phased lits.
	    queue_implication( i+i, NULL_CLAUSE);
	    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 (int i=0; i< uni_phased.size(); ++i)
		cout << uni_phased[i] << " ";
	    cout <<endl;
	}
    }
    //3. detect all the unit clauses
    for (ClauseIdx i=0, sz=clauses().size(); i<sz; ++i) {
	if (clause(i).num_lits() == 1){ //unit clause
	    queue_implication(find_unit_literal(i), i);
	}
    }

    if(deduce()==CONFLICT) return CONFLICT;
    return NO_CONFLICT;    
}

void CSolver::real_solve(void)
{
    while(1) {
	run_periodic_functions();
	if (decide_next_branch()) {
	    while (deduce()==CONFLICT) { 
		int blevel = analyze_conflicts();
		if (blevel <= 0) {
		    _stats.outcome = UNSATISFIABLE;
		    return;
		}
	    }
	}
	else {
	    _stats.outcome = SATISFIABLE;
	    return;
	}
	if (time_out()) { 
	    _stats.outcome = TIME_OUT;
	    return; 
	}
	if (_stats.is_mem_out) {
	    _stats.outcome = MEM_OUT;
	    return; 
	}	    
    }
}

int CSolver::solve(void)
{
    init();
    //preprocess 
    if(preprocess()==CONFLICT) {
	_stats.outcome = UNSATISFIABLE;
    }
    else //the real search
	real_solve();
    _stats.finish_cpu_time = current_cpu_time();
    _stats.finish_world_time = current_world_time();
    return _stats.outcome;
}

void CSolver::back_track(int blevel)
{
    CHECK (cout << "Back track to " << blevel <<" ,currently in "<< dlevel() << " level" << endl;);
    CHECK_FULL (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);
	num_free_variables() += assignments.size();
	assignments.clear();
    }
    dlevel() = blevel - 1;
    ++_stats.num_backtracks;
    CHECK_FULL (dump());
    CHECK(verify_integrity());
}

int CSolver::deduce(void) 
{
    while (!_implication_queue.empty() && _conflicts.size()==0) {
	int literal = _implication_queue.front().first;
	int variable_index = literal>>1;
	ClauseIdx cl = _implication_queue.front().second;
	_implication_queue.pop();
	CVariable & the_var = variables()[variable_index];
	if ( the_var.value() == UNKNOWN) { // an implication
	    int dl;
	    if (_params.back_track_complete)
		dl = dlevel();
	    else 
		dl = find_max_clause_dlevel(cl);
	    set_var_value(variable_index, !(literal&0x1), cl, dl);
	    _assignment_stack[dl]->push_back(literal);
	    CHECK(verify_integrity());
	}
	else if (the_var.value() == (literal&0x1) ) { //a conflict
	    //note: literal & 0x1 == 1 means the literal is in negative phase
	    _conflicts.push_back(cl);
	}
    }
    while(!_implication_queue.empty()) _implication_queue.pop();
    return (_conflicts.size()?CONFLICT:NO_CONFLICT);
}


void CSolver::verify_integrity(void) 
{
}

void CSolver::mark_vars_at_level(ClauseIdx cl, int var_idx, int dl)
{
    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;
	    }
	}
	else {
	    int dl1 = variable(v).dlevel();
	    assert (variable(v).dlevel() < dl);
	    if (variable(v).in_new_cl() == -1){ //it's not in the new cl
		variable(v).set_in_new_cl((*itr).var_sign());
		_conflict_lits.push_back((*itr).s_var());
	    }
	}
    }
}

int CSolver::analyze_conflicts(void) {
    return conflict_analysis_zchaff();
}

int CSolver::conflict_analysis_zchaff (void) 
{
    assert (_conflicts.size());
    assert (_implication_queue.empty());
    assert (_num_marked == 0);
    static int entries = 0;
    ++ entries;
    int back_level = 0;
    ClauseIdx conflict_cl;
    vector<ClauseIdx> added_conflict_clauses;
    int sss = _conflicts.size();
    for (int i=0, sz=_conflicts.size(); i<sz; ++i) {
	ClauseIdx cl = _conflicts[i];

	if (!is_conflict(cl)) continue;

	back_level = 0; // reset it
	while (_conflict_lits.size()) {
	    CVariable & var = variable(_conflict_lits.back() >> 1);
	    _conflict_lits.pop_back();
	    assert (var.in_new_cl() != -1);
	    var.set_in_new_cl(-1);
	}
	int max_dlevel = find_max_clause_dlevel(cl); // find the max level, which is the back track level
	bool first_time = true; //its the beginning
	bool prev_is_uip = false;
	mark_vars_at_level (cl, -1 /*var*/, max_dlevel);

	vector <int> & assignments = *_assignment_stack[max_dlevel];
	for (int j = assignments.size() - 1; j >= 0; --j ) { //now add conflict lits, and unassign vars
	    int assigned = assignments[j];
	    if (variable(assigned>>1).is_marked()) {
		variable(assigned>>1).clear_marked();
		-- _num_marked; 
		ClauseIdx ante_cl = variables()[assigned>>1].get_antecedence();

		if ( (_num_marked == 0 && 
		      (!first_time) && 
		      (prev_is_uip == false))
		      || ante_cl==NULL_CLAUSE) { //conclude add clause
		    assert (variable(assigned>>1).in_new_cl()==-1);
		    _conflict_lits.push_back(assigned^0x1);  // add this assignment's reverse, e.g. UIP
		    int conflict_cl = add_clause(_conflict_lits.begin(), _conflict_lits.size());
		    if (conflict_cl < 0 ) {
			_stats.is_mem_out = true;
			_conflicts.clear();
			assert (_implication_queue.empty());
			return 1; 
		    }
		    _conflict_lits.pop_back();  // remove for continue use of _conflict_lits
		    added_conflict_clauses.push_back(conflict_cl);

		    CHECK(cout <<"Conflict clause: " << cl << " : " << clause(cl) << endl;
			  cout << "**Add Clause " <<conflict_cl<< " : "<<clause(conflict_cl) << endl; 
			);

		    prev_is_uip = true;
		    break; //if do this, only one clause will be added.
		}
		else prev_is_uip = false;

		if ( ante_cl != NULL_CLAUSE ) 
		    mark_vars_at_level(ante_cl, assigned>>1/*var*/, max_dlevel);
		else 
		    assert (j == 0);
		first_time = false;
	    }
	}
	back_level = max_dlevel;
	back_track(max_dlevel);	
    }
    assert (_num_marked == 0);
    if (back_level==0) //there are nothing to be done
	    return back_level;

    if (_params.back_track_complete) {
	for (int i=0; i< added_conflict_clauses.size(); ++i) {
	    ClauseIdx cl = added_conflict_clauses[i];
	    if (find_unit_literal(cl)) { //i.e. if it's a unit clause
  		int dl = find_max_clause_dlevel(cl);
  		if (dl < dlevel()) { //thus make sure implied vars are at current dl.
  		    back_track(dl+1);
		}
	    }
	}
    }
    int cnt = 0;
    for (int i=0, sz=added_conflict_clauses.size(); i<sz; ++i) {
	conflict_cl = added_conflict_clauses[i];
	int lit = find_unit_literal(conflict_cl);
	if (lit) {
	    queue_implication(lit, conflict_cl);
	    ++cnt;
	}
    }
    assert (cnt > 0);
    assert (!_params.back_track_complete || cnt == 1);

    _conflicts.clear();

    while (_conflict_lits.size()) {
	CVariable & var = variable(_conflict_lits.back() >> 1);
	_conflict_lits.pop_back();
	assert (var.in_new_cl() != -1);
	var.set_in_new_cl(-1);
    }
    CHECK( dump_assignment_stack(););
    CHECK(cout << "Conflict Analasis: conflict at level: " << back_level;
  	  cout << "  Assertion Clause is " << conflict_cl<< endl; );
    return back_level;
}