source: vis_dev/zchaff/zchaff_solver.h @ 77

Last change on this file since 77 was 10, checked in by cecile, 13 years ago

Zchaff

File size: 12.0 KB
Line 
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
45enum SAT_StatusT {
46  UNDETERMINED,
47  UNSATISFIABLE,
48  SATISFIABLE,
49  TIME_OUT,
50  MEM_OUT,
51  ABORTED
52};
53#endif
54
55enum SAT_DeductionT {
56  CONFLICT,
57  NO_CONFLICT
58};
59
60class CSolver;
61
62typedef void(*HookFunPtrT)(void *) ;
63typedef void(*OutsideConstraintHookPtrT)(CSolver * solver);
64typedef bool(*SatHookPtrT)(CSolver * solver);
65
66// **Struct********************************************************************
67//
68//  Synopsis    [Sat solver parameters ]
69//
70//  Description []
71//
72//  SeeAlso     []
73//
74// ****************************************************************************
75
76struct 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
125struct 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
166inline bool cmp_var_stat(const pair<CVariable *, int> & v1,
167                         const pair<CVariable *, int> & v2) {
168  return v1.second >= v2.second;
169}
170
171struct 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
183struct CImplication {
184  int lit;
185  int antecedent;
186};
187
188struct 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
201class 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 const 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
Note: See TracBrowser for help on using the repository browser.