zchaff_dbase.cpp

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

    return (double)num_literals()/((double) (lit_pool_size() - num_clauses())) ; 
}

CLitPoolElement & CDatabase::lit_pool(int i) 
{
    return _lit_pool_start[i];
}

void CDatabase::compact_lit_pool(void)
{
    unsigned i, sz;
    DBG1(cout << "Begin Compaction...... " << 
	 endl << "***Before Compaction "<< endl;  
	 output_lit_pool_stats(););
    int new_index = 1;
    int skipped = 0;
    //first do the compaction for the lit pool
    for (i=1, sz= lit_pool_size(); i<sz;  ++i){ //begin with 1 because 0 position is always 0
	if (!lit_pool(i).is_literal() && !lit_pool(i-1).is_literal())
	    continue;
	else {
	    lit_pool(new_index) = lit_pool(i);
	    ++new_index;
	}
    }
    _lit_pool_finish = lit_pool_begin() + new_index;
    //update all the pointers to the literals;
    //1. clean up the watched pointers from variables
    for (i=1, sz = variables().size(); i< sz;  ++i) {
	variable(i).watched(0).clear();
	variable(i).watched(1).clear();
    }
    for (i=1, sz = lit_pool_size(); i<sz;  ++i) {	
	CLitPoolElement & lit = lit_pool(i);
        //2. reinsert the watched pointers
	if (lit.is_literal()) {
	    if (lit.is_watched()) {
		int var_idx = lit.var_index();
		int sign = lit.var_sign();
		variable(var_idx).watched(sign).push_back(& lit_pool(i));
	    }
	}
	//3. update the clauses' first literal pointer
	else { //lit is not literal
	    int cls_idx = lit.get_clause_index();
	    clause(cls_idx).first_lit() = &lit_pool(i) - clause(cls_idx).num_lits();
	}
    }
    DBG1(cout << "***After Compaction " << endl; 
	 output_lit_pool_stats(); 
	 cout << endl << endl;);
    ++_stats.num_compact;
}

bool CDatabase::enlarge_lit_pool(void) //will return true if successful, otherwise false.
{
    unsigned i, sz;
    //if memory efficiency < 2/3, we do a compaction
    if ( lit_pool_utilization() < 0.67) {
	compact_lit_pool();
	return true;
    }
    //otherwise we have to enlarge it.
    DBG1(cout << "Begin Enlarge Lit Pool" << endl;);
    //first, check if memory is running out
    int current_mem = estimate_mem_usage();
    float grow_ratio = 1;
    if (current_mem < _params.mem_limit /4 ) 
	grow_ratio = 2;
    else if (current_mem < _params.mem_limit /2 ) 
	grow_ratio = 1.5;
    else if (current_mem < _params.mem_limit * 0.8) 
	grow_ratio = 1.2;
    if (grow_ratio < 1.2) {
	if ( lit_pool_utilization() < 0.9) {  //still has some garbage
	    compact_lit_pool();
	    return true;
	}
	else 
	    return false;
    }
    //second, make room for new lit pool.
    CLitPoolElement * old_start = _lit_pool_start;
    CLitPoolElement * old_finish = _lit_pool_finish;
    int old_size = _lit_pool_end_storage - _lit_pool_start;
    int new_size = (int)(old_size * grow_ratio);
    _lit_pool_start = (CLitPoolElement *) realloc( _lit_pool_start, sizeof(CLitPoolElement) * new_size);
    _lit_pool_finish = _lit_pool_start + (old_finish - old_start);
    _lit_pool_end_storage = _lit_pool_start + new_size;

    //update all the pointers
    int displacement = _lit_pool_start - old_start;
    for (i=0; i< clauses().size(); ++i)
	if (clause(i).status()!=DELETED_CL) 
	    clause(i).first_lit() += displacement; 

    for (i=0, sz = variables().size(); i < sz ;  ++i) {
	CVariable & v = variable(i);
	for (int j=0; j< 2 ; ++j) {
	    int k, sz1;
	    vector<CLitPoolElement *> & watched = v.watched(j);
	    for (k=0, sz1 = watched.size(); k< sz1 ; ++k) {
		watched[k] += displacement; 
	    }
	}
    }
    DBG1(output_lit_pool_stats();
	 cout << endl << endl;);
    ++_stats.num_enlarge;
    return true;
}

ClauseIdx CDatabase::get_free_clause_idx(void)
{
    ClauseIdx new_cl;
    new_cl = _clauses.size();
    _clauses.resize(new_cl + 1);
    clause(new_cl).set_id(_stats.num_added_clauses);
    return new_cl;
}

