zchaff_solver.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 <cstdio>
#include <cmath>
#include <algorithm>
#include <fstream>
#include "zchaff_solver.h"
//typedef double DOUBLE;
//  extern "C" DOUBLE PLED_FindMaxFlow(int nvtxs, int nedges,
//  				   int *edge_from, int *edge_to, 
//  				   DOUBLE *ewts, int *part);

#define VERIFY_ON

#ifdef VERIFY_ON
ofstream verify_out("resolve_trace");
#endif

void CSolver::re_init_stats(void)
{
    _stats.is_mem_out		= false;
    _stats.outcome		= UNDETERMINED;

    _stats.next_restart 	= _params.restart.first_restart;
    _stats.restart_incr 	= _params.restart.backtrack_incr;
    _stats.next_cls_deletion 	= _params.cls_deletion.interval;
    _stats.next_var_score_decay = _params.decision.decay_period;

    _stats.current_randomness 	= _params.decision.base_randomness;

    _stats.total_bubble_move 	= 0;
    _stats.num_decisions 	= 0;
    _stats.num_decisions_stack_conf	= 0;
    _stats.num_decisions_vsids	= 0;
    _stats.num_decisions_shrinking=0;
    _stats.restarts_since_vsids	= 0;
    _stats.num_backtracks	= 0;
    _stats.max_dlevel 			= 0;
    _stats.num_implications   		= 0;
    _stats.num_restarts			= 0;
    _stats.num_del_orig_cls		= 0;
    _stats.num_shrinkings               = 0;
    _stats.start_cpu_time	= get_cpu_time();
    _stats.finish_cpu_time	= 0;
    _stats.random_seed		= 0;
    _stats.sum_sizes_iter = 0;
    _stats.sum_squares_iter =0;
    _stats.num_conf_cls_iter =0;
}

void CSolver::init_stats(void) 
{
    re_init_stats();

    _stats.been_reset		= true;
    _stats.outcome 		= UNDETERMINED;

    _stats.num_free_variables 	= 0;
    _stats.num_free_branch_vars = 0;
}

void CSolver::init_parameters(void)
{
    _params.verbosity				= 0;
    _params.time_limit				= 3600 * 48;
    _params.shrinking.size                      = 95;
    _params.shrinking.enable                    = true;

    _params.decision.strategy 			= 0;
    _params.decision.restart_randomness		= 0;	
    _params.decision.base_randomness		= 0;
    _params.decision.decay_period		= 40; 
    _params.decision.bubble_init_step 		= 0x400;

    _params.cls_deletion.enable 		= true ;
    _params.cls_deletion.head_activity          = 500;//250;//60
    _params.cls_deletion.tail_activity          = 10;//35;//7
    _params.cls_deletion.head_num_lits          = 6;//6;//8
    _params.cls_deletion.tail_num_lits          = 45;//45;//42
    _params.cls_deletion.tail_vs_head           = 16;
    _params.cls_deletion.interval	        = 600;
    

    _params.restart.enable			= true;
    _params.restart.interval			= 700;
    _params.restart.first_restart		= 10*_params.restart.interval;
    _params.restart.backtrack_incr		= _params.restart.interval;
    _params.restart.backtrack_incr_incr 	= 0;
}

CSolver::CSolver(void) {
    init_parameters();
    init_stats();
    _dlevel			= 0;		
    _force_terminate		= false;
    _implication_id		= 0;
    _num_marked			= 0;
    _num_in_new_cl		= 0;
    _outside_constraint_hook	= NULL;
    _sat_hook	                = NULL;
}

CSolver::~CSolver()
{
    while (!_assignment_stack.empty()) {
	delete _assignment_stack.back();
	_assignment_stack.pop_back();
    }
}

void CSolver::set_time_limit(float t) 
{ 
    _params.time_limit = t; 
}

float CSolver::elapsed_cpu_time(void) 
{
    return get_cpu_time() - _stats.start_cpu_time;
}

float CSolver::cpu_run_time() 
{ 
    return (_stats.finish_cpu_time - _stats.start_cpu_time);
}

void CSolver::set_variable_number(int n) 
{
    assert (num_variables() == 0);
    CDatabase::set_variable_number(n);
    _stats.num_free_variables	= num_variables();
    while (_assignment_stack.size() <= num_variables())
	_assignment_stack.push_back(new vector<int>);
    assert (_assignment_stack.size() == num_variables() + 1);
}

int CSolver::add_variable(void) 
{
    int num = CDatabase::add_variable();
    ++_stats.num_free_variables;
    while (_assignment_stack.size() <= num_variables())
	_assignment_stack.push_back(new vector<int>);
    assert (_assignment_stack.size() == num_variables() + 1);
    return num;
}

void CSolver::set_mem_limit(int s)
{ 
    CDatabase::set_mem_limit(s); 
}

void CSolver::set_decision_strategy(int s) 
{
    _params.decision.strategy = s; 
}

void CSolver::set_randomness(int n) 
{
    _params.decision.base_randomness = n; 
}

void CSolver::set_random_seed(int seed) {
    srand (seed);
}

void CSolver::enable_cls_deletion(bool allow) {
    _params.cls_deletion.enable=allow;
}

void CSolver::add_hook( HookFunPtrT fun, int interval) 
{
    pair<HookFunPtrT, int> a(fun, interval);
    _hooks.push_back(pair<int, pair<HookFunPtrT, int> > (0, a));
}

void CSolver::run_periodic_functions(void)
{
    //a. restart
    if (_params.restart.enable && _stats.num_backtracks > _stats.next_restart && _shrinking_cls.empty()) {
        _stats.next_restart = _stats.num_backtracks + _stats.restart_incr;
	delete_unrelevant_clauses();
        if(_stats.num_restarts%5==1)     
            compact_lit_pool();
	restart(); 
        cout<<"\rDecision: "<<_assignment_stack[0]->size()<<"/"<<num_variables();
        cout<<"\tTime: "<<get_cpu_time()-_stats.start_cpu_time<<"/"<<_params.time_limit<<flush;
    }
    //b. decay variable score	         
    if (_stats.num_backtracks > _stats.next_var_score_decay) {
	_stats.next_var_score_decay = _stats.num_backtracks + _params.decision.decay_period;
	decay_variable_score();
    }
    //d. run hook functions
    for (unsigned i=0; i< _hooks.size(); ++i) {
	pair<int,pair<HookFunPtrT, int> > & hook = _hooks[i];
	if (_stats.num_decisions >= hook.first) {
	    hook.first += hook.second.second;
	    hook.second.first((void *) this);
	}
    }
} 
    

void CSolver::init_solve(void)
{
    CDatabase::init_stats();
    re_init_stats();
    _stats.been_reset 		= false;

    assert (_conflicts.empty());
    assert (_conflict_lits.empty());
    assert (_num_marked == 0);
    assert (_num_in_new_cl == 0);
    assert (_dlevel == 0);
	
    for (unsigned i=0, sz = variables().size(); i< sz; ++i) {
	variable(i).score(0) = variable(i).lits_count(0);
	variable(i).score(1) = variable(i).lits_count(1);
    }

    _ordered_vars.resize( num_variables());
    update_var_score();
    int seed = 0;//time(NULL);
    //seed=1066564017;
    if(_stats.random_seed==0)
	_stats.random_seed=seed;
    else
	seed=_stats.random_seed;
    srand(seed);
    top_unsat_cls=clauses().end();
    top_unsat_cls--;
    _shrinking_benefit=0;
    _shrinking_cls.clear();
    _shrinking_conf_cls_length=0;
    DBG2(dump());
}

void CSolver::set_var_value(int v, int value, ClauseIdx ante, int dl)
{
    assert (value == 0 || value == 1);
    DBG2(dump());
    CHECK(verify_integrity());
    DBG1 (cout << "Setting\t" << (value>0?"+":"-") << v 
	  << " at " << dlevel() << " because " << ante<< endl;);
    CVariable & var = variable(v);
    assert (var.value() == UNKNOWN);
    var.set_dlevel(dl);
    var.set_value(value);
    var.antecedent() = ante;
    var.assgn_stack_pos() = _assignment_stack[dl]->size();
    _assignment_stack[dl]->push_back(v*2+!value);

    if (dl == dlevel())
	set_var_value_current_dl(v, value);
    else 
	set_var_value_not_current_dl(v, value);
	
    ++_stats.num_implications ;
    if (var.is_branchable()) 
	--num_free_variables();
}

void CSolver::set_var_value_current_dl(int v, int value)
{
    vector<CLitPoolElement *> & watchs = variable(v).watched(value);
    for (vector <CLitPoolElement *>::iterator itr = watchs.begin(); itr != watchs.end(); ++itr) {
	ClauseIdx cl_idx;
	CLitPoolElement * other_watched = *itr;
	CLitPoolElement * watched = *itr;
	int dir = watched->direction();
	CLitPoolElement * ptr = watched;
	while(1) {
	    ptr += dir;
	    if (ptr->val() <= 0) { //reached one end of the clause
		if (dir == 1) 	//reached the right end, i.e. spacing element is the cl_id
		    cl_idx = ptr->get_clause_index();
		if (dir == watched->direction()) { //we haven't go both directions.
		    ptr = watched;	
		    dir = -dir;			//change direction, go the other way
		    continue;
		}
                //otherwise, we have already go through the whole clause
		int the_value = literal_value (*other_watched);
		if (the_value == 0) //a conflict
		    _conflicts.push_back(cl_idx);
		else if ( the_value != 1) //i.e. unknown
		    queue_implication (other_watched->s_var(), cl_idx, dlevel());
		break;
	    }
	    if (ptr->is_watched()) {	//literal is the other watched lit, skip it.
		other_watched = ptr;
		continue;
	    }
	    if (literal_value(*ptr) == 0) // literal value is 0, keep going
		continue;
	    //now the literal's value is either 1 or unknown, watch it instead
	    int v1 = ptr->var_index();
	    int sign = ptr->var_sign();
	    variable(v1).watched(sign).push_back(ptr);
	    ptr->set_watch(dir);
	    //remove the original watched literal from watched list
	    watched->unwatch();
	    *itr = watchs.back(); //copy the last element in it's place
	    watchs.pop_back();	//remove the last element
	    --itr;		//do this so with don't skip one during traversal
	    break;
	}
    }
}

void CSolver::set_var_value_not_current_dl(int v, int value)
{
//the only difference between this one and the last function
//is that because the assignment var is not at current_dl, 
//(that means, < current_dl), it's possible some variable 
//have a dlevel higher than the assigned one. So, we need 
//to make sure that watched literal has the highest dlevel if
//we can't find other unassigned or value 1 literals
//also, it's possible we need to readjust decision levels of 
//some variables implied.
    ClauseIdx cl_idx;
    CLitPoolElement * watched, * other_watched, * ptr, * max_ptr = NULL;
    int dir,max_dl;
    vector<CLitPoolElement *> & watchs = variable(v).watched(value);
    for (vector <CLitPoolElement *>::iterator itr = watchs.begin(); 
	 itr != watchs.end(); ++itr) {
	max_dl = -1;
	watched = *itr;
	dir = watched->direction();
	ptr = watched;
	while(1) {
	    ptr += dir;
	    if (ptr->val() <= 0) {
		if (dir == 1) 
		    cl_idx = ptr->get_clause_index();
		if (dir == watched->direction()) {
		    ptr = watched;
		    dir = -dir;
		    continue;
		}
		CLitPoolElement * current_watched = watched;
		if (variable(watched->var_index()).dlevel() < max_dl) {
		    int v1 = max_ptr->var_index();
		    int sign = max_ptr->var_sign();
		    variable(v1).watched(sign).push_back(max_ptr);
		    max_ptr->set_watch(dir);
		    watched->unwatch();
		    *itr = watchs.back();
		    watchs.pop_back();
		    --itr;
		    current_watched = max_ptr;
		}
		int max = variable(current_watched->var_index()).dlevel();
		int the_value = literal_value (*other_watched);
		if (the_value == 0) {
		    //it's a conflict, but we will not put into _conflicts
		    //instead, make it a implication so it will be resolved 
		    //in deduce()
		    assert (variable(other_watched->var_index()).dlevel() >= max);
//  		    cout << "Queueing Conflict for " << other_watched->var_index() << " orig DL: " 
//  			 << variable(other_watched->var_index()).dlevel() << " current DL: " 
//  			 << max << endl;
		    queue_implication(other_watched->s_var(), cl_idx, max);
		}
		else if ( the_value == 1) {
		    int v1 = other_watched->var_index();
		    if (variable(v1).dlevel() > max)
			queue_implication(other_watched->s_var(), cl_idx, max);
		}
		else 
		    queue_implication (other_watched->s_var(), cl_idx, max);