zchaff_probe.cpp

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

/*********************************************************************
 Copyright 2000-2004, Princeton University.  All rights reserved. 
 By using this software the USER indicates that he or she has read, 
 understood and will comply with the following:

 --- Princeton University hereby grants USER nonexclusive permission 
 to use, copy and/or modify this software for internal, noncommercial,
 research purposes only. Any distribution, including commercial sale 
 or license, of this software, copies of the software, its associated 
 documentation and/or modifications of either is strictly prohibited 
 without the prior consent of Princeton University.  Title to copyright
 to this software and its associated documentation shall at all times 
 remain with Princeton University.  Appropriate copyright notice shall 
 be placed on all software copies, and a complete copy of this notice 
 shall be included in all copies of the associated documentation.  
 No right is  granted to use in advertising, publicity or otherwise 
 any trademark, service mark, or the name of Princeton University. 


 --- This software and any associated documentation is provided "as is" 

 PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS 
 OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A 
 PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR 
 ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, 
 TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.  

 Princeton University shall not be liable under any circumstances for 
 any direct, indirect, special, incidental, or consequential damages 
 with respect to any claim by USER or any third party on account of 
 or arising from the use, or inability to use, this software or its 
 associated documentation, even if Princeton University has been advised
 of the possibility of those damages.
*********************************************************************/
#include <hash_set>
#include "zchaff_solver.h"

struct pair_int_equal {
    bool operator () (pair<int,int> a, pair<int,int> b) const {
	return (a.first==b.first && a.second == b.second);
    }
};

struct pair_int_comp {
    bool operator () (pair<int,int> a, pair<int,int> b) const {
	if (a.first < b.first) 
	    return true;
	else if (a.first == b.first && a.second < b.second)
	    return true;
	return false;
    }
};

struct pair_int_hash_fun {
    size_t operator () (const pair<int, int> a) const {
	return (a.first + (a.second << 16));
    }
};


typedef hash_set<pair<int,int>, pair_int_hash_fun, pair_int_equal> PairHash;

inline static void hash_insert( PairHash & table,
		int a, int b)
{
    table.insert(pair<int,int> (a, b));
}

inline static void hash_remove(PairHash & table,
		int a, int b)
{
    table.erase(pair<int,int> (a, b));
}

inline static bool hash_contain(PairHash & table,
		int a, int b)
{
    return (table.find(pair<int,int>(a,b))) != table.end();
}

static void dump_vector(vector<int> & list) {
    for (int i=0; i< list.size(); ++i)
	cout << list[i] << "  ";
    cout << endl;
}

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::add_probe_clause(vector<int> lits)
{
    int cl = add_clause(lits.begin(), lits.size(), VOLATILE_GID);
    clause(cl).status() = PROBE_CL;
}

int CSolver::do_deduction(void)
//after make a implication, try to go to
//a state which is consistant. So, the dlevel
//will remain the same if no conflict occured
//else it will be smaller than current.
{
    while (deduce() == CONFLICT) {
	if (analyze_conflicts() < 0)
	    break;
    }
    return dlevel();
}


int CSolver::simplify(void)
{
    vector<pair<int,int> > equiv_svar_pair;
    assert(dlevel() == 0);
    bool modified = true;
//      while (modified) {
//  	modified = false;
	if (probe(equiv_svar_pair, modified)==CONFLICT)
	    return CONFLICT;
	if (!equiv_svar_pair.empty()) {
	    modified = true;
	    make_equivalent(equiv_svar_pair);
	}
//    }
    return NO_CONFLICT;
}

void CSolver::make_equivalent(vector<pair<int, int> > & equiv)
{
//      if (equiv.size() == 0) return;
//      vector<vector<int> * > equ_class;
//      hash_map<int, int> var_to_class;
//      //1.initially, everything map to itself.
//      for(int i=0; i< variables().size(); ++i) {
//  	equ_clause.push_back(new vector<int>);
//  	equ_clauss.back().push_back(i+i);
//  	var_to_class[i] = i+i;	
//      }
//      //2. make equivalent
//      for (int i=0; i< equiv.size(); ++ i) {
//  	int a = equiv[i].first;
//  	int b = equiv[i].second;
//  	int va = a >>1;
//  	int sa = a & 0x1;
//  	int vb = b >>1;
//  	int sb = b & 0x1;
//  	int eq_a = var_to_class[a >> 1];
//  	int eq_b = var_to_class[b >> 1];
//  	if ((eq_a>>a) == (eq_b>>1)) {
//  	    int signa = (eq_a & 0x1) ^ sa;
//  	    int singb = (eq_b & 0x1) ^ sb;
//  		assert (signa == singb);
//  	}
//  	else {
//  	    int s = (eq_a & 0x1)^(eq_b & 0x1)^sa^sb ;
//  	    vector<int> & class_a = *equ_class[eq_a>>1];
//  	    vector<int> & class_b = *equ_class[eq_b>>1];
//  	    assert (class_a.size() > 0);
//  	    assert (class_b.size() > 0);
//  	    for (int j=0; j< class_b.size(); ++j) {
//  		int m = class_b[j];
//  		assert (var_to_class[m>>1] == (eq_b >> 1));
//  		var_to_class[m>>1] == eq_a ^ s ^ (m & 0x1);
//  		class_a.push_back(m ^ s);
//  	    }
//  	    class_b.clear();
//  	}
//      }
    //3. update var map
    equiv.clear();
}

