zverify_df.cpp

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

//  		cerr << "One of the clause involved is " << cl1 << endl;
//  		exit(1);
//  	    }
//  	}
	    
//  	for (unsigned i=0; i< literals.size(); ++i) {
//  	    int lit = literals[i];
//  	    int vid = (lit>>0x1);
//  	    int sign = (lit&0x1);
//  	    if (_variables[vid].in_clause_phase == UNKNOWN) 
//  		continue;
//  	    assert (_variables[vid].in_clause_phase == sign);
//  	    _variables[vid].in_clause_phase = UNKNOWN;
//  	    cl.my_literals.push_back(lit);
//  	}
//  	::sort(cl.my_literals.begin(), cl.my_literals.end());
//  	cl.my_is_built = true;
//      }
//  }

void CDatabase::recursive_find_involved(int cl_id) 
{
    if (_clauses[cl_id].is_involved == true)
	return;
    _clauses[cl_id].is_involved = true;
    
    recursive_construct_clause(cl_id);
    
    int num_1 = 0;
    for (unsigned i=0; i< _clauses[cl_id].literals.size(); ++i) {
	int lit = _clauses[cl_id].literals[i];
	int vid = (lit>>1);
	int sign = (lit & 0x1);
	assert (_variables[vid].value != UNKNOWN);
	if ((_variables[vid].value == 1 && sign == 0) ||
	    (_variables[vid].value == 0 && sign == 1)) {
	    if (num_1 == 0) 
		++ num_1;
	    else {
		cerr << "Clause " << cl_id << " has more than one value 1 literals " << endl;
		exit(1);
	    }
	}
	else { //literal value 0, so seek its antecedent
	    int ante = _variables[vid].antecedent;
	    recursive_find_involved(ante);
	}
    }
}

void CDatabase::recursive_construct_clause(int cl_id)
{
    CClause & cl = _clauses[cl_id];
    if (cl.is_built == true)
	return;

    assert (cl.resolvents.size() > 1);

    //I have to construct them first because of recursion may
    //mess up with the in_clause_signs. 
    for (unsigned i=0; i< cl.resolvents.size(); ++i) {
	_clauses[cl.resolvents[i]].is_needed = true;
	recursive_construct_clause(cl.resolvents[i]);
    }
    
//      cout << "Constructing clause " << cl_id << endl;
    vector<int> literals;

    //initialize
    int cl1 = cl.resolvents[0];
    assert (_clauses[cl1].is_built);
    for (unsigned i=0; i< _clauses[cl1].literals.size(); ++i) {
	int lit = _clauses[cl1].literals[i];
	int vid = (lit>>0x1);
	int sign = (lit&0x1);
	assert (_variables[vid].in_clause_phase == UNKNOWN);
	_variables[vid].in_clause_phase = sign;
	literals.push_back(lit);
    }
    
    for (unsigned i=1; i< cl.resolvents.size(); ++i) {
	int distance = 0;
	int cl1 = cl.resolvents[i];
	assert (_clauses[cl1].is_built);
	for (unsigned j=0; j< _clauses[cl1].literals.size(); ++j) {
	    int lit = _clauses[cl1].literals[j];
	    int vid = (lit>>0x1);
	    int sign = (lit&0x1);
	    if (_variables[vid].in_clause_phase == UNKNOWN) {
		_variables[vid].in_clause_phase = sign;
		literals.push_back(lit);
	    }
	    else if (_variables[vid].in_clause_phase != sign) {
				//distance 1 literal
		++distance;
		_variables[vid].in_clause_phase = UNKNOWN;
	    }
	}
	if (distance != 1) {
	    cerr << "Resolve between two clauses with distance larger than 1" << endl;
	    cerr << "The resulting clause is " << cl_id << endl;
	    cerr << "Starting clause is " << cl.resolvents[0] << endl;
	    cerr << "One of the clause involved is " << cl1 << endl;
	    exit(1);
	}
    }
    vector<int> temp_cls;
    for (unsigned i=0; i< literals.size(); ++i) {
	int lit = literals[i];
	int vid = (lit>>0x1);
	int sign = (lit&0x1);
	if (_variables[vid].in_clause_phase == UNKNOWN) 
	    continue;
	assert (_variables[vid].in_clause_phase == sign);
	_variables[vid].in_clause_phase = UNKNOWN;
	temp_cls.push_back(lit);
    }
    cl.literals.resize(temp_cls.size());
    for (unsigned i=0; i< temp_cls.size(); ++i)
	cl.literals[i] = temp_cls[i];

//      ::sort(cl.literals.begin(), cl.literals.end());
//      assert (cl.literals.size()== cl.my_literals.size());
//      for (unsigned i=0; i< cl.literals.size(); ++i)
//  	assert (cl.literals[i] == cl.my_literals[i]);
    cl.is_built = true;
    ++ _current_num_clauses;
    if (_current_num_clauses%10 == 0)
	check_mem_out();	
}

