zverify_bf.cpp

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

    cout << "Successfully read " << num_init_clauses() << " Clauses " << endl;
}

void CDatabase::first_pass(void)
{
    _max_clause_id = 0;
    int * fanout_count;
    fanout_count = new int [CLS_COUNT_ARRAY_SIZE];
    bool first = true;
    int base = 0;
    char token[WORD_LEN];
    vector<char> buffer;

    _counter_stream.seekg(0, ios::beg);
    int iteration = 0;
    while (first || _max_clause_id >  base) {
	cout << "Iteration    " << iteration++ << endl;
	_trace_stream.seekg(0,ios::beg);
	_trace_stream.clear();

	for (int i=0; i< CLS_COUNT_ARRAY_SIZE; ++i) 
	    fanout_count[i] = 0;

	while (!_trace_stream.eof()) {
	    get_line(_trace_stream, buffer);
	    char * ptr = &(*buffer.begin());
	    get_token(ptr, token);
	    if (strcmp (token, "CL:") == 0) {
		vector<int> resolvents;

		get_token(ptr, token);
		int cl_id = my_a2i(token);
		if (cl_id > _max_clause_id -1 ) 
		    _max_clause_id = cl_id + 1;
		get_token(ptr, token);
		assert (strcmp(token, "<=") == 0);

		while (get_token(ptr, token)) {
		    int r = my_a2i(token);
		    resolvents.push_back(r);
		}
		for (unsigned i=0; i< resolvents.size(); ++i) {
		    int cl_id = resolvents[i];
		    int index = cl_id - base;
		    if (index >= 0 && index < CLS_COUNT_ARRAY_SIZE) //in the window
			++ fanout_count[index];
		}
	    }
	    else if (strcmp (token, "VAR:") == 0) {
		get_token(ptr,token);
		int vid = my_a2i(token);

		get_token(ptr,token);
		assert (strcmp(token, "L:") == 0);
		get_token(ptr,token); //skip the level

		get_token(ptr,token);
		assert (strcmp(token, "V:") == 0);
		get_token(ptr,token);
		int value = my_a2i(token);
		assert (value == 1 || value == 0);

		get_token(ptr,token);
		assert (strcmp(token, "A:") == 0);
		get_token(ptr,token);
		int ante = my_a2i(token);

		get_token(ptr,token);
		assert (strcmp(token, "Lits:") == 0);

		_variables[vid].value = value;
		_variables[vid].antecedent = ante;
		int index = ante - base;
		if (index >= 0 && index < CLS_COUNT_ARRAY_SIZE) //in the window
		    ++ fanout_count[index];
	    }
	    else if (strcmp (token, "CONF:") == 0) {
		get_token(ptr,token);
		_conf_id = my_a2i(token);
		get_token(ptr,token);
		assert (strcmp(token, "==") == 0);

		int index = _conf_id - base;
		if (index >= 0 && index < CLS_COUNT_ARRAY_SIZE) //in the window
		    ++ fanout_count[index];

		while (get_token(ptr, token) && first) {
		    int lit = my_a2i(token);
		    assert (lit > 0);
		    assert ((unsigned)(lit>>1) < _variables.size());
		    _conf_clause.push_back(lit);
		}
	    }
	}
	int top;
	if (_max_clause_id <  base + CLS_COUNT_ARRAY_SIZE)
	    top = _max_clause_id;
	else 
	    top = base + CLS_COUNT_ARRAY_SIZE;
	for (int i=base; i< top; ++i)
	    _counter_stream << fanout_count[i-base] << endl;

	first = false;
	base += CLS_COUNT_ARRAY_SIZE;
    }	
    delete [] fanout_count;
}

