CVC3
xchaff_solver.h
Go to the documentation of this file.
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__
59 };
60 #endif
61 
65 };
66 
67 typedef void(*HookFunPtrT)(void *) ;
68 /**Struct**********************************************************************
69 
70  Synopsis [Sat solver parameters ]
71 
72  Description []
73 
74  SeeAlso []
75 
76 ******************************************************************************/
78  float time_limit;
79 
82 
89 
90  int verbosity;
92 
102 
107 };
108 /**Struct**********************************************************************
109 
110  Synopsis [Sat solver statistics ]
111 
112  Description []
113 
114  SeeAlso []
115 
116 ******************************************************************************/
117 struct CSolverStats {
119  int outcome;
120 
121  bool is_mem_out; //this flag will be set if memory out
122 
128 
130 
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;
156 
157  vector<pair<int,pair< HookFunPtrT, int> > > _hooks;
158 
159 //these are for decision making
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 *);
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
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);
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
228  void set_time_limit(float t)
229  { _params.time_limit = t; }
230  void set_mem_limit(int s) {
232  }
234  { _params.decision_strategy = s; }
237  void enable_cls_deletion(bool allow)
238  { _params.allow_clause_deletion = allow; }
241  void set_max_unrelevance(int n )
242  { _params.max_unrelevance = n; }
247  void set_allow_multiple_conflict( bool b = false) {
249  }
250  void set_allow_multiple_conflict_clause( bool b = false) {
252  }
253  void set_randomness(int n) {
255  }
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
264  void RegisterDLevelHook(void (*f)(void *, int), void *cookie)
265  { _dlevel_hook = f; _dlevel_hook_cookie = cookie; }
266  void RegisterDecisionHook(int (*f)(void *, bool *), void *cookie)
267  { _decision_hook = f; _decision_hook_cookie = cookie; }
268  void RegisterAssignmentHook(void (*f)(void *, int, int), void *cookie)
269  { _assignment_hook = f; _assignment_hook_cookie = cookie; }
270  void RegisterDeductionHook(void (*f)(void *), void *cookie)
271  { _deduction_hook = f;
272  _deduction_hook_cookie = cookie; }
273 
274  int outcome () { return _stats.outcome; }
277  return _stats.num_free_variables;
278  }
279  int max_dlevel() { return _stats.max_dlevel; }
282 
283  const char * version(void){
284  return "Z2001.2.17";
285  }
286 
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 
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 
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 
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 
316  float cpu_run_time() {
317  return (_stats.finish_cpu_time -
318  _stats.start_cpu_time)/1000.0 ;
319  }
320 
321  float world_run_time() {
322  return (_stats.finish_world_time -
323  _stats.start_world_time) / 1000.0 ;
324  }
325 
328  }
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  }
337  int & dlevel() { return _dlevel; }
338 
339 //top level function
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 
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);
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  }
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);
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