zchaff_probe.cpp

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

    }
    return NO_CONFLICT;
}



int CSolver::justify_one_clause(ClauseIdx cls_idx) 
//this will probe free variables in the clause one by one
{    
    CClause & cl = clause(cls_idx);
    vector<int> need_to_probe;
    for (int i=0; i< cl.num_lits(); ++i) {
	int litvalue = literal_value(cl.literal(i));
	if (litvalue==1)
	    return NO_CONFLICT;
	else if (litvalue != 0)
	    need_to_probe.push_back(cl.literal(i).s_var());
    }
    int num_free_lits = need_to_probe.size();
    assert (num_free_lits > 1);

    DBG1(cout << "Justify "; detail_dump_cl(cls_idx); cout <<endl;);
    //1. The first free lit
    ++ dlevel();
    int dl = dlevel();
    queue_implication(need_to_probe[0], NULL_CLAUSE);
    do_deduction();
    if (dlevel() != dl) //conflict happened
	return CONFLICT;
    //common will keep the common implications
    vector<int> common(*_assignment_stack[dlevel()]);
    //undo the implication
    back_track(dlevel());
    ::sort(common.begin(), common.end());
    //2. The rest free lit
    for (int i=1; i< num_free_lits; ++i) {
	++ dlevel();
	queue_implication(need_to_probe[i], NULL_CLAUSE);
	do_deduction();
	if (dlevel() != dl) //conflict happened
	    return CONFLICT;
	//get the common implication
	vector<int> temp1(*_assignment_stack[dlevel()]);
	get_common(temp1, common);
	back_track(dlevel());
	if (common.empty()) return NO_CONFLICT;
    }
    assert (!common.empty());
    DBG0(	cout << "Recursive learning found "; 
		dump_vector(common); 
		cout << endl;);
    vector<int> cls_lits;
    //this is the reason, though not a good one, for the implication
    for (int i=1; i<= dlevel(); ++i) 
	cls_lits.push_back( (*_assignment_stack[i])[0] ^ 0x1);
    //add the reason clause, and make the implication
    for (int i=0; i< common.size(); ++i) {
	cls_lits.push_back(common[i]);
	int cl = add_probe_clause(cls_lits);
	queue_implication(common[i], cl); 
	cls_lits.pop_back();
    }
    int result = deduce();
    assert(result != CONFLICT);
    return NO_CONFLICT;
}






//  int CSolver::simplify() 
//  {
//      vector<pair<int,int> > equiv_svar_pair;
//      if (probe(equiv_svar_pair)==CONFLICT) return CONFLICT;
//      assert (_simplified_inst==NULL);
//      _simplified_inst = new CSolver;

