1 /* =========FOR INTERNAL USE ONLY. NO DISTRIBUTION PLEASE ========== */ 2 3 /********************************************************************* 4 Copyright 2000-2001, Princeton University. All rights reserved. 5 By using this software the USER indicates that he or she has read, 6 understood and will comply with the following: 7 8 --- Princeton University hereby grants USER nonexclusive permission 9 to use, copy and/or modify this software for internal, noncommercial, 10 research purposes only. Any distribution, including commercial sale 11 or license, of this software, copies of the software, its associated 12 documentation and/or modifications of either is strictly prohibited 13 without the prior consent of Princeton University. Title to copyright 14 to this software and its associated documentation shall at all times 15 remain with Princeton University. Appropriate copyright notice shall 16 be placed on all software copies, and a complete copy of this notice 17 shall be included in all copies of the associated documentation. 18 No right is granted to use in advertising, publicity or otherwise 19 any trademark, service mark, or the name of Princeton University. 20 21 22 --- This software and any associated documentation is provided "as is" 23 24 PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS 25 OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A 26 PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR 27 ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, 28 TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. 29 30 Princeton University shall not be liable under any circumstances for 31 any direct, indirect, special, incidental, or consequential damages 32 with respect to any claim by USER or any third party on account of 33 or arising from the use, or inability to use, this software or its 34 associated documentation, even if Princeton University has been advised 35 of the possibility of those damages. 36 *********************************************************************/ 37 38 39 40 #ifndef __SAT_SOLVER__ 41 #define __SAT_SOLVER__ 42 43 #include <sys/time.h> 44 #include <sys/resource.h> 45 #include <stdlib.h> 46 47 #include "xchaff_utils.h" 48 #include "xchaff_dbase.h" 49 50 #ifndef __SAT_STATUS__ 51 #define __SAT_STATUS__ 52 enum SAT_StatusT { 53 UNDETERMINED, 54 UNSATISFIABLE, 55 SATISFIABLE, 56 TIME_OUT, 57 MEM_OUT, 58 ABORTED 59 }; 60 #endif 61 62 enum SAT_DeductionT { 63 CONFLICT, 64 NO_CONFLICT 65 }; 66 67 typedef void(*HookFunPtrT)(void *) ; 68 /**Struct********************************************************************** 69 70 Synopsis [Sat solver parameters ] 71 72 Description [] 73 74 SeeAlso [] 75 76 ******************************************************************************/ 77 struct CSolverParameters { 78 float time_limit; 79 80 int decision_strategy; 81 int preprocess_strategy; 82 83 bool allow_clause_deletion; 84 int clause_deletion_interval; 85 int max_unrelevance; 86 int min_num_clause_lits_for_delete; 87 int max_conflict_clause_length; 88 int bubble_init_step; 89 90 int verbosity; 91 int randomness; 92 93 bool allow_restart; 94 float next_restart_time; 95 float restart_time_increment; 96 float restart_time_incr_incr; 97 int next_restart_backtrack; 98 int restart_backtrack_incr; 99 int restart_backtrack_incr_incr; 100 int restart_randomness; 101 int base_randomness; 102 103 bool back_track_complete; 104 int conflict_analysis_method; 105 bool allow_multiple_conflict; 106 bool allow_multiple_conflict_clause; 107 }; 108 /**Struct********************************************************************** 109 110 Synopsis [Sat solver statistics ] 111 112 Description [] 113 114 SeeAlso [] 115 116 ******************************************************************************/ 117 struct CSolverStats { 118 bool is_solver_started; 119 int outcome; 120 121 bool is_mem_out; //this flag will be set if memory out 122 123 long start_cpu_time; 124 long last_cpu_time; 125 long finish_cpu_time; 126 long start_world_time; 127 long finish_world_time; 128 129 long total_bubble_move; 130 131 int num_decisions; 132 int num_backtracks; 133 int max_dlevel; 134 int num_implications; 135 int num_free_variables; 136 }; 137 138 /**Class********************************************************************** 139 140 Synopsis [Sat Solver] 141 142 Description [This class contains the process and datastructrues to solve 143 the Sat problem.] 144 145 SeeAlso [] 146 147 ******************************************************************************/ 148 class CSolver:public CDatabase 149 { 150 protected: 151 int _dlevel; //current decision elvel 152 vector<vector<int> *> _assignment_stack; 153 queue<pair<int,ClauseIdx> > _implication_queue; 154 CSolverParameters _params; 155 CSolverStats _stats; 156 157 vector<pair<int,pair< HookFunPtrT, int> > > _hooks; 158 159 //these are for decision making 160 int _max_score_pos; 161 vector<int> _last_var_lits_count[2]; 162 vector<pair<int,int> >_var_order; 163 164 //these are for conflict analysis 165 int _num_marked; //used when constructing conflict clauses 166 vector<ClauseIdx> _conflicts; //the conflict clauses 167 vector<long> _conflict_lits; //used when constructing conflict clauses 168 169 //these are for the extended API 170 void (*_dlevel_hook)(void *, int); 171 int (*_decision_hook)(void *, bool *); 172 void (*_assignment_hook)(void *, int, int); 173 void (*_deduction_hook)(void *); 174 void *_dlevel_hook_cookie; 175 void *_decision_hook_cookie; 176 void *_assignment_hook_cookie; 177 void *_deduction_hook_cookie; 178 179 //needed to support dynamic adding of unit clauses 180 vector<ClauseIdx> _addedUnitClauses; 181 182 protected: 183 void real_solve(void); 184 185 int preprocess(bool allowNewClauses); 186 187 int deduce(void); 188 189 bool decide_next_branch(void); 190 191 int analyze_conflicts(void); 192 int conflict_analysis_grasp (void); 193 int conflict_analysis_zchaff (void); 194 195 void back_track(int level); 196 197 void init(void); 198 //for conflict analysis 199 void mark_vars_at_level(ClauseIdx cl, 200 int var_idx, 201 int dl); 202 203 int find_max_clause_dlevel(ClauseIdx cl); //the max dlevel of all the assigned lits in this clause 204 205 //for bcp 206 void set_var_value(int var, 207 int value, 208 ClauseIdx ante, 209 int dl); 210 void set_var_value_not_current_dl(int v, 211 vector<CLitPoolElement *> & neg_ht_clauses); 212 void set_var_value_with_current_dl(int v, 213 vector<CLitPoolElement*> & neg_ht_clauses); 214 void unset_var_value(int var); 215 216 void run_periodic_functions (void); 217 //misc functions 218 void update_var_stats(void); 219 220 bool time_out(void); 221 222 void delete_unrelevant_clauses(void); 223 public: 224 //constructors and destructors 225 CSolver() ; 226 ~CSolver(); 227 //member access function set_time_limit(float t)228 void set_time_limit(float t) 229 { _params.time_limit = t; } set_mem_limit(int s)230 void set_mem_limit(int s) { 231 CDatabase::set_mem_limit(s); 232 } set_decision_strategy(int s)233 void set_decision_strategy(int s) 234 { _params.decision_strategy = s; } set_preprocess_strategy(int s)235 void set_preprocess_strategy(int s) 236 { _params.preprocess_strategy = s; } enable_cls_deletion(bool allow)237 void enable_cls_deletion(bool allow) 238 { _params.allow_clause_deletion = allow; } set_cls_del_interval(int n)239 void set_cls_del_interval(int n) 240 { _params.clause_deletion_interval = n; } set_max_unrelevance(int n)241 void set_max_unrelevance(int n ) 242 { _params.max_unrelevance = n; } set_min_num_clause_lits_for_delete(int n)243 void set_min_num_clause_lits_for_delete(int n) 244 { _params.min_num_clause_lits_for_delete = n; } set_max_conflict_clause_length(int l)245 void set_max_conflict_clause_length(int l) 246 { _params.max_conflict_clause_length = l; } 247 void set_allow_multiple_conflict( bool b = false) { 248 _params.allow_multiple_conflict = b ; 249 } 250 void set_allow_multiple_conflict_clause( bool b = false) { 251 _params.allow_multiple_conflict_clause = b; 252 } set_randomness(int n)253 void set_randomness(int n) { 254 _params.base_randomness = n; 255 } set_random_seed(int seed)256 void set_random_seed(int seed) { 257 if (seed < 0) 258 srand ( current_world_time() ); 259 else 260 srand (seed); 261 } 262 263 //these are for the extended API RegisterDLevelHook(void (* f)(void *,int),void * cookie)264 void RegisterDLevelHook(void (*f)(void *, int), void *cookie) 265 { _dlevel_hook = f; _dlevel_hook_cookie = cookie; } RegisterDecisionHook(int (* f)(void *,bool *),void * cookie)266 void RegisterDecisionHook(int (*f)(void *, bool *), void *cookie) 267 { _decision_hook = f; _decision_hook_cookie = cookie; } RegisterAssignmentHook(void (* f)(void *,int,int),void * cookie)268 void RegisterAssignmentHook(void (*f)(void *, int, int), void *cookie) 269 { _assignment_hook = f; _assignment_hook_cookie = cookie; } RegisterDeductionHook(void (* f)(void *),void * cookie)270 void RegisterDeductionHook(void (*f)(void *), void *cookie) 271 { _deduction_hook = f; 272 _deduction_hook_cookie = cookie; } 273 outcome()274 int outcome () { return _stats.outcome; } num_decisions()275 int num_decisions() { return _stats.num_decisions; } num_free_variables()276 int & num_free_variables() { 277 return _stats.num_free_variables; 278 } max_dlevel()279 int max_dlevel() { return _stats.max_dlevel; } num_implications()280 int num_implications() { return _stats.num_implications; } total_bubble_move(void)281 long total_bubble_move(void) { return _stats.total_bubble_move; } 282 version(void)283 const char * version(void){ 284 return "Z2001.2.17"; 285 } 286 current_cpu_time(void)287 int current_cpu_time(void) { 288 struct rusage ru; 289 getrusage(RUSAGE_SELF, &ru); 290 return ( ru.ru_utime.tv_sec*1000 + 291 ru.ru_utime.tv_usec/1000+ 292 ru.ru_stime.tv_sec*1000 + 293 ru.ru_stime.tv_usec/1000 ); 294 } 295 current_world_time(void)296 int current_world_time(void) { 297 struct timeval tv; 298 struct timezone tz; 299 gettimeofday(&tv,&tz); 300 return (tv.tv_sec * 1000 + tv.tv_usec/1000) ; 301 } 302 elapsed_cpu_time()303 float elapsed_cpu_time() { 304 int current = current_cpu_time(); 305 int diff = current - _stats.last_cpu_time; 306 _stats.last_cpu_time = current; 307 return diff/1000.0; 308 } 309 total_run_time()310 float total_run_time() { 311 if (!_stats.is_solver_started) return 0; 312 return (current_cpu_time() - 313 _stats.start_cpu_time)/1000.0 ; 314 } 315 cpu_run_time()316 float cpu_run_time() { 317 return (_stats.finish_cpu_time - 318 _stats.start_cpu_time)/1000.0 ; 319 } 320 world_run_time()321 float world_run_time() { 322 return (_stats.finish_world_time - 323 _stats.start_world_time) / 1000.0 ; 324 } 325 estimate_mem_usage()326 int estimate_mem_usage() { 327 return CDatabase::estimate_mem_usage(); 328 } mem_usage(void)329 int mem_usage(void) { 330 int mem_dbase = CDatabase::mem_usage(); 331 int mem_assignment = 0; 332 for (int i=0; i< _stats.max_dlevel; ++i) 333 mem_assignment += _assignment_stack[i]->capacity() * sizeof(int); 334 mem_assignment += sizeof(vector<int>)* _assignment_stack.size(); 335 return mem_dbase + mem_assignment; 336 } dlevel()337 int & dlevel() { return _dlevel; } 338 339 //top level function add_hook(HookFunPtrT fun,int interval)340 void add_hook( HookFunPtrT fun, int interval) { 341 pair<HookFunPtrT, int> a(fun, interval); 342 _hooks.push_back(pair<int, pair<HookFunPtrT, int> > (0, a)); 343 } 344 queue_implication(int lit,ClauseIdx ante_clause)345 void queue_implication (int lit, ClauseIdx ante_clause) { 346 CHECK (cout << "\t\t\t\t\t\tQueueing " << (lit&0x01?" -":" +") << (lit>>1) ; 347 cout << " because of " << ante_clause << endl; ); 348 _implication_queue.push(pair<int, ClauseIdx>(lit, ante_clause)); 349 } 350 351 int add_variables(int new_vars); 352 353 ClauseIdx add_clause(vector<long>& lits, bool addConflicts=true); 354 355 void verify_integrity(void); 356 357 // ClauseIdx add_clause_with_order_adjustment(int * lits, int n_lits); restart(void)358 void restart (void){ 359 if (_params.verbosity > 1 ) 360 cout << "Restarting ... " << endl; 361 if (dlevel() > 1) { 362 //clean up the original var_stats. 363 for (unsigned i=1; i<variables().size(); ++i) { 364 variable(i).score(0) = 0; 365 variable(i).score(1) = 0; 366 _last_var_lits_count[0][i] = 0; 367 _last_var_lits_count[1][i] = 0; 368 } 369 update_var_stats(); 370 back_track(1); //backtrack to level 0. restart. 371 } 372 } 373 374 int solve(bool allowNewClauses); 375 int continueCheck(); 376 377 void dump_assignment_stack(ostream & os = cout); 378 379 void output_current_stats(void); 380 381 void dump(ostream & os = cout ) { 382 CDatabase::dump(os); 383 dump_assignment_stack(os); 384 } 385 }; 386 #endif 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418