xchaff_solver.h

Go to the documentation of this file.

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