zchaff64/zchaff_solver.h

   1 // *********************************************************************
   2 // Copyright 2000-2004, Princeton University.  All rights reserved.
   3 // By using this software the USER indicates that he or she has read,
   4 // understood and will comply with the following:
   5 //
   6 // --- Princeton University hereby grants USER nonexclusive permission
   7 // to use, copy and/or modify this software for internal, noncommercial,
   8 // research purposes only. Any distribution, including commercial sale
   9 // or license, of this software, copies of the software, its associated
  10 // documentation and/or modifications of either is strictly prohibited
  11 // without the prior consent of Princeton University.  Title to copyright
  12 // to this software and its associated documentation shall at all times
  13 // remain with Princeton University.  Appropriate copyright notice shall
  14 // be placed on all software copies, and a complete copy of this notice
  15 // shall be included in all copies of the associated documentation.
  16 // No right is  granted to use in advertising, publicity or otherwise
  17 // any trademark,  service mark, or the name of Princeton University.
  18 //
  19 //
  20 // --- This software and any associated documentation is provided "as is"
  21 //
  22 // PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
  23 // OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
  24 // PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR
  25 // ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
  26 // TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
  27 //
  28 // Princeton University shall not be liable under any circumstances for
  29 // any direct, indirect, special, incidental, or consequential damages
  30 // with respect to any claim by USER or any third party on account of
  31 // or arising from the use, or inability to use, this software or its
  32 // associated documentation, even if Princeton University has been advised
  33 // of the possibility of those damages.
  34 // *********************************************************************
  35
  36 #ifndef __SAT_SOLVER__
  37 #define __SAT_SOLVER__
  38
  39 #include "zchaff_version.h"
  40 #include "zchaff_dbase.h"
  41
  42 #ifndef _SAT_STATUS_
  43 #define _SAT_STATUS_
  44
  45 enum SAT_StatusT {
  46   UNDETERMINED,
  47   UNSATISFIABLE,
  48   SATISFIABLE,
  49   TIME_OUT,
  50   MEM_OUT,
  51   ABORTED
  52 };
  53 #endif
  54
  55 enum SAT_DeductionT {
  56   CONFLICT,
  57   NO_CONFLICT
  58 };
  59
  60 class CSolver;
  61
  62 typedef void(*HookFunPtrT)(void *) ;
  63 typedef void(*OutsideConstraintHookPtrT)(CSolver * solver);
  64 typedef bool(*SatHookPtrT)(CSolver * solver);
  65
  66 // **Struct********************************************************************
  67 //
  68 //  Synopsis    [Sat solver parameters ]
  69 //
  70 //  Description []
  71 //
  72 //  SeeAlso     []
  73 //
  74 // ****************************************************************************
  75
  76 struct CSolverParameters {
  77   float         time_limit;
  78   int           verbosity;
  79
  80   struct {
  81     unsigned    size;
  82     int         enable;
  83     int         upper_bound;
  84     int         lower_bound;
  85     int         upper_delta;
  86     int         lower_delta;
  87     int         bound_update_frequency;
  88     unsigned    window_width;
  89   } shrinking;
  90
  91   struct {
  92     int         base_randomness;
  93     int         bubble_init_step;
  94     int         decay_period;
  95   } decision;
  96
  97   struct {
  98     bool        enable;
  99     unsigned    interval;
 100     unsigned    head_activity;
 101     unsigned    tail_activity;
 102     unsigned    head_num_lits;
 103     unsigned    tail_num_lits;
 104     int         tail_vs_head;
 105   } cls_deletion;
 106
 107   struct {
 108     bool        enable;
 109     int         interval;
 110     int         first_restart;
 111     int         backtrack_incr;
 112   } restart;
 113 };
 114
 115 // **Struct********************************************************************
 116 //
 117 //  Synopsis    [Sat solver statistics ]
 118 //
 119 // Description []
 120 //
 121 //  SeeAlso     []
 122 //
 123 // ****************************************************************************
 124
 125 struct CSolverStats {
 126   bool          been_reset;  // when delete clause in incremental solving,
 127                              // must reset.
 128   SAT_StatusT   outcome;
 129   bool          is_mem_out;  // this flag will be set if memory out
 130   double        start_cpu_time;
 131   double        finish_cpu_time;
 132   int           current_randomness;
 133   int           next_restart;
 134   int           restart_incr;
 135   int           next_cls_deletion;
 136   int           next_var_score_decay;
 137   int           num_free_variables;
 138   int           num_free_branch_vars;
 139   long64        total_bubble_move;
 140   int           num_decisions;
 141   int           num_decisions_stack_conf;
 142   int           num_decisions_vsids;
 143   int           num_decisions_shrinking;
 144   int           num_shrinkings;
 145   int           shrinking_benefit;
 146   int           shrinking_cls_length;
 147   int           num_backtracks;
 148   int           max_dlevel;
 149   int           random_seed;
 150   long64        num_implications;
 151   int           num_restarts;
 152   int           num_del_orig_cls;
 153 };
 154
 155 // **Class*********************************************************************
 156 //
 157 //  Synopsis    [Sat Solver]
 158 //
 159 //  Description [This class contains the process and datastructrues to solve
 160 //               the Sat problem.]
 161 //
 162 //  SeeAlso     []
 163 //
 164 // ****************************************************************************
 165
 166 inline bool cmp_var_stat(const pair<CVariable *, int> & v1,
 167                          const pair<CVariable *, int> & v2) {
 168   return v1.second >= v2.second;
 169 }
 170
 171 struct cmp_var_assgn_pos {
 172   bool operator() (CVariable * v1, CVariable * v2) {
 173     if (v1->dlevel() > v2->dlevel())
 174       return true;
 175     else if (v1->dlevel() < v2->dlevel())
 176       return false;
 177     else if (v1->assgn_stack_pos() > v2->assgn_stack_pos())
 178       return true;
 179     return false;
 180   }
 181 };
 182
 183 struct CImplication {
 184   int lit;
 185   int antecedent;
 186 };
 187
 188 struct ImplicationQueue:queue<CImplication> {
 189   void dump(ostream & os) {
 190     queue<CImplication> temp(*this);
 191     os << "Implication Queue Previous: " ;
 192     while (!temp.empty()) {
 193       CImplication a = temp.front();
 194       os << "(" << ((a.lit & 0x1) ? "-" : "+") << (a.lit >> 1)
 195          << ":" << a.antecedent << ")  ";
 196       temp.pop();
 197     }
 198   }
 199 };
 200
 201 class CSolver:public CDatabase {
 202   protected:
 203     int                 _id;                  // the id of the solver, in case
 204                                               // we need to distinguish
 205     bool                _force_terminate;
 206     CSolverParameters   _params;              // parameters for the solver
 207     CSolverStats        _stats;               // statistics and states
 208
 209     int                 _dlevel;              // current decision elvel
 210     vector<vector<int>*>_assignment_stack;
 211     queue<int>          _recent_shrinkings;
 212     bool                _mark_increase_score;  // used in mark_vars during
 213                                               // multiple conflict analysis
 214     long64              _implication_id;
 215     ImplicationQueue    _implication_queue;
 216
 217     // hook function run after certain number of decisions
 218     vector<pair<int, pair<HookFunPtrT, int> > > _hooks;
 219     OutsideConstraintHookPtrT                   _outside_constraint_hook;
 220     SatHookPtrT         _sat_hook;  // hook function run after a satisfiable
 221                                     // solution found, return true to continue
 222                               // solving and false to terminate as satisfiable
 223
 224     // these are for decision making
 225     int                 _max_score_pos;   // index the unassigned var with
 226                                           // max score
 227     vector<pair<CVariable*, int> > _ordered_vars;  // pair's first pointing to
 228                                               // the var, second is the score.
 229
 230     // these are for conflict analysis
 231     int               _num_marked;     // used when constructing learned clause
 232     int               _num_in_new_cl;  // used when constructing learned clause
 233     vector<ClauseIdx> _conflicts;      // the conflicting clauses
 234     vector<int>       _conflict_lits;  // used when constructing learned clause
 235     vector<int>       _resolvents;
 236     multimap<int, int> _shrinking_cls;
 237
 238   protected:
 239     void re_init_stats(void);
 240     void init_stats(void);
 241     void init_parameters(void);
 242     void init_solve(void);
 243     void real_solve(void);
 244     void restart(void);
 245     int preprocess(void);
 246     int deduce(void);
 247     void run_periodic_functions(void);
 248
 249     // for decision making
 250     bool decide_next_branch(void);
 251     void decay_variable_score(void) ;
 252     void adjust_variable_order(int * lits, int n_lits);
 253     void update_var_score(void);
 254
 255     // for conflict analysis
 256     ClauseIdx add_conflict_clause(int * lits, int n_lits, int gflag);
 257     int analyze_conflicts(void);
 258     ClauseIdx finish_add_conf_clause(int gflag);
 259     int conflict_analysis_firstUIP(void);
 260     void mark_vars(ClauseIdx cl, int var_idx);
 261     void back_track(int level);
 262
 263     // for bcp
 264     void set_var_value(int var, int value, ClauseIdx ante, int dl);
 265     void set_var_value_BCP(int v, int value);
 266     void unset_var_value(int var);
 267
 268     // misc functions
 269     bool time_out(void);
 270     void delete_unrelevant_clauses(void);
 271     ClauseIdx add_clause_with_gid(int * lits, int n_lits, int gid = 0);
 272
 273   public:
 274     // constructors and destructors
 275     CSolver(void);
 276     ~CSolver(void);
 277
 278     // member access function
 279     void set_time_limit(float t);
 280     void set_mem_limit(int s);
 281     void enable_cls_deletion(bool allow);
 282     void set_randomness(int n) ;
 283     void set_random_seed(int seed);
 284
 285     void set_variable_number(int n);
 286     int add_variable(void) ;
 287     void mark_var_branchable(int vid);
 288     void mark_var_unbranchable(int vid);
 289
 290     inline int & dlevel(void) {
 291       return _dlevel;
 292     }
 293
 294     inline int outcome(void) {
 295       return _stats.outcome;
 296     }
 297
 298     inline int num_decisions(void) {
 299       return _stats.num_decisions;
 300     }
 301
 302     inline int num_decisions_stack_conf(void) {
 303       return _stats.num_decisions_stack_conf;
 304     }
 305
 306     inline int num_decisions_vsids(void) {
 307       return _stats.num_decisions_vsids;
 308     }
 309
 310     inline int num_decisions_shrinking(void) {
 311       return _stats.num_decisions_shrinking;
 312     }
 313
 314     inline int num_shrinkings(void) {
 315       return _stats.num_shrinkings;
 316     }
 317
 318     inline int & num_free_variables(void) {
 319       return _stats.num_free_variables;
 320     }
 321
 322     inline int max_dlevel(void) {
 323       return _stats.max_dlevel;
 324     }
 325
 326     inline int random_seed(void) {
 327       return _stats.random_seed;
 328     }
 329
 330     inline long64 num_implications(void) {
 331       return _stats.num_implications;
 332     }
 333
 334     inline long64 total_bubble_move(void) {
 335       return _stats.total_bubble_move;
 336     }
 337
 338     inline char * version(void) {
 339       return __ZCHAFF_VERSION__;
 340     }
 341
 342     float elapsed_cpu_time(void);
 343     float cpu_run_time(void) ;
 344     int estimate_mem_usage(void) {
 345       return CDatabase::estimate_mem_usage();
 346     }
 347
 348     int mem_usage(void);
 349
 350     void queue_implication(int lit, ClauseIdx ante_clause) {
 351       CImplication i;
 352       i.lit = lit;
 353       i.antecedent = ante_clause;
 354       _implication_queue.push(i);
 355     }
 356
 357     // top level function
 358     inline int id(void) {
 359       return _id;
 360     }
 361
 362     inline void set_id(int i) {
 363       _id = i;
 364     }
 365
 366     inline void force_terminate(void) {
 367       _force_terminate = true;
 368     }
 369
 370     inline void unset_force_terminate(void) {
 371       _force_terminate = false;
 372     }
 373
 374     // for incremental SAT
 375     int add_clause_incr(int * lits, int n_lits, int gid = 0);
 376
 377     void make_decision(int lit) {
 378         ++dlevel();
 379         queue_implication(lit, NULL_CLAUSE);
 380     }
 381
 382     void add_hook(HookFunPtrT fun, int interval);
 383
 384     inline void add_outside_constraint_hook(OutsideConstraintHookPtrT fun) {
 385       _outside_constraint_hook = fun;
 386     }
 387
 388     inline void add_sat_hook(SatHookPtrT fun) {
 389       _sat_hook = fun;
 390     }
 391
 392     void verify_integrity(void);
 393     void delete_clause_group(int gid);
 394     void reset(void);
 395     int solve(void);
 396     ClauseIdx add_orig_clause(int * lits, int n_lits, int gid = 0);
 397     void clean_up_dbase(void);
 398     void dump_assignment_stack(ostream & os = cout);
 399     void dump_implication_queue(ostream & os = cout);
 400
 401     void print_cls(ostream & os = cout);
 402     void dump(ostream & os = cout ) {
 403         CDatabase::dump(os);
 404         dump_assignment_stack(os);
 405     }
 406     void add_outside_clauses(void);
 407 };
 408 #endif