void CSolver::get_rl_candidate(vector<vector<ClauseIdx> > * candidate)
{
    candidate[0].resize(variables().size());
    candidate[1].resize(variables().size());
    if (_params.preprocess.do_recursive_learning) {
	for (int i=0; i< clauses().size(); ++i) {
	    if (clause(i).status() == DELETED_CL || clause(i).status() == PROBE_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) {
		int lit_value = literal_value(cl.literal(j));
		if (lit_value ==0)
		    continue;
		else if (lit_value==1)
		    break;
		else
		    ++ free_lits;
	    }
	    if (j < num_lits || //i.e. break occured, clause SAT
		free_lits > _params.preprocess.max_rl_length)
		continue;
	    assert (free_lits > 1);
	    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);
		}
	    }
	}
    }
}

int CSolver::probe(vector<pair<int,int> > & equiv_svar_pair, bool & modified) 
{
    assert (dlevel() == 0);

    //use candidate to store the candidate clause for recursive learning
    vector<vector<ClauseIdx> > candidate[2];
    get_rl_candidate( candidate);
    //implication table store relationship a=>b. We need a < b; 
    PairHash implication_table;
    //put all the decision variables into "lits", this is a reason 
    //for the implications, though may not be the best one.
    vector<int> lits;
    for (int i=1; i<= dlevel(); ++i) 
	lits.push_back((*_assignment_stack[i])[0] ^ 0x1);
    //now do the real probing
    for (int i=1; i<= num_variables(); ++i) {
	if (variable(i).value() != UNKNOWN)
	    continue;
	DBG0(cout << "Probing VID : " << i << endl;);
	for (int phase = 0; phase < 2; ++phase) {
	    int svar = i + i + phase;
	    ++dlevel();
	    int dl = dlevel();
	    queue_implication(svar, NULL_CLAUSE);
	    vector<ClauseIdx> & rl_candidates = candidate[!phase][i];	
	    DBG0(  cout << "Probe " << i << " with value " << !phase << endl; );
	    probe_one_variable_assignment(rl_candidates);
	    if (dlevel() != dl) //that means some conflict happened inside, 
		if (dlevel() == -1) 
		    return CONFLICT;	
		else{
		    modified = true;
		    break;
		}
	    //dlevel() == dl, so the assigmentstack has all the implications;
	    vector<int> & assign = *_assignment_stack[dlevel()];
	    assert(assign[0] == svar);
	    for (int j=1, sz = assign.size(); j< sz; ++j) {
		int a, b;
		int v = assign[j]>> 1;
		int sign = assign[j]&0x1;
		if (v > i) {
		    a = svar;
		    b = assign[j] ;
		}
		else {
		    a = assign[j] ^ 0x1;
		    b = svar ^ 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;);
			//here only add an "artificial" clause because we know it's dlevel 0, 
			//and this must be true globaly in the general case, we need to add 
			//"reasons" for this, it's pretty expensive though.
			lits.push_back( b);
			int cl = add_probe_clause(lits);
			queue_implication(b, cl);
			lits.pop_back();
		    }
		    else if (hash_contain(implication_table, a, b^0x1)) {
			DBG0(cout << "Probe infered " << (a^0x1)  << " must be true " << endl;);
			lits.push_back( a^0x1);
			int cl = add_probe_clause(lits);
			queue_implication(a^0x1, cl);
			lits.pop_back();
		    }
		    else if (hash_contain(implication_table, a^0x1, b^0x1)) {
			//because a < b, always b being represented by a. 
			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;);
		    }
		}
	    }
	    back_track(dl);
	    if (!_implication_queue.empty()) {
		modified = true;
		do_deduction();
		assert (dlevel() == 0); //we know there should be no conflict
	    }
	}
    }
    return NO_CONFLICT;
}

int CSolver::probe_one_variable_assignment( vector<ClauseIdx>& cls)
{
    assert (dlevel() == 1);
    int dl = dlevel();
    do_deduction();
    if (dl != dlevel())
	return CONFLICT;
    if (_params.preprocess.do_recursive_learning) {
	for (int i=0; i<cls.size(); ++i) {
	    justify_one_clause(cls[i]);
	    if (dlevel() != dl) 
		return CONFLICT;
	}