//      _var_map.clear();
//      for (int i=0; i<= variables().size(); ++i)
//  	_var_map.push_back(i); //e.g. each var map to itself
//      for (int i=0; i<= variables().size(); ++i)
//  	if (variable(i).value() != UNKNOWN) 
//  	    _var_map[i] = 0;
//      for (int i=0; i< equiv_svar_pair.size(); ++i) {
//  	int va = equiv_svar_pair[i].first>>1;
//  	int sa = equiv_svar_pair[i].first & 0x1;
//  	int vb = equiv_svar_pair[i].second>>1;
//  	int sb = equiv_svar_pair[i].second & 0x1;
//  	if (sa == sb) _var_map[vb] = va;
//  	else _var_map[vb] = -va;
//      }
//      for (bool modified=true; modified; ) {
//  	modified = false;
//  	for (int i=1; i< variables().size(); ++i) {
//  	    int equiv = _var_map[i];
//  	    if (_var_map[abs(equiv)] != abs(equiv)) {
//  		int equiv_equiv = _var_map[abs(equiv)];
//  		if (equiv>0 )
//  		    _var_map[i] = equiv_equiv;
//  		else 
//  		    _var_map[i] = -equiv_equiv;
//  		modified = true;
//  	    }
//  	}
//  	for (int i=0; i< variables().size(); ++i) {
//  	    cout << i << "(" << _var_map[i] << ")  ";
//  	}
//  	cout << endl << endl;
//      }
//      int new_idx = 0;
//      for (int i=0; i< variables().size(); ++i) {
//  	if (_var_map[i] == i) {
//  	    _var_map[i] = new_idx;
//  	    ++new_idx;
//  	}
//  	else {
//  	    assert (_var_map[i] < i && _var_map[i] > -i);
//  	    if (_var_map[i] < 0)
//  		_var_map[i] = - _var_map[-_var_map[i]];
//  	    else 
//  		_var_map[i] = _var_map[_var_map[i]];
//  	}
//      }
//      _simplified_inst->set_variable_number(new_idx);
//      for (int i=0; i< clauses().size(); ++i) {
//  	set<int> lits;
//  	set<int> vars;
//  	CClause & cl = clause(i);
//  	if (cl.status() != IN_USE) continue;
//  	int j;
//  	for ( j=0; j< cl.num_lits(); ++j) {
//  	    if (literal_value(cl.literal(j))==1) break;
//  	    if (literal_value(cl.literal(j))==0) continue;
//  	    int vidx = cl.literal(j).var_index();
//  	    int vsign = cl.literal(j).var_sign();
//  	    int actual_vidx = _var_map[vidx];
//  	    int actual_vsign = 0;
//  	    if (actual_vidx < 0) {
//  		actual_vidx = - actual_vidx;
//  		actual_vsign = 1;
//  	    }
//  	    actual_vsign = vsign ^ actual_vsign;
//  	    lits.insert((actual_vidx<<1) + actual_vsign);
//  	    vars.insert(actual_vidx);
//  	}
//  	if (j < cl.num_lits() || lits.size() != vars.size()) continue;
//  	vector<int> temp;
//  	for (set<int>::iterator itr = lits.begin(); itr != lits.end(); ++itr) 
//  	    temp.push_back(*itr);
//  	_simplified_inst->add_clause(temp.begin(), temp.size());
//      }
//      ofstream out("out.cnf");
//      out << "p cnf " << new_idx-1 << "  " << _simplified_inst->num_clauses() << endl;
//      for (int i=0; i< _simplified_inst->num_clauses(); ++i) {
//  	CClause & cl = _simplified_inst->clause(i);
//  	for (int j=0; j< cl.num_lits(); ++j) {
//  	    if (cl.literal(j).var_sign())
//  		out << "-";
//  	    out << cl.literal(j).var_index() << " ";
//    	}
//  	out << "0" << endl;
//      }
//      out.close();
//      cout <<"Found equivalence, so exit, output to out.cnf" << endl;
//      exit(0);
//      return NO_CONFLICT;
//  }

//  int CSolver::probe(vector<pair<int,int> > & equiv_svar_pair) 
//  {
//      int dl = dlevel();

//      vector<vector<ClauseIdx> > candidate[2];

//      //use candidate to store the candidate clause for recursive learning
//      candidate[0].resize(variables().size());
//      candidate[1].resize(variables().size());

//      if (_params.do_recursive_learning) {
//  	for (int i=0; i< clauses().size(); ++i) {
//  	    if (clause(i).status() == DELETED_CL) 
//  		continue;
//  	    CClause & cl = clause(i);
//  	    int num_lits = cl.num_lits();
//  	    int free_lits = 0;
//  	    int j;
//  	    for ( j=0; j< num_lits; ++j) {
//  		if (literal_value(cl.literal(j))==0)
//  		    continue;
//  		else if (literal_value(cl.literal(j))==1)
//  		    break;
//  		else
//  		    ++ free_lits;
//  	    }
//  	    if (j < num_lits || //i.e. break occured, clause SAT
//  		free_lits > _params.max_recursive_learning_cl_length)
//  		continue;
//  	    for (j=0; j< num_lits; ++j) {
//  		int vidx = cl.literal(j).var_index();
//  		int phase = cl.literal(j).var_sign();
//  		if (variable(vidx).value() == UNKNOWN ) {
//  		    candidate[phase][vidx].push_back(i);
//  		}
//  	    }
//  	}
//      }
//      //implication table store relationship a=>b. We need a < b; 
//      PairHash implication_table;
//      for (int i=1; i<= num_variables(); ++i) {
//  	cout << "Probing VID : " << i << endl;
//  	assert (dlevel()==dl);
//  	if (variable(i).value() != UNKNOWN) 
//  	    continue;
//  	for (int phase = 0; phase < 2; ++phase) {
//  	    vector<ClauseIdx> & probe_candidates = candidate[!phase][i];	
//  	    if (probe_one_variable_assignment(i, 
//  					      phase,
//  					      implication_table, 
//  					      equiv_svar_pair,
//  					      probe_candidates)==CONFLICT) {
//  		if (dlevel()==dl) {
//  		    phase = -1;
//  		}
//  		else {
//  		    if (dlevel() < 0)
//  			return CONFLICT;
//  		    dl = dlevel(); //make it the new probing level;
//  		    implication_table.clear();
//  		    i=0; //probe every var again, because we reached a new dlevel
//  		    break;
//  		}
//  	    }
//  	}
//      }
//      return NO_CONFLICT;
//  }