void CDatabase::second_pass(void)
{
    int n_fanout;
    vector<char> buffer;
    char token[WORD_LEN];

    _trace_stream.seekg(0,ios::beg);
    _trace_stream.clear();

    _counter_stream.seekg(0, ios::beg);
    _counter_stream.clear();

    assert (_current_clause_id == _num_init_clauses);
    
    for (int i=0; i< _current_clause_id; ++i) {
	_counter_stream >> n_fanout;
	set_clause_fanout(i, n_fanout);
    }
    _init_clause_count = _current_clause_count;
    
    for (int i=_current_clause_id; i< _max_clause_id; ++i) {
	_counter_stream >> n_fanout;
	while (!_trace_stream.eof()) {
	    get_line(_trace_stream, buffer);
	    char * ptr = &(*buffer.begin());
	    get_token(ptr, token);
	    if (strcmp (token, "CL:") == 0) {
		vector<int> resolvents;

		get_token(ptr, token);
		int cl_id = my_a2i(token);
		assert (cl_id == i);

		get_token(ptr, token);
		assert (strcmp(token, "<=") == 0);

		while (get_token(ptr, token)) {
		    int r = my_a2i(token);
		    resolvents.push_back(r);
		}
		
		if (_output_core) {
		    int storage[resolvents.size() + 2];
		    storage[0] = - cl_id;
		    storage[1] = - resolvents.size();
		    for (unsigned j=0; j< resolvents.size(); ++j)
			storage[j+2] = resolvents[j];
		    fwrite(storage, sizeof(int), resolvents.size() + 2, _tmp_rsource_fp);
		}
		
		add_clause_by_resolvents(cl_id, resolvents);
		_current_clause_id = cl_id + 1;
		set_clause_fanout(cl_id, n_fanout);
		break;
	    }
	}	
    }
//    assert (_counter_stream.eof());
}


void CDatabase::dump(void) 
{
//      cout << "p cnf " << _variables.size() - 1 << " " << _num_init_clauses << endl;
//      for (unsigned i=0; i< _clauses.size(); ++i) {
//  	for (unsigned j=0; j< _clauses[i].literals.size(); ++j ) {
//  	    int lit = _clauses[i].literals[j];
//  	    cout << ((lit & 0x1)?"-":"") << (lit>>1) << " ";
//  	}
//  	cout << "0" << endl;
//      }
}

int CDatabase::recursive_find_level(int vid)
{
    int ante = _variables[vid].antecedent;
    assert (_variables[vid].value != UNKNOWN);
    assert (_variables[vid].antecedent != -1);
    assert (_clauses.find(ante) != _clauses.end());;
    if (_variables[vid].level != -1) 
	return _variables[vid].level;
    int level = -1;
    CClause & cl = *_clauses[ante];
    for (unsigned i=0; i<cl.literals.size(); ++i) {
	int v = (cl.literals[i] >> 1);
	int s = (cl.literals[i] & 0x1);
	if (v == vid) {
	    assert(_variables[v].value != s);
	    continue;
	}
	else {
	    assert(_variables[v].value == s);
	    int l = recursive_find_level(v);
	    if (level < l )
		level = l;
	}
    }
    _variables[vid].level = level + 1;
    return level + 1;
}

void CDatabase::set_var_number(int nvar) 
{ 
    _variables.resize(nvar + 1);
    for (unsigned i=0; i < _variables.size(); ++i) {
	_variables[i].value = UNKNOWN;
	_variables[i].in_clause_phase = UNKNOWN;
    }
}

bool CDatabase::real_verify(void)
{
    cout << "Levelize variables... ";
    for (unsigned i=1; i< _variables.size(); ++i) {
	int cl_id = _variables[i].antecedent;
	if (_variables[i].value != UNKNOWN &&  cl_id != -1) {
	    int level = recursive_find_level(i);
//	    cout << "Var: " << i << " level " << level << endl;
	}
    }
    cout << "finished"<< endl;
    //Can we construct an empty clause? 
    cout << "Begin Resolution... " ;
    set<CVariable *, cmp_var_level> clause_lits;
    assert (_clauses.find(_conf_id) != _clauses.end());
    _empty_r_source.push_back(_conf_id);
    CClause & conf_cl = *_clauses[_conf_id];
    for (unsigned i=0; i< conf_cl.literals.size(); ++i) {
	assert (lit_value(conf_cl.literals[i]) == 0);
	int vid = (conf_cl.literals[i] >> 1);
	clause_lits.insert(&_variables[vid]);
    }	
    assert (clause_lits.size() == conf_cl.literals.size());

    while(!clause_lits.empty()) {
//  	for (set<CVariable *, cmp_var_level>::iterator itr = clause_lits.begin();
//  	     itr != clause_lits.end(); ++itr) {
//  	    int vid = (*itr) - &_variables[0];
//  	    cout << vid << "(" << (*itr)->level << ") ";
//  	}
//  	cout << endl;

	int vid = (*clause_lits.begin() - &_variables[0]);
	int ante = _variables[vid].antecedent;
	if (ante == -1) {
	    cerr << "Variable " << vid << " has an NULL antecedent ";
	    exit(1);
	}
	clause_lits.erase(clause_lits.begin());
	_variables[vid].in_clause_phase = 1;
	assert (_clauses.find(ante) != _clauses.end());
	CClause & cl = *_clauses[ante];
	_empty_r_source.push_back(ante);
	int distance = 0;
	for (unsigned i=0; i< cl.literals.size(); ++i) {
	    int l = cl.literals[i];
	    int v = (l>>1);
	    assert (_variables[v].value != UNKNOWN);
	    if (lit_value(l) == 1) {
		if (vid != v) {
		    cerr << "The antecedent of the variable is not really an antecedent " << endl;
		    exit(1);
		}
		else 
		    ++distance;
	    }
	    else
		clause_lits.insert(&_variables[v]);
	}
	assert (distance == 1);
    }
    cout << " Empty clause generated. " << endl;
    if (_output_core) 
	calculate_unsat_core();
    return true;
}

