zchaff_probe.cpp

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

//  //  	    lits.pop_back();
//  //  	    lits.push_back(b^0x1);
//  //  	    lits.push_back(a);
//  //  	    add_clause(lits.begin(), lits.size());
//  //  	    }
//  //  	}}
	


//  bool CSolver::get_reason_for_implication(int a, 
//  					 int b, 
//  					 int dl,
//  					 vector<pair<int, int> >& trace, //first ==> literal, second ==> ante
//  					 vector<int>& lits)
//  //if we have a==>b, with the assignment stack at this dlevel in "trace"
//  //find the clause which will have this implication info, the lits will
//  //have a and b in it, and all the other literals (dlevel < dl)
//  //trace should has b in it, and a as the first entry.
//  {
//      assert (_num_marked == 0);
//      assert (trace[0].first == a);
//      //1.first set b to be marked
//      variable(b>>1).set_marked();
//      //2.reverse traverse the assignment stack
//      for (int i=trace.size() - 1; i>0 ; ++i) {
//  	int vid = trace[i].first>>1;	
//  	CVariable & var = variable(vid);
//  	if (!var.is_marked())
//  	    continue;
//  	else {
//  	    var.clear_marked();
//  	    -- _num_marked;
//  	    int ante = trace[i].second;
//  	    for (CLitPoolElement * itr = clause(ante).literals(); (*itr).val() > 0 ; ++ itr) {
//  		int v = (*itr).var_index();
//  		if (v == vid) 
//  		    continue;
//  		else if (variable(v).dlevel()<dl && variable(v).value() != UNKNOWN) {
//  		    if (variable(v).in_new_cl() == -1){ //it's not in the new cl
//  			variable(v).set_in_new_cl((*itr).var_sign());
//  			lits.push_back((*itr).s_var());
//  		    }
//  		}
//  		else{
//  		    assert (variable(v).dlevel()==dl || variable(v).value()== UNKNOWN);
//  		    if (!variable(v).is_marked()) {
//  			variable(v).set_marked();
//  			++ _num_marked;
//  		    }
//  		}
//  	    }
//  	}
//      }
//      //3. should have single marked vars, clean up
//      assert (_num_marked == 1);
//      assert (variable(a>>1).is_marked());    
//      variable(a>>1).clear_marked();
//      -- _num_marked;
//  }

//  int CSolver::do_probe() 
//  {
//      switch(_params.probe_strength) {
//      case 0:
//  	return NO_CONFLICT;
//  	break;
//      case 1:
//  	return probe_n_vars(_params.num_probe_vars);
//  	break;
//      case 2:
//  	probe_vars_level_2();
//  	break;
//      case 3:
//  	probe_vars_level_2();
//  	break;
//      }	
//  }

//  void CSolver::get_cl_lits_from_reason_lits(vector<int> & reason_lits, vector<int> & cl_lits)
//  {
//      for (int k=0, sz1=reason_lits.size(); k< sz1; ++k) {
//  	int vid = reason_lits[k]>>1;
//  	int sign = reason_lits[k] & 0x1;
//  	if (variable(vid).in_new_cl()==-1) {
//  	    cl_lits.push_back(cl_lits);
//  	    variable(vid).set_in_new_cl(sign);
//  	}
//  	else 
//  	    assert(variable(vid).in_new_cl() == sign);
//      }
//      for (int j=0, sz=cl_lits.size()-1; j<sz; ++j)
//  	variable(cl_lits>>1).set_in_new_cl(-1);
//  }

//  int CSolver::probe_n_vars(int num_probes) 
//  {
//      if (num_probes > num_free_variables() )
//  	num_probes = num_free_variables();
	
//      for (int i=_max_score_pos; num_probes >0;  ++i) {
//  	CVariable & var = *_var_order[i].first;
//  	if (var.value()==UNKNOWN) {
//  	    int vidx = _var_order[i].first - variables().begin();
	    
//  	    vector<pair<int,int> > trace_0 = _implication_cache[vidx + vidx];
//  	    assert (trace_0.size() == 0);
//  	    if (probe_one_var(vidx, 0) == CONFLICT)
//  		return CONFLICT;
//  	    get_current_dl_implication_trace(trace_0);
//  	    backtrack(dlevel());

//  	    vector<pair<int,int> > trace_1 = _implication_cache[vidx + vidx + 1];
//  	    assert (trace_1.size() == 0);
//  	    if (probe_one_var(vidx, 1) == CONFLICT)
//  		return CONFLICT;
//  	    get_current_dl_implication_trace(trace_1);
//  	    backtrack(dlevel());
//  	    vector<int> common, temp1;
//  	    for (int j=0, sz=trace_0.size(); j< sz; ++j)
//  		common.push_back(trace_0.first);
//  	    for (int j=0, sz=trace_1.size(); j< sz; ++j)
//  		temp1.push_back(trace_1.first);
//  	    ::sort(common.begin(), common.end());
//  	    get_common(temp1, common);
//  	    if (!common.empty()) {
//  		for (int j=0, sz=common.size(); j< sz; ++j) {
//  		    vector<int> reason_lits;
//  		    int a = vidx + vidx;
//  		    int b = common[j];
//  		    get_reason_for_implication(a, b, dlevel()+1, trace_0, reason_lits);
//  		    int a = vidx + vidx + 1;
//  		    get_reason_for_implication(a, b, dlevel()+1, trace_1, reason_lits);
//  		    vector<int> cl_lits;
//  		    get_cl_lits_from_reason_lits(reason_lits, cl_lits);
//  		    cl_lits.push_back(common[j]);
//  		}
//  		int cl = add_clause(cl_lits.begin(), lits.size());
//  		queue_implication(common[j], cl);
//  	    }
//  	--num_probes;
//  	}
//      }
//      int result = deduce();
//      assert (result != CONFLICT);
//      return NO_CONFLICT;
//  }

