src/sat/xchaff_solver.h

/* =========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.
*********************************************************************/


#ifndef __SAT_SOLVER__
#define __SAT_SOLVER__

#include <sys/time.h>
#include <sys/resource.h>
#include <stdlib.h>

#include "xchaff_utils.h"
#include "xchaff_dbase.h"

#ifndef __SAT_STATUS__
#define __SAT_STATUS__
enum SAT_StatusT {
    UNDETERMINED,
    UNSATISFIABLE,
    SATISFIABLE,
    TIME_OUT,
    MEM_OUT,
    ABORTED
};
#endif

enum SAT_DeductionT {
    CONFLICT,
    NO_CONFLICT
};

typedef void(*HookFunPtrT)(void *) ;
/**Struct**********************************************************************

  Synopsis    [Sat solver parameters ]

  Description []

  SeeAlso     []

******************************************************************************/
struct CSolverParameters {
    float 	time_limit;

    int 	decision_strategy;
    int 	preprocess_strategy;

    bool 	allow_clause_deletion;
    int	       	clause_deletion_interval;
    int 	max_unrelevance;
    int 	min_num_clause_lits_for_delete;
    int 	max_conflict_clause_length;
    int		bubble_init_step;

    int		verbosity;
    int 	randomness;

    bool	allow_restart;
    float	next_restart_time;
    float	restart_time_increment;
    float	restart_time_incr_incr;
    int 	next_restart_backtrack;
    int 	restart_backtrack_incr;
    int		restart_backtrack_incr_incr;
    int		restart_randomness;
    int		base_randomness;

    bool	back_track_complete;
    int		conflict_analysis_method;
    bool 	allow_multiple_conflict;
    bool 	allow_multiple_conflict_clause;
};
/**Struct**********************************************************************

  Synopsis    [Sat solver statistics ]

  Description []

  SeeAlso     []

******************************************************************************/
struct CSolverStats {
    bool 	is_solver_started;
    int 	outcome;

    bool	is_mem_out;		//this flag will be set if memory out

    long 	start_cpu_time;
    long	last_cpu_time;
    long 	finish_cpu_time;
    long 	start_world_time;
    long 	finish_world_time;

    long  	total_bubble_move;

    int 	num_decisions;
    int		num_backtracks;
    int 	max_dlevel;
    int 	num_implications;
    int 	num_free_variables;
};

/**Class**********************************************************************

  Synopsis    [Sat Solver]

  Description [This class contains the process and datastructrues to solve
               the Sat problem.]

  SeeAlso     []

******************************************************************************/
class CSolver:public CDatabase
{
protected:
    int 			_dlevel;		//current decision elvel
    vector<vector<int> *> 	_assignment_stack;
    queue<pair<int,ClauseIdx> >	_implication_queue;
    CSolverParameters 		_params;
    CSolverStats     		_stats;

    vector<pair<int,pair< HookFunPtrT, int> > > _hooks;

//these are for decision making
    int				_max_score_pos;
    vector<int>			_last_var_lits_count[2];
    vector<pair<int,int> >_var_order;

//these are for conflict analysis
    int 		_num_marked;	//used when constructing conflict clauses
    vector<ClauseIdx> 	_conflicts;	//the conflict clauses
    vector<long> 	_conflict_lits; //used when constructing conflict clauses

//these are for the extended API
    void (*_dlevel_hook)(void *, int);
    int  (*_decision_hook)(void *, bool *);
    void (*_assignment_hook)(void *, int, int);
    void (*_deduction_hook)(void *);
    void *_dlevel_hook_cookie;
    void *_decision_hook_cookie;
    void *_assignment_hook_cookie;
    void *_deduction_hook_cookie;

//needed to support dynamic adding of unit clauses
    vector<ClauseIdx> _addedUnitClauses;

protected:
    void real_solve(void);

    int preprocess(bool allowNewClauses);

    int deduce(void);

    bool decide_next_branch(void);

    int analyze_conflicts(void);
    int conflict_analysis_grasp (void);
    int conflict_analysis_zchaff (void);

    void back_track(int level);

    void init(void);
//for conflict analysis
    void mark_vars_at_level(ClauseIdx cl,
			    int var_idx,
			    int dl);

    int find_max_clause_dlevel(ClauseIdx cl);	//the max dlevel of all the assigned lits in this clause

//for bcp
    void set_var_value(int var,
		       int value,
		       ClauseIdx ante,
		       int dl);
    void set_var_value_not_current_dl(int v,
				      vector<CLitPoolElement *> & neg_ht_clauses);
    void set_var_value_with_current_dl(int v,
				       vector<CLitPoolElement*> & neg_ht_clauses);
    void unset_var_value(int var);

    void run_periodic_functions (void);
//misc functions
    void update_var_stats(void);

    bool time_out(void);