FILE * CDatabase::reverse_file(FILE * fp_in)
{
    //currently fp_in point to the end of the input file
    assert (((unsigned)MAX_BUFF_SIZE > _variables.size() * 2) && 
	    "Buff must be able to contain at least 2 biggest clauses"); 
    int * read_buff;
    read_buff = (int *) malloc((MAX_BUFF_SIZE + _variables.size())*sizeof(int));
    int * write_buff;
    write_buff = (int*) malloc((MAX_BUFF_SIZE + _variables.size()) * sizeof(int));

    long file_size = ftell(fp_in)/sizeof(int);
    assert (ftell(fp_in)%sizeof(int) == 0);
    int num_trunks = file_size/MAX_BUFF_SIZE;

    FILE * fp = tmpfile();
    int last_remain = 0;
    cout << "Reverse Trunk ";
    for (int i=0; i< num_trunks; ++i) {
	cout << i << " ";
	cout.flush();
	fseek(fp_in, -MAX_BUFF_SIZE*sizeof(int), SEEK_CUR);
	int r = fread(read_buff, sizeof(int), MAX_BUFF_SIZE, fp_in);
	assert (r == MAX_BUFF_SIZE);
	fseek(fp_in, -MAX_BUFF_SIZE*sizeof(int), SEEK_CUR);
	int write_idx = 0;
	for (int index=MAX_BUFF_SIZE - 1 + last_remain; index>= 1; --index) {
	    if (read_buff[index] < 0) {
		assert (read_buff[index -1] < 0);
		int num_lits = -read_buff[index];
		-- index;
		for (int j=0; j< num_lits + 2; ++j)
		    write_buff[write_idx ++] = read_buff[j + index];
	    }
	}
	fwrite(write_buff, sizeof(int), write_idx, fp);
	last_remain = 0;
	for (int j = 0; j < MAX_BUFF_SIZE; ++j) {
	    if (read_buff[j] < 0 && read_buff[j+1] < 0)
		break;
	    else 
		read_buff[j + MAX_BUFF_SIZE] = read_buff[j];
	    ++ last_remain;
	}
    }
    cout <<" Last " << endl;
    //the last trunk
    int last_trunk_size = file_size%MAX_BUFF_SIZE;
    int last_trunk_begin = MAX_BUFF_SIZE - last_trunk_size;
    assert (ftell(fp_in) == (long) (last_trunk_size * sizeof(int)));
    fseek(fp_in, -last_trunk_size*sizeof(int), SEEK_CUR);
    fread(read_buff + last_trunk_begin, sizeof(int), last_trunk_size, fp_in);
    int index; 
    int write_idx = 0;

    for (index = MAX_BUFF_SIZE-1 + last_remain; index >= last_trunk_begin + 1; --index) {
	if (read_buff[index] < 0) {
	    assert (read_buff[index -1] < 0);
	    int num_lits = -read_buff[index];
	    -- index;
	    for (int j=0; j< num_lits + 2; ++j)
		write_buff[write_idx ++] = read_buff[j + index];
	}	
    }
    fwrite(write_buff, sizeof(int), write_idx, fp);
    assert (read_buff[last_trunk_begin] < 0 &&
	    read_buff[last_trunk_begin+1] < 0);
    free(read_buff);
    free(write_buff);
    return fp;
}

void CDatabase::print_file(FILE * fp)
{
    ofstream out("out_file");
    int inputs[_variables.size()];
    int info[2];
    int pos = ftell(fp);
    rewind(fp);
    fread(info, sizeof(int), 2, fp);
    while (!feof(fp)) {
	assert (info[0] < 0);
	assert (info[1] < 0);
	unsigned num_in = -info[1];
	assert ( num_in < _variables.size());
	fread(inputs, sizeof(int), num_in, fp);
	out << "CL : " << -info[0] << " Num: "<< num_in << " :";
	for (unsigned i=0; i< num_in; ++i)
	    out << inputs[i] << " ";
	out << endl;
	fread(info, sizeof(int), 2, fp);
    }	
    fseek (fp, pos, SEEK_SET);
}