ClauseIdx CDatabase::add_clause(int * lits, int n_lits, int gflag)  { 
    int new_cl;
    //a. do we need to enlarge lits pool?
    while (lit_pool_free_space() <= n_lits + 1) { 
	if (enlarge_lit_pool()==false) 
	    return -1; //mem out, can't enlarge lit pool, because 
	//ClauseIdx can't be -1, so it shows error.
    }
    //b. get a free cl index;
    new_cl = get_free_clause_idx();
    //c. add the clause lits to lits pool
    CClause & cl = clause(new_cl);
    cl.init(lit_pool_end(), n_lits, gflag);
    lit_pool_incr_size(n_lits + 1);
    if(n_lits==2){
        ++variable(lits[0]>>1).two_lits_count(lits[0]&0x1);
        ++variable(lits[1]>>1).two_lits_count(lits[1]&0x1);
    }
    for (int i=0; i< n_lits; ++i){
	int var_idx = lits[i]>>1;
	assert((unsigned)var_idx < variables().size());
	int var_sign = lits[i]&0x1;
	cl.literal(i).set(var_idx, var_sign);
	++variable(var_idx).lits_count(var_sign);
#ifdef KEEP_LIT_CLAUSES
	variable(var_idx).lit_clause(var_sign).push_back(new_cl);
#endif
    }
    //the element after the last one is the spacing element
    cl.literal(n_lits).set_clause_index(new_cl); 
    //d. set the watched pointers
    if (cl.num_lits() > 1) {
	//add the watched literal. note: watched literal must be the last free var
	int max_idx = -1, max_dl = -1;
	int i, sz = cl.num_lits();
	//set the first watched literal
	for (i=0; i< sz; ++i) {
	    int v_idx = cl.literal(i).var_index();
	    int v_sign = cl.literal(i).var_sign();
	    CVariable & v = variable(v_idx);
	    if (literal_value(cl.literal(i)) != 0 ){
		v.watched(v_sign).push_back( & cl.literal(i));
		cl.literal(i).set_watch(1);
		break;
	    }
	    else {
		if (v.dlevel() > max_dl) {
		    max_dl = v.dlevel();
		    max_idx = i;
		}
	    }
	}
	if (i >= sz) { //no unassigned literal. so watch literal with max dlevel
	    int v_idx = cl.literal(max_idx).var_index();
	    int v_sign = cl.literal(max_idx).var_sign();
	    variable(v_idx).watched(v_sign).push_back( & cl.literal(max_idx));
	    cl.literal(max_idx).set_watch(1);
	}
	//set the second watched literal
	max_idx = -1; max_dl = -1;
	for (i=sz-1; i>=0; --i) {
	    if (cl.literal(i).is_watched())
		continue; // need to watch two different literals
	    int v_idx = cl.literal(i).var_index();
	    int v_sign = cl.literal(i).var_sign();
	    CVariable & v = variable(v_idx);
	    if (literal_value(cl.literal(i)) != 0) {
		v.watched(v_sign).push_back( & cl.literal(i));
		cl.literal(i).set_watch(-1);
		break;
	    }
	    else {
		if (v.dlevel() > max_dl) {
		    max_dl = v.dlevel();
		    max_idx = i;
		}
	    }
	}
	if (i < 0) {
	    int v_idx = cl.literal(max_idx).var_index();
	    int v_sign = cl.literal(max_idx).var_sign();
	    variable(v_idx).watched(v_sign).push_back( & cl.literal(max_idx));
	    cl.literal(max_idx).set_watch(-1);
	}
    }
    //update some statistics
    ++_stats.num_added_clauses; 
    _stats.num_added_literals += n_lits;
    return new_cl;
}


void CDatabase::output_lit_pool_stats (void) 
{
    cout << "Lit_Pool Used " << lit_pool_size() << " Free " << lit_pool_free_space()
	 << " Total " << lit_pool_size() + lit_pool_free_space()
	 << " Num. Cl " << num_clauses() << " Num. Lit " << num_literals(); 
    cout << " Efficiency " <<  lit_pool_utilization() << endl;
}


void CDatabase::detail_dump_cl(ClauseIdx cl_idx, ostream & os ) 
{
    os << "CL : " << cl_idx;
    CClause & cl = clause(cl_idx);
    if (cl.status()==DELETED_CL) 
	os << "\t\t\t======removed=====";
    char value;
    for (unsigned i=0; i< cl.num_lits(); ++i) {
	if (literal_value(cl.literal(i))==0) value = '0';
	else if (literal_value(cl.literal(i))==1) value = '1';
	else value = 'X';
	os << cl.literal(i) << "(" << value << "@" << variable(cl.literal(i).var_index()).dlevel()<< ")  ";
    }
    os << endl;
}

void CDatabase::dump(ostream & os) {
    unsigned i;
    os << "Dump Database: " << endl;
    for( i=0; i<_clauses.size(); ++i) 
	detail_dump_cl(i);
    for( i=1; i<_variables.size(); ++i)
	os << "VID " << i << ":\t" << variable(i);
}