//  int CSolver::probe_one_var(int vidx, int phase)
//  {
//      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;
//  }

//  void CSolver::get_current_dl_implication_trace(vector<pair<int, int> > & traces)
//  {
//      int dlevel = dlevel();
//      vector<int> & assign = *_assignment_stack[dlevel];
//      assert (traces.empty());
//      assert (!assign.empty());
//      for (int i=0, sz = assign.size(); i< sz; ++i) {
//  	int svar = assign[i];
//  	int vid = svar>> 1;
//  	traces.push_back(pair<int, int>(svar, variable(vid).get_antecedence()));
//      }
//  }

//  static void get_common(vector<int> & temp1, vector<int> & common) 
//  //will put the common vars of temp1 and common into common, suppose common
//  //is already sorted, in is not
//  {
//      ::sort(temp1.begin(), temp1.end());
//      vector<int> temp2;
//      common.swap(temp2);
//      vector<int>::iterator itr1, itr2;
//      for (itr1=temp1.begin(), itr2= temp2.begin(); itr1 != temp1.end() && itr2 != temp2.end(); ) {
//  	if ( *itr1 < *itr2) 
//  	    ++itr1;
//  	else if (*itr1 > *itr2)
//  	    ++itr2;
//  	else {
//  	    common.push_back(*itr1);
//  	    ++itr1; ++itr2;
//  	}
//      }
//  }
//  int CSolver::simple_justify_one_clause(ClauseIdx cls_idx)
//  //this will not probe free vars in the clause, instead, use the pre-probed trace
//  //must have all free vars probed first.
//  {
//      CClause & cl = clause(cls_idx);
//      vector<int> free_lits;
//      for (int i=0; i< cl.num_lits(); ++i) {
//  	int litvalue = literal_value(cl.literal(i));
//  	if (litvalue==1)
//  	    return; //clause is already sat
//  	else if (litvalue != 0)
//  	    free_lits.push_back(cl.literal(i).s_var());
//      }
//      assert (free_lits.size() > 1);
//      vector<int> common;
//      vector<int> & trace = _implication_cache[free_lits[0]];
//      for (int i=0, sz=trace.size(); i< sz; ++i)
//  	common.push_back(trace[i].first);
//      ::sort(common.begin(), common.end());
//      for (int i=1, sz = free_lits.size(); i< sz; ++i) {
//  	vector<int> temp1;	
//  	vector<int> & trace = _implication_cache[free_lits[i]];
//  	for (int j=0, sz=trace.size(); j< sz; ++j)
//  	    temp1.push_back(trace[j].first);
//  	get_common(temp1, common);
//  	//find the common implications of temp1 and temp2
//  	if (common.empty()) return;
//      }
//      CHECK(cout << "Recursive learning found "; 
//  	  dump_vector(common); 
//  	  cout << endl;);
//      for (int i=0; i< common.size(); ++i) {
//  	vector<int> reason_lits;
//  	for (int j=0; j< num_free_lits; ++j) {
//  	    int a = free_lits[j];
//  	    int b = common[i];
//  	    get_reason_for_implication(a, b, dlevel()+1, _implication_cache[a], reason_lits);
//  	}
//  	vector<int> cl_lits;
//  	get_cl_lits_from_reason_lits(reason_lits, cl_lits);
//  	cl_lits.push_back(common[i]);
//  	int cl = add_clause(cl_lits.begin(), cl_lits.size());
//  	CHECK( detail_dump_cl(cl); cout << endl; );
//  	queue_implication(common[i], cl);
//      }
//      int result = deduce();
//      assert(result != 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());
//      }
//      CHECK(cout << "Justify "; detail_dump_cl(cls_idx); cout <<endl;);

//      int num_free_lits = need_to_probe.size();
//      assert (num_free_lits > 1);
//      //this is used to keep track of the "reasons" when add clause
//      vector<pair<int,int> > implication_trace[num_free_lits];   

//      //1. The first free lit
//      ++ dlevel();
//      queue_implication(need_to_probe[0], 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;
//      //store the trace
//      get_current_dl_implication_trace(implication_trace[0]);
//      //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);
//  	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;
//  	//store the trace
//  	get_current_dl_implication_trace(implication_trace[i]);
//  	//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());
//      CHECK(	cout << "Recursive learning found "; 
//  		dump_vector(common); 
//  		cout << endl;);
//      for (int i=0; i< common.size(); ++i) {
//  	vector<int> reason_lits;
//  	for (int j=0; j< num_free_lits; ++j) {
//  	    int a = need_to_probe[j];
//  	    int b = common[i];
//  	    get_reason_for_implication(a, b, dlevel()+1, implication_trace[j], reason_lits);
//  	}
//  	vector<int> cl_lits;
//  	get_cl_lits_from_reason_lits(reason_lits, cl_lits);
//  	cl_lits.push_back(common[i]);
//  	int cl = add_clause(cl_lits.begin(), cl_lits.size());
//  	CHECK( detail_dump_cl(cl); cout << endl; );
//  	queue_implication(common[i], cl);
//      }
//      int result = deduce();
//      assert(result != CONFLICT);
//      return NO_CONFLICT;
//  }