void CDatabase::calculate_unsat_core(void)
{
    cout << "Begin Output Unsat Core ... ";
    FILE * r_source_fp;
//      FILE * clause_fp;
//      clause_fp = reverse_file(_tmp_clause_fp);
//      close(_tmp_clause_fp);
//      rewind(clause_fp);

    r_source_fp = reverse_file(_tmp_rsource_fp);
    fclose(_tmp_rsource_fp);
    rewind(r_source_fp);
    hash_set<int> involved;
    for (unsigned i=0; i< _empty_r_source.size(); ++i)
	involved.insert(_empty_r_source[i]);

    int r_source[_variables.size()];
    int info[2];
    
    fread(info, sizeof(int), 2, r_source_fp);
    while (!feof(r_source_fp)) {
	assert (info[0] < 0);
	assert (info[1] < 0);
	int cl_id = -info[0];
	unsigned num_srcs = -info[1];
	assert ( num_srcs < _variables.size());
	fread(r_source, sizeof(int), num_srcs, r_source_fp);
	if (involved.find(cl_id) != involved.end()) {
	    involved.erase(cl_id);
	    for (unsigned i=0; i< num_srcs; ++i) {
		int s= r_source[i];
		assert (s < cl_id);
		involved.insert(s);
	    }
	}
	fread(info, sizeof(int), 2, r_source_fp);
    }	
    fclose(r_source_fp);

    int needed_cls_count = 0;
    int needed_var_count = 0;
    for (int i=0; i< num_init_clauses(); ++i) {
	if (involved.find(i) != involved.end()) {
	    assert (_clauses.find(i) != _clauses.end());
	    ++ needed_cls_count;
	    CClause & cl = * _clauses[i];
	    for (unsigned j=0; j< cl.literals.size(); ++j) {
		int vid = (cl.literals[j] >> 1);
		if (_variables[vid].is_needed == false) {
		    ++ needed_var_count;
		    _variables[vid].is_needed = true;
		}
	    }
	}
    }
    cout << "Original Num. Clauses:\t\t\t" << num_init_clauses() << endl;
    cout << "Needed Clauses to Construct Empty:\t"<< needed_cls_count << endl;
    cout << "Total Variable count:\t\t\t" << _variables.size()-1 << endl;
    cout << "Variables involved in Empty:\t\t" << needed_var_count << endl;
    ofstream dump("unsat_core.cnf");
    dump << "c Variables Not Involved: ";
    unsigned int k=0;
    for (unsigned i=1; i< _variables.size(); ++i) {
	if (_variables[i].is_needed == false) {
	    if (k%20 == 0) 
		dump << endl << "c ";
	    ++k;
	    dump << i << " ";
	}
    }
    dump << endl;
    dump << "p cnf " << _variables.size()-1 << " " << needed_cls_count << endl;
    for (int i=0; i< num_init_clauses(); ++i) {
	if (involved.find(i) != involved.end()) {
	    CClause & cl = * _clauses[i];
	    dump << "c Original Cls ID: " << i << endl;
	    for (unsigned j=0; j< cl.literals.size(); ++j)
		dump << ((cl.literals[j] & 0x1)?" -":" ") << (cl.literals[j] >> 1);
	    dump << " 0" << endl;
	}
    }
}


int main(int argc, char * * argv)
{
    cout << "ZVer SAT Solver Verifier" << endl;
    cout << "Copyright Princeton University, 2002-2004. All Right Reseverd." << endl;
    if (argc != 3 && argc != 4) {
	cout << "Usage: verify CNF_File Dump_File [-core]" << endl;
	cout << "-core : output the unsat core of the instance " << endl;
	cout << endl;
	exit(1);
    }
    _peak_mem = get_mem_usage();
    CDatabase dbase;
    double begin_time = get_cpu_time();
    dbase.init(argv[1], argv[2]);

    if (argc == 4) {
	if (strcmp(argv[3], "-core")!=0) {
	    cerr << "The third argument must be -core" << endl;
	    exit(1);
	}
	dbase.set_output_core(true);
    }
    else 
	dbase.set_output_core(false);

    bool status = dbase.verify();

    cout << "Total Runtime\t\t\t\t" << get_cpu_time() - begin_time << endl;
    cout << "Peak Mem Usage\t\t\t\t" << _peak_mem << endl;
    if (status == true) 
	cout << "Verify Successful " << endl;
    else 
	cout << "Failed to verify the result " << endl;

    return (0);
}