int CDatabase::recursive_find_level(int vid)
{
    int ante = _variables[vid].antecedent;
    assert (_variables[vid].value != UNKNOWN);
    assert (_variables[vid].antecedent != -1);
    assert (_clauses[ante].is_involved);
    if (_variables[vid].level != -1) 
	return _variables[vid].level;
    int level = -1;
    for (unsigned i=0; i<_clauses[ante].literals.size(); ++i) {
	int v = (_clauses[ante].literals[i] >> 1);
	int s = (_clauses[ante].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;
}

bool CDatabase::real_verify(void)
{
    //1. If a variable is assigned value at dlevel 0, 
    //either it's pure or it has an antecedent
    for (unsigned i=1; i< _variables.size(); ++i) {
	if (_variables[i].value != UNKNOWN && _variables[i].antecedent == -1) {
	    if ((_variables[i].num_lits[0]==0 && _variables[i].value==0) || 
		(_variables[i].num_lits[1]==0 && _variables[i].value==1)) {
//  		cout << "Variable " << i << " is assigned " << _variables[i].value
//  		     << " because it is pure literal. " << endl;
	    }
	    else {
		cerr << "Don't know why variable " << i << " is assigned " << _variables[i].value
		     << " for no reasons" << endl;
		exit(1);
	    }
	}
    }
    //2. Construct the final conflicting clause if needed and find all 
    //the clauses that are involved in making it conflicting
    cout << "Begin constructing all involved clauses " << endl;
    _clauses[_conf_id].is_needed = true;
    recursive_find_involved(_conf_id);
    int count = 0;
    for (unsigned i=num_init_clauses(); i< _clauses.size(); ++i)
	if (_clauses[i].is_built)
	    ++ count;
    cout << "Num. Learned Clause:\t\t\t" << _clauses.size() - num_init_clauses() << endl;
    cout << "Num. Clause Built:\t\t\t" << count << endl;
    cout << "Constructed all involved clauses " << endl;
    
    //2.5. Verify the literals in the CONF clause
    assert(_clauses[_conf_id].is_built);
    assert(_clauses[_conf_id].is_involved);
    bool _found;
    for(unsigned i=0;i<_conf_clause.size();i++){
        _found=false;
        for(unsigned j=0;j<_clauses[_conf_id].literals.size();j++){
            if(_conf_clause[i]==_clauses[_conf_id].literals[j]){
                _found=true;
                break;
            }
        }
        if(!_found){
            cerr << "The conflict clause in trace can't be verified! "<<endl;
            cerr << "Literal "<<_conf_clause[i]<<" is not found."<<endl;
        }
    }
    cout << "Conflict clause verification finished." <<endl;

    //3. Levelize the variables that are decided at dlevel 0
    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) {
	    if (_clauses[cl_id].is_involved) {
		int level = recursive_find_level(i);
//  		cout << "Var: " << i << " level " << level << endl;
	    }
	}
    }
    cout << "finished"<< endl;
    //4. Can we construct an empty clause? 
    cout << "Begin Resolution..." ;
    set<CVariable *, cmp_var_level> clause_lits;
    for (unsigned i=0; i< _clauses[_conf_id].literals.size(); ++i) {
	assert (lit_value(_clauses[_conf_id].literals[i]) == 0);
	int vid = (_clauses[_conf_id].literals[i] >> 1);
	clause_lits.insert(&_variables[vid]);
    }
    assert (clause_lits.size() == _clauses[_conf_id].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);
	}
	_clauses[ante].is_needed = true;
	clause_lits.erase(clause_lits.begin());
	_variables[vid].in_clause_phase = 1;
	CClause & cl = _clauses[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;
    cout << "Mem Usage :\t\t\t\t" << get_mem_usage()<< endl;
    int needed_cls_count = 0;
    int needed_var_count = 0;
    for (int i=0; i< num_init_clauses(); ++i) {
	if (_clauses[i].is_needed == true) {
	    ++ needed_cls_count;
	    for (unsigned j=0; j< _clauses[i].literals.size(); ++j) {
		int vid = (_clauses[i].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;

    for (unsigned i=0; i< _clauses.size(); ++i) {
	if (_clauses[i].is_built)
	    assert (_clauses[i].is_needed || i < (unsigned)num_init_clauses());
    }
    if (_dump_core == true) {
	cout << "Unsat Core dumped:\t\t\tunsat_core.cnf" << 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 (_clauses[i].is_needed) {
		dump << "c Original Cls ID: " << i << endl;
		for (unsigned j=0; j< _clauses[i].literals.size(); ++j)
		    dump << ((_clauses[i].literals[j] & 0x1)?" -":" ") << (_clauses[i].literals[j] >> 1);
		dump << " 0" << endl;
	    }
	}
    }
    return true;
}

bool CDatabase::verify(char * filename)
{	
    vector<char> buffer;
    char token [WORD_LEN];

    ifstream in_file (filename);
    if (!in_file) {
	cerr << "Can't open input CNF file " << filename << endl;
	exit(1);
    }
    
    while (!in_file.eof()) {
	get_line(in_file, 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);

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

	    while (get_token(ptr, token)) {
		int r = my_a2i(token);
		resolvents.push_back(r);
	    }
	    int c = add_learned_clause_by_resolvents(resolvents);
	    assert (c == cl_id);
	}
	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;
	}
	else if (strcmp (token, "CONF:") == 0) {
	    get_token(ptr,token);
	    _conf_id = my_a2i(token);

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

	    while (get_token(ptr, token)) {
		int lit = my_a2i(token);
		assert (lit > 0);
		assert ((lit>>1) < (int)_variables.size());
		_conf_clause.push_back(lit);
	    }
	}
    }	
    if (_conf_id == -1) {
	cerr << "No final conflicting clause defined " << endl;
	exit (1);
    }
    cout << "Mem Usage After Readin file:\t\t" << get_mem_usage() << endl;
//      construct_learned_clauses();
//      for (unsigned i=num_init_clauses(); i< _clauses.size(); ++i) {
//  	assert (_clauses[i].my_is_built);
//  	for (unsigned j=0; j< _clauses[i].my_literals.size(); ++j) {
//  	    int svar = _clauses[i].my_literals[j];
//  	    int vid = (svar>>1);
//  	    int sign = (svar&0x1);
//  	    cout << (sign?"-":"") << vid << " " ;
//  	}
//  	cout << endl;
//      }
//      return true;
    return real_verify();
}

int main(int argc, char * * argv)
{
    cout << "ZVerify SAT Solver Verifier" << endl;
    cout << "Copyright Princeton University, 2003-2004. All Right Reseverd." << endl;
    if (argc != 3 && argc !=4) {
	cerr << "Usage: " << argv[0] << " CNF_File Dump_File [-core]" << endl
	     << "-core: dump the unsat core " << endl;
	cerr << endl;
	exit(1);
    }
    if (argc == 3) 
	_dump_core = false;
    else {
	assert (argc == 4);
	if (strcmp(argv[3], "-core") != 0) {
	    cerr << "Must use -core as the third parameter" << endl;
	    exit(1);
	}
	_dump_core = true;
    }
    cout << "COMMAND LINE: ";
    for (int i=0; i< argc; ++i) 
	cout << argv[i] << " ";
    cout << endl;

    _peak_mem = get_mem_usage();
    CDatabase dbase;
    double begin_time = get_cpu_time();
    dbase.read_cnf(argv[1]);
    if (dbase.verify(argv[2]) == true) {
	double end_time = get_cpu_time();
	cout << "CPU Time:\t\t\t\t" << end_time - begin_time << endl;
	cout << "Peak Mem Usage:\t\t\t\t" << _peak_mem << endl;
	cout << "Verification Successful " << endl;
    }
    else {
	cout << "Failed to verify the result " << endl;
    }
}