    void delete_unrelevant_clauses(void);
public:
//constructors and destructors
    CSolver() ;
    ~CSolver();
//member access function
    void set_time_limit(float t)
	{ _params.time_limit = t; }
    void set_mem_limit(int s) 	{
	CDatabase::set_mem_limit(s);
    }
    void set_decision_strategy(int s)
	{ _params.decision_strategy = s; }
    void set_preprocess_strategy(int s)
	{ _params.preprocess_strategy = s; }
    void enable_cls_deletion(bool allow)
	{ _params.allow_clause_deletion = allow; }
    void set_cls_del_interval(int n)
	{ _params.clause_deletion_interval = n; }
    void set_max_unrelevance(int n )
	{ _params.max_unrelevance = n; }
    void set_min_num_clause_lits_for_delete(int n)
	{ _params.min_num_clause_lits_for_delete = n; }
    void set_max_conflict_clause_length(int l)
	{ _params.max_conflict_clause_length = l; }
    void set_allow_multiple_conflict( bool b = false) {
	_params.allow_multiple_conflict = b ;
    }
    void set_allow_multiple_conflict_clause( bool b = false) {
	_params.allow_multiple_conflict_clause = b;
    }
    void set_randomness(int n) {
	_params.base_randomness = n;
    }
    void set_random_seed(int seed) {
	if (seed < 0)
	    srand ( current_world_time() );
	else
	    srand (seed);
    }

//these are for the extended API
    void RegisterDLevelHook(void (*f)(void *, int), void *cookie)
         { _dlevel_hook = f; _dlevel_hook_cookie = cookie; }
    void RegisterDecisionHook(int (*f)(void *, bool *), void *cookie)
         { _decision_hook = f; _decision_hook_cookie = cookie; }
    void RegisterAssignmentHook(void (*f)(void *, int, int), void *cookie)
         { _assignment_hook = f; _assignment_hook_cookie = cookie; }
    void RegisterDeductionHook(void (*f)(void *), void *cookie)
         { _deduction_hook = f;
           _deduction_hook_cookie = cookie; }

    int outcome () 	{ return _stats.outcome; }
    int num_decisions() { return _stats.num_decisions; }
    int & num_free_variables() {
	return _stats.num_free_variables;
    }
    int max_dlevel() 	{ return _stats.max_dlevel; }
    int num_implications() { return _stats.num_implications; }
    long total_bubble_move(void) {	return _stats.total_bubble_move; }

    const char * version(void){
	return "Z2001.2.17";
    }

    int current_cpu_time(void) {
	struct rusage ru;
	getrusage(RUSAGE_SELF, &ru);
	return ( ru.ru_utime.tv_sec*1000 +
		 ru.ru_utime.tv_usec/1000+
		 ru.ru_stime.tv_sec*1000 +
		 ru.ru_stime.tv_usec/1000 );
    }

    int current_world_time(void) {
	struct timeval tv;
	struct timezone tz;
	gettimeofday(&tv,&tz);
	return (tv.tv_sec * 1000 + tv.tv_usec/1000) ;
    }

    float elapsed_cpu_time() {
	int current = current_cpu_time();
	int diff = current - _stats.last_cpu_time;
	_stats.last_cpu_time = current;
	return diff/1000.0;
    }

    float total_run_time() {
      if (!_stats.is_solver_started) return 0;
      return (current_cpu_time() -
	      _stats.start_cpu_time)/1000.0 ;
    }

    float cpu_run_time() {
	return (_stats.finish_cpu_time -
		_stats.start_cpu_time)/1000.0 ;
    }

    float world_run_time() {
	return (_stats.finish_world_time -
		_stats.start_world_time) / 1000.0 ;
    }

    int estimate_mem_usage() {
	return CDatabase::estimate_mem_usage();
    }
    int mem_usage(void) {
	int mem_dbase = CDatabase::mem_usage();
	int mem_assignment = 0;
	for (int i=0; i< _stats.max_dlevel; ++i)
	    mem_assignment += _assignment_stack[i]->capacity() * sizeof(int);
	mem_assignment += sizeof(vector<int>)* _assignment_stack.size();
	return mem_dbase + mem_assignment;
    }
    int & dlevel() { return _dlevel; }

//top level function
    void add_hook( HookFunPtrT fun, int interval) {
	pair<HookFunPtrT, int> a(fun, interval);
	_hooks.push_back(pair<int, pair<HookFunPtrT, int> > (0, a));
    }

    void queue_implication (int lit, ClauseIdx ante_clause) {
	CHECK (cout << "\t\t\t\t\t\tQueueing " << (lit&0x01?" -":" +") << (lit>>1) ;
	       cout << " because of  " << ante_clause << endl; );
	_implication_queue.push(pair<int, ClauseIdx>(lit, ante_clause));
    }

    int add_variables(int new_vars);

    ClauseIdx add_clause(vector<long>& lits, bool addConflicts=true);

    void verify_integrity(void);

//    ClauseIdx add_clause_with_order_adjustment(int * lits, int n_lits);
    void restart (void){
	if (_params.verbosity > 1 )
	    cout << "Restarting ... " << endl;
	if (dlevel() > 1) {
	    //clean up the original var_stats.
	    for (unsigned i=1; i<variables().size(); ++i) {
		variable(i).score(0) = 0;
		variable(i).score(1) = 0;
		_last_var_lits_count[0][i] = 0;
		_last_var_lits_count[1][i] = 0;
	    }
	    update_var_stats();
	    back_track(1); //backtrack to level 0. restart.
	}
    }

    int	solve(bool allowNewClauses);
    int continueCheck();

    void dump_assignment_stack(ostream & os = cout);

    void output_current_stats(void);

    void dump(ostream & os = cout ) {
	CDatabase::dump(os);
	dump_assignment_stack(os);
    }
};
#endif