//  int CSolver::probe_one_variable_assignment(int vidx, int phase, 
//  					   PairHash& implication_table,
//  					   vector<pair<int,int> > & equiv_svar_pair,
//  					   vector<ClauseIdx>& probe_cl_candidates)
//  {
//      CHECK(  cout << "Probe " << vidx << " with value " << !phase << endl; );
//      assert( _implication_queue.empty());
//      ++dlevel();
//      int dl = dlevel();
//      int probe_lit = vidx+vidx+phase;
//      queue_implication(probe_lit , NULL_CLAUSE);
//      bool is_conflict= false;
//      while (deduce() == CONFLICT) {
//  	is_conflict = true;
//  	if (analyze_conflicts() <= 0)
//  	    break; //no need to deduce ananymore.
//      }
//      if (is_conflict==true) 
//  	return CONFLICT;

//      if (_params.do_recursive_learning) {
//  	vector<ClauseIdx> cls = probe_cl_candidates;
//  	for (int i=0; i<cls.size(); ++i) {
//  	    assert (dlevel()==dl);
//  	    if (justify_one_clause(cls[i])==CONFLICT) {
//  		if (dlevel() < dl) 
//  		    return CONFLICT;
//  		else {
//  		    assert (dl == dlevel());
//  		    i = -1; //redo the probe
//  		}
//  	    }
//  	}
//      }
//      vector<int> assign(*_assignment_stack[dlevel()]);
//      back_track(dlevel()); //now undo the whole probe

//      assert( _implication_queue.empty());
//      for (int j=1; j< assign.size(); ++j) {
//  	int a, b; //we will add a=>b into implication_table, maintain a < b;
//  	int v = assign[j]>> 1;
//  	int sign = assign[j]&0x1;
//  	if (v > vidx) {
//  	    a = probe_lit;
//  	    b = assign[j] ;
//  	}
//  	else {
//  	    a = assign[j] ^ 0x1;
//  	    b = probe_lit ^ 0x1;
//  	}
//    	if (!hash_contain(implication_table, a, b)) {
//  	    hash_insert(implication_table, a, b);
//  	    if (hash_contain(implication_table, a^0x1, b)) {
//  		DBG0(cout << "Probe infered " << b  << " must be true " << endl;);
//  		vector<int> lits;
//  		for (int i=1; i< dlevel(); ++i)
//  		    lits.push_back( (*_assignment_stack[i])[0] ^ 0x1);
//  		lits.push_back(b);
//  		int cl = add_clause(lits.begin(), lits.size());
//  		queue_implication(b, cl);
//  	    }
//  	    else if (hash_contain(implication_table, a^0x1, b^0x1)) {
//  		equiv_svar_pair.push_back(pair<int,int>(a, b));
//  		DBG0(
//  		    cout << "Found " << a << " <==> " << b << endl;
//  		    if ((a&0x1)==(b&0x1) )	
//  		    cout << "i.e. " << a/2 <<"<===>" <<b/2 << endl;
//  		    else 
//  		    cout << "i.e. " << a/2 <<"<===>-" << b/2 << endl;
//  		    );
//  	    }
//  	}
//      }
//      if (!_implication_queue.empty()) {
//  	int result = deduce();
//  	assert (result == NO_CONFLICT);
//      }
//      return NO_CONFLICT;
//  }
//  //  		cout << "Probe infered " << a << " <==> " << b << endl;

//  //  		 b can be replaced by a, i.e. a<=>b
//  //  	    vector<int> lits;
//  //  	    for (int i=1; i< dlevel(); ++i)
//  //  		lits.push_back( (*_assignment_stack[i])[0] ^ 0x1);
//  //  	    lits.push_back(b);
//  //  	    lits.push_back(a^0x1);
//  //  	    add_clause(lits.begin(), lits.size());
//  //  	    lits.pop_back();