asap_solver.cpp

命题逻辑的求解器,2004年SAT竞赛第一名的求解器

/* =========FOR INTERNAL USE ONLY. NO DISTRIBUTION PLEASE ========== */

/*********************************************************************
 Copyright 2000-2001, 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 "asap_solver.h"

CSolver::CSolver(void)    
{
    dlevel()=0;
    _params.time_limit 		= 3600 * 48;		//2 days
    _params.decision_strategy 	= 0;
    _params.preprocess_strategy = 0;
    _params.allow_clause_deletion 		= true ;
    _params.clause_deletion_interval		= 5000;
    _params.max_unrelevance			= 20;
    _params.min_num_clause_lits_for_delete	= 100;
    _params.max_conflict_clause_length		= 5000;
    _params.bubble_init_step 	= 32;

    _params.randomness		= 0;
    _params.verbosity		= 0;

    _params.back_track_complete	= true;
    _params.allow_multiple_conflict		= false;
    _params.allow_multiple_conflict_clause	= false;

    _params.allow_restart	= true;	
    _params.next_restart_time	= 50;		//this set the first restart time (in seconds)
    _params.restart_time_increment	= 0;
    _params.restart_time_incr_incr = 0;

    _params.next_restart_backtrack= 0;
    _params.restart_backtrack_incr= 40000;		
    _params.restart_backtrack_incr_incr = 100;

    _params.restart_randomness	= 0;	
    _params.base_randomness	= 0;
    _params.randomness		= 0;

    _stats.is_solver_started	= false;
    _stats.outcome		= UNKNOWN;
    _stats.is_mem_out		= false;
    _stats.start_cpu_time	= 0;	   	
    _stats.finish_cpu_time	= 0;
    _stats.last_cpu_time	= 0;	   	

    _stats.start_world_time	= 0;
    _stats.finish_world_time	= 0;

    _stats.num_decisions 	= 0;
    _stats.num_backtracks	= 0;
    _stats.max_dlevel 		= 0;
    _stats.num_implications   	= 0;

    _num_marked 		= 0;
    _dlevel			= 0;		
    _stats.total_bubble_move 	= 0;

}

CSolver::~CSolver()
{
    for (int i=0; i<variables().size(); ++i)
	delete _assignment_stack[i];
}

void CSolver::run_periodic_functions(void)
{
    //a. clause deletion
    if ( _params.allow_clause_deletion &&
	 _stats.num_backtracks % _params.clause_deletion_interval == 0)
  	    delete_unrelevant_clauses(); 
    //b. restart
    if (_params.allow_restart && _stats.num_backtracks > _params.next_restart_backtrack) {
	_params.next_restart_backtrack += _params.restart_backtrack_incr;
	_params.restart_backtrack_incr += _params.restart_backtrack_incr_incr;
  	float current = current_cpu_time()/1000;
  	if (current > _params.next_restart_time) {
  	    if (_params.verbosity > 1) cout << "restart..." << endl;
  	    _params.next_restart_time = current + _params.restart_time_increment;
	    _params.restart_time_increment += _params.restart_time_incr_incr;
	    _params.randomness = _params.restart_randomness;
	    restart();
	}
    }    
    //c. update var stats for decision
    if ((_stats.num_decisions % 0xff)==0) 
	    update_var_stats();
    //d. run hook functions
    for (int 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(void)
{
    CDatabase::init();

    _stats.is_solver_started 	= true;
    _stats.start_cpu_time 	= current_cpu_time();
    _stats.start_world_time	= current_world_time();
    _stats.num_free_variables	= num_variables();
    for (int i=0; i<variables().size(); ++i)
	_assignment_stack.push_back(new vector<int>);

    _var_order.resize( num_variables());
    _last_var_lits_count[0].resize(variables().size());
    _last_var_lits_count[1].resize(variables().size());
    CHECK(dump());
}

void CSolver::set_var_value(int v, int value, ClauseIdx ante, int dl)
{
    assert (value == 0 || value == 1);
    CHECK_FULL(dump());
    CHECK(verify_integrity());
    CHECK (cout << "Setting\t" << (value>0?"+":"-") << v 
	   << " at " << dl << " because " << ante<< endl;);
    ++_stats.num_implications ;
    --num_free_variables();
    CVariable & var = _variables[v];
    assert (var.value() == UNKNOWN);
    var.dlevel() = dl;
    var.value() = value;
    var.set_antecedence(ante);
    vector<CLitPoolElement *> & ht_ptrs = var.ht_ptr(value);
    if (dl == dlevel()) 
	set_var_value_with_current_dl(v, ht_ptrs);
    else 
	set_var_value_not_current_dl(v, ht_ptrs);
}


void CSolver::set_var_value_with_current_dl(int v, vector<CLitPoolElement *> & ht_ptrs)
{
    ClauseIdx cl_idx;
    CLitPoolElement * ht_ptr, * other_ht_ptr, * ptr;
    int dir;
    for (vector <CLitPoolElement *>::iterator itr = ht_ptrs.begin(); itr != ht_ptrs.end(); ++itr) {
	ht_ptr = *itr;
	dir = ht_ptr->direction();
	ptr = ht_ptr;
	while(1) {
	    ptr += dir;
	    if (ptr->val() <= 0) {
		if (dir == 1) 
		    cl_idx = - ptr->val();
		if (dir == ht_ptr->direction()) {
		    ptr = ht_ptr;
		    dir = -dir;
		    continue;
		}
		int the_value = literal_value (*other_ht_ptr);
		if (the_value == 0) //a conflict
		    _conflicts.push_back(cl_idx);
		else if ( the_value != 1) //e.g. unknown
		    queue_implication (other_ht_ptr->s_var(), cl_idx);
		break;
	    }
	    if (ptr->is_ht()) {
		other_ht_ptr = ptr;
		continue;
	    }
	    if (literal_value(*ptr) == 0) 
		continue;
	    //now it's value is either 1 or unknown
	    int v1 = ptr->var_index();
	    int sign = ptr->var_sign();
	    variable(v1).ht_ptr(sign).push_back(ptr);
	    ht_ptr->unset_ht();
	    ptr->set_ht(dir);

	    *itr = ht_ptrs.back();
	    ht_ptrs.pop_back();
	    --itr;
	    break;
	}
    }
}

void CSolver::set_var_value_not_current_dl(int v, vector<CLitPoolElement *> & ht_ptrs)
{
    ClauseIdx cl_idx;
    CLitPoolElement * ht_ptr, * other_ht_ptr, * ptr, * max_ptr = NULL;
    int dir,max_dl;

    for (vector <CLitPoolElement *>::iterator itr = ht_ptrs.begin(); 
	 itr != ht_ptrs.end(); ++itr) {
	max_dl = -1;
	ht_ptr = *itr;
	dir = ht_ptr->direction();
	ptr = ht_ptr;
	while(1) {
	    ptr += dir;
	    if (ptr->val() <= 0) {
		if (dir == 1) 
		    cl_idx = - ptr->val();
		if (dir == ht_ptr->direction()) {
		    ptr = ht_ptr;
		    dir = -dir;
		    continue;
		}
		if (variable(ht_ptr->var_index()).dlevel() < max_dl) {
		    int v1 = max_ptr->var_index();
		    int sign = max_ptr->var_sign();
		    variable(v1).ht_ptr(sign).push_back(max_ptr);
		    ht_ptr->unset_ht();
		    max_ptr->set_ht(dir);
		    *itr = ht_ptrs.back();
		    ht_ptrs.pop_back();
		    --itr;
		}
		int the_value = literal_value (*other_ht_ptr);
		if (the_value == 0) //a conflict
		    _conflicts.push_back(cl_idx);
		else if ( the_value != 1) //e.g. unknown
		    queue_implication (other_ht_ptr->s_var(), cl_idx);
		break;
	    }
	    if (ptr->is_ht()) {
		other_ht_ptr = ptr;
		continue;
	    }
	    if (literal_value(*ptr) == 0) {
		if (variable(ptr->var_index()).dlevel() > max_dl) {
		    max_dl = variable(ptr->var_index()).dlevel();
		    max_ptr = ptr;
		}
		continue;
	    }
	    //now it's value is either 1 or unknown
	    int v1 = ptr->var_index();
	    int sign = ptr->var_sign();
	    variable(v1).ht_ptr(sign).push_back(ptr);
	    ht_ptr->unset_ht();
	    ptr->set_ht(dir);

	    *itr = ht_ptrs.back();
	    ht_ptrs.pop_back();
	    --itr;
	    break;
	}
    }
}

void CSolver::unset_var_value(int v)
{
    CHECK(cout <<"Unset var " << (variable(v).value()?"+":"-") << v << endl;);
    CVariable & var = variable(v);
    if (var.var_score_pos() < _max_score_pos)
	_max_score_pos = var.var_score_pos();
    var.value() = UNKNOWN;
    var.set_antecedence(NULL_CLAUSE);
    var.dlevel() = -1;
}

int CSolver::find_max_clause_dlevel(ClauseIdx cl)
{
//if cl has single literal, then dlevel should be 0 
    int max_level = 0;
    if (cl == NULL_CLAUSE || cl == FLIPPED) 
	return dlevel();
    for (int i=0, sz= clause(cl).num_lits(); i<sz;  ++i) {
	int var_idx =((clause(cl).literals())[i]).var_index();
	if (_variables[var_idx].value() != UNKNOWN) {
	    if (max_level < _variables[var_idx].dlevel())
		max_level =  _variables[var_idx].dlevel();
	}
    }
    return max_level; 
}

void CSolver::dump_assignment_stack(ostream & os = cout) {
    cout << "Assignment Stack:  ";
    for (int i=0; i<= dlevel(); ++i) {
	if ((*_assignment_stack[i]).size() > 0)
	if (variable( (*_assignment_stack[i])[0]>>1).get_antecedence()==FLIPPED)
	    cout << "*" ;
	cout << "(" <<i << ":";
	for (int j=0; j<(*_assignment_stack[i]).size(); ++j )
	    cout << ((*_assignment_stack[i])[j]&0x1?"-":"+")
		 << ((*_assignment_stack[i])[j] >> 1) << " ";
	cout << ") " << endl;
    }
    cout << endl;
}


bool CDatabase::is_conflict(ClauseIdx cl)
{
    CLitPoolElement * lits = clause(cl).literals();
    for (int i=0, sz= clause(cl).num_lits(); i<sz;  ++i)
	if (literal_value(lits[i]) != 0)
		return false;
    return true;
}

bool CDatabase::is_satisfied(ClauseIdx cl)
{
    CLitPoolElement * lits = clause(cl).literals();
    for (int i=0, sz= clause(cl).num_lits(); i<sz; ++i) 
	if (literal_value(lits[i]) == 1) 
	    return true;
    return false;
}

int CDatabase::find_unit_literal(ClauseIdx cl) 
{
//if it's not unit, return 0.
    int unassigned = 0;
    for (int i=0, sz= clause(cl).num_lits(); i<sz;  ++i) {
	int var_idx =((clause(cl).literals())[i]).var_index();
	if (_variables[var_idx].value() == UNKNOWN) {
	    if (unassigned == 0) 
		unassigned = clause(cl).literals()[i].s_var();
	    else //more than one unassigned
		return 0;
	}
    }
    return unassigned;
}

void CSolver::delete_unrelevant_clauses(void) 
{
    CHECK_FULL (dump());
    int original_num_deleted = num_deleted_clauses();
    int original_del_lits = num_deleted_literals();
    if (CDatabase::_stats.mem_used_up) {
	CDatabase::_stats.mem_used_up = false;
	if (++CDatabase::_stats.mem_used_up_counts < 5) {
	    _params.max_unrelevance = (int) (_params.max_unrelevance * 0.8);
	    if (_params.max_unrelevance < 4)
		_params.max_unrelevance = 4;
	    _params.min_num_clause_lits_for_delete = (int) (_params.min_num_clause_lits_for_delete* 0.8);
	    if (_params.min_num_clause_lits_for_delete < 10)
		_params.min_num_clause_lits_for_delete = 10;
	    _params.max_conflict_clause_length = (int) (_params.max_conflict_clause_length*0.8);
	    if (_params.max_conflict_clause_length < 50 )
		_params.max_conflict_clause_length = 50;
	    CHECK(
	    cout << "Forced to reduce unrelevance in clause deletion. " << endl;
	    cout <<"MaxUnrel: " << _params.max_unrelevance 
		 << "  MinLenDel: " << _params.min_num_clause_lits_for_delete
		 << "  MaxLenCL : " << _params.max_conflict_clause_length << endl;
		);
	}
    }
    //first find out the clause to delete and mark them
    for (vector<CClause>::iterator itr = clauses().begin() + init_num_clauses(); 
	 itr != clauses().end(); ++itr) {
	CClause & cl = * itr;
	CLitPoolElement * lits = cl.literals();
	if (!cl.in_use() || cl.num_lits() < _params.min_num_clause_lits_for_delete ) continue;
	int val_0_lits = 0, val_1_lits = 0, unknown_lits = 0;
	for (int i=0; i< cl.num_lits(); ++i) {
	    int lit_value = literal_value (cl.literal(i));
  	    if (lit_value == 0 ) ++val_0_lits;
  	    else if (lit_value == 1) ++val_1_lits;
  	    else ++unknown_lits;
	    if (unknown_lits + val_1_lits > _params.max_unrelevance) {
		mark_clause_deleted(cl);
		_unused_clause_idx_queue.push(itr - clauses().begin());
		CHECK (cout << "Deleting Unrelevant clause: " << cl << endl;);
		break;
	    }
	    if (cl.num_lits() > _params.max_conflict_clause_length && 
		(unknown_lits+val_1_lits > 1) ) { //to make sure it's not generating an implication
		                                  //and it's not an antecedence for other var assignment
		mark_clause_deleted(cl);
		CHECK (cout << "Deleting too large clause: " << cl << endl;);
		_unused_clause_idx_queue.push(itr - clauses().begin());
		break;